Theorem fo1st

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

	Ref	Expression
Assertion	fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$

Proof

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