This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 vsnex 
 |-  { 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 eqabi 
 |-  _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