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

Metamath Proof Explorer

Theorem 2ndval

Description: The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion 2ndval 
|- ( 2nd ` A ) = U. ran { A }

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( x = A -> { x } = { A } )
2 1 rneqd 
 |-  ( x = A -> ran { x } = ran { A } )
3 2 unieqd 
 |-  ( x = A -> U. ran { x } = U. ran { A } )
4 df-2nd 
 |-  2nd = ( x e. _V |-> U. ran { x } )
5 snex 
 |-  { A } e. _V
6 5 rnex 
 |-  ran { A } e. _V
7 6 uniex 
 |-  U. ran { A } e. _V
8 3 4 7 fvmpt 
 |-  ( A e. _V -> ( 2nd ` A ) = U. ran { A } )
9 fvprc 
 |-  ( -. A e. _V -> ( 2nd ` A ) = (/) )
10 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
11 10 biimpi 
 |-  ( -. A e. _V -> { A } = (/) )
12 11 rneqd 
 |-  ( -. A e. _V -> ran { A } = ran (/) )
13 rn0 
 |-  ran (/) = (/)
14 12 13 eqtrdi 
 |-  ( -. A e. _V -> ran { A } = (/) )
15 14 unieqd 
 |-  ( -. A e. _V -> U. ran { A } = U. (/) )
16 uni0 
 |-  U. (/) = (/)
17 15 16 eqtrdi 
 |-  ( -. A e. _V -> U. ran { A } = (/) )
18 9 17 eqtr4d 
 |-  ( -. A e. _V -> ( 2nd ` A ) = U. ran { A } )
19 8 18 pm2.61i 
 |-  ( 2nd ` A ) = U. ran { A }