Theorem fo2nd

Description: The 2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	fo2nd	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
2	1	rnex	$$⊢\mathrm{ran}\left\{x\right\}\in \mathrm{V}$$
3	2	uniex	$$⊢\bigcup \mathrm{ran}\left\{x\right\}\in \mathrm{V}$$
4		df-2nd	$$⊢2^{nd}=\left(x\in \mathrm{V}⟼\bigcup \mathrm{ran}\left\{x\right\}\right)$$
5	3 4	fnmpti	$$⊢2^{nd}Fn\mathrm{V}$$
6	4	rnmpt	$$⊢\mathrm{ran}{2}^{nd}=\left\{y|\exists x\in \mathrm{V}y=\bigcup \mathrm{ran}\left\{x\right\}\right\}$$
7		vex	$$⊢y\in \mathrm{V}$$
8		opex	$$⊢⟨y,y⟩\in \mathrm{V}$$
9	7 7	op2nda	$$⊢\bigcup \mathrm{ran}\left\{⟨y,y⟩\right\}=y$$
10	9	eqcomi	$$⊢y=\bigcup \mathrm{ran}\left\{⟨y,y⟩\right\}$$
11		sneq	$$⊢x=⟨y,y⟩\to \left\{x\right\}=\left\{⟨y,y⟩\right\}$$
12	11	rneqd	$$⊢x=⟨y,y⟩\to \mathrm{ran}\left\{x\right\}=\mathrm{ran}\left\{⟨y,y⟩\right\}$$
13	12	unieqd	$$⊢x=⟨y,y⟩\to \bigcup \mathrm{ran}\left\{x\right\}=\bigcup \mathrm{ran}\left\{⟨y,y⟩\right\}$$
14	13	rspceeqv	$$⊢\left(⟨y,y⟩\in \mathrm{V}\wedge y=\bigcup \mathrm{ran}\left\{⟨y,y⟩\right\}\right)\to \exists x\in \mathrm{V}y=\bigcup \mathrm{ran}\left\{x\right\}$$
15	8 10 14	mp2an	$$⊢\exists x\in \mathrm{V}y=\bigcup \mathrm{ran}\left\{x\right\}$$
16	7 15	2th	$$⊢y\in \mathrm{V}\leftrightarrow \exists x\in \mathrm{V}y=\bigcup \mathrm{ran}\left\{x\right\}$$
17	16	abbi2i	$$⊢\mathrm{V}=\left\{y|\exists x\in \mathrm{V}y=\bigcup \mathrm{ran}\left\{x\right\}\right\}$$
18	6 17	eqtr4i	$$⊢\mathrm{ran}{2}^{nd}=\mathrm{V}$$
19		df-fo	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\leftrightarrow \left(2^{nd}Fn\mathrm{V}\wedge \mathrm{ran}{2}^{nd}=\mathrm{V}\right)$$
20	5 18 19	mpbir2an	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$