Consider a non-trivial elementary embedding $j:V\_\lambda\to V\_\lambda$ and, for each $A\subset V\_\lambda$, set $j(A)=\bigcup\_{\delta<\lambda}j(A\cap V\_\delta)$.


In *Implications between strong large cardinals,* Annals of Pure and Applied Logic 90 (1997) 79-90, Laver says that $j:(V\_\lambda, \in,A)\to (V\_\lambda, \in, j(A))$ is an elementary embedding.


I think that this is equivalent to $j$ being $\Sigma\_0^1$-elementary, i.e., it satisfies the definition of elementary embedding for formulas with second order variables but without second order quantifiers.


Could someone provide a hint or a reference for this fact? I think I could prove it from a particular case, namely, that $\forall x\in V\_\lambda\exists y\in V\_\lambda\ (x,y)\in A$ implies $\forall x\in V\_\lambda\exists y\in V\_\lambda\ (x,y)\in j(A)$.


Does this case follow easily from $j$ being elementary? I cannot see it.


Edited:


I have found a proof in chapter 2 of [these notes](http://www.logic.univie.ac.at/~dimonte/notes.htm) (theorem 0.4), but I think that the proof has a gap, since it considers skolem functions $f\_i$ and assumes tacitly that $j(f\_i)$ are also total functions, but they could be just partial functions.



A question on rank-to-rank embeddings
Here is the author of the notes you quoted. Thank you very much for pointing this out, there is indeed a gap in the proof: I truly took for granted that if $f$ is total then $j^+(f)$ is total (more specifically, that if $f$ is a Skolem function, then $j^+(f)$ is a Skolem function, but once one has totality, the rest is easy).


Anyway, I think this is true. In fact, I think the following is true:


**Lemma** If $f:V\_\lambda\to V\_\lambda$ is a partial function, then $j^+(dom(f))=dom(j^+(f))$.


This is not immediate: by definition, $j^+(dom(f))=\bigcup\_{n\in\omega}j(dom(f)\cap V\_{\kappa\_n})$; on the other hand, $dom(j^+(f))=\bigcup\_{n\in\omega}j(dom(f\cap V\_{\kappa\_n}))$, and the single summands are not equal, for example if $f$ is the critical sequence then $j(dom(f\cap V\_{\kappa\_n}))=\{0,\dots,n-2\}$, while $j(dom(f)\cap V\_{\kappa\_n})$ is always $\omega$. 


The following is an attempt for proving this. I don't see any errors (but then again, I didn't in my notes). Sorry for the unpleasant wall of equations, that is just how I did it. Maybe there is another, more synthetic way to prove it.


*Proof of Lemma*. The trick is to uniformize the division in pieces, i.e., to consider $dom(f\cap V\_{\kappa\_n})\cap V\_{\kappa\_m}$. Then


$j^+(dom(f))=\bigcup\_{m\in\omega}j(dom(f)\cap V\_{\kappa\_m})=\bigcup\_{m\in\omega}j(\bigcup\_{n\in\omega}dom(f\cap V\_{\kappa\_n})\cap V\_{\kappa\_m})$


because the dominion of the union of functions is the union of the dominions of the single functions. But now $\langle dom(f\cap V\_{\kappa\_n})\cap V\_{\kappa\_m}:n\in\omega\rangle$ is an $\omega$-sequence bounded in $V\_{\kappa\_m}$, therefore it is in $V\_\lambda$, so we can carry the $j$ inside


$\bigcup\_{m\in\omega}j(\bigcup\_{n\in\omega}dom(f\cap V\_{\kappa\_n})\cap V\_{\kappa\_m})=\bigcup\_{m\in\omega}\bigcup\_{n\in\omega}j(dom(f\cap V\_{\kappa\_n})\cap V\_{\kappa\_m})=$


$=\bigcup\_{n\in\omega}\bigcup\_{m\in\omega}j(dom(f\cap V\_{\kappa\_n})\cap V\_{\kappa\_m})$.


$dom(f\cap V\_{\kappa\_n})$ is an element of $V\_\lambda$, therefore there exists an $m$ such that it is in $V\_{\kappa\_m}$, so that is just a finite union.


$\bigcup\_{m\in\omega}\bigcup\_{n\in\omega}j(dom(f\cap V\_{\kappa\_n})\cap V\_{\kappa\_m})=\bigcup\_{n\in\omega}j(dom(f\cap V\_{\kappa\_n}))=j^+(dom(f))$.


