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	|- 2nd : _V -onto-> _V

Proof

Step	Hyp	Ref	Expression
1		snex	|- { x } e. _V
2	1	rnex	|- ran { x } e. _V
3	2	uniex	|- U. ran { x } e. _V
4		df-2nd	|- 2nd = ( x e. _V |-> U. ran { x } )
5	3 4	fnmpti	|- 2nd Fn _V
6	4	rnmpt	|- ran 2nd = { y | E. x e. _V y = U. ran { x } }
7		vex	|- y e. _V
8		opex	|- <. y , y >. e. _V
9	7 7	op2nda	|- U. ran { <. y , y >. } = y
10	9	eqcomi	|- y = U. ran { <. y , y >. }
11		sneq	|- ( x = <. y , y >. -> { x } = { <. y , y >. } )
12	11	rneqd	|- ( x = <. y , y >. -> ran { x } = ran { <. y , y >. } )
13	12	unieqd	|- ( x = <. y , y >. -> U. ran { x } = U. ran { <. y , y >. } )
14	13	rspceeqv	|- ( ( <. y , y >. e. _V /\ y = U. ran { <. y , y >. } ) -> E. x e. _V y = U. ran { x } )
15	8 10 14	mp2an	|- E. x e. _V y = U. ran { x }
16	7 15	2th	|- ( y e. _V <-> E. x e. _V y = U. ran { x } )
17	16	abbi2i	|- _V = { y | E. x e. _V y = U. ran { x } }
18	6 17	eqtr4i	|- ran 2nd = _V
19		df-fo	|- ( 2nd : _V -onto-> _V <-> ( 2nd Fn _V /\ ran 2nd = _V ) )
20	5 18 19	mpbir2an	|- 2nd : _V -onto-> _V