Metamath Proof Explorer

Theorem 2nd2val

Description: Value of an alternate definition of the 2nd function. (Contributed by NM, 10-Aug-2006) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Assertion 2nd2val 
|- ( { <. <. x , y >. , z >. | z = y } ` A ) = ( 2nd ` A )

Proof

Step Hyp Ref Expression
1 elvv 
 |-  ( A e. ( _V X. _V ) <-> E. w E. v A = <. w , v >. )
2 fveq2 
 |-  ( A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = y } ` A ) = ( { <. <. x , y >. , z >. | z = y } ` <. w , v >. ) )
3 df-ov 
 |-  ( w { <. <. x , y >. , z >. | z = y } v ) = ( { <. <. x , y >. , z >. | z = y } ` <. w , v >. )
4 simpr 
 |-  ( ( x = w /\ y = v ) -> y = v )
5 mpov 
 |-  ( x e. _V , y e. _V |-> y ) = { <. <. x , y >. , z >. | z = y }
6 5 eqcomi 
 |-  { <. <. x , y >. , z >. | z = y } = ( x e. _V , y e. _V |-> y )
7 vex 
 |-  v e. _V
8 4 6 7 ovmpoa 
 |-  ( ( w e. _V /\ v e. _V ) -> ( w { <. <. x , y >. , z >. | z = y } v ) = v )
9 8 el2v 
 |-  ( w { <. <. x , y >. , z >. | z = y } v ) = v
10 3 9 eqtr3i 
 |-  ( { <. <. x , y >. , z >. | z = y } ` <. w , v >. ) = v
11 2 10 eqtrdi 
 |-  ( A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = y } ` A ) = v )
12 vex 
 |-  w e. _V
13 12 7 op2ndd 
 |-  ( A = <. w , v >. -> ( 2nd ` A ) = v )
14 11 13 eqtr4d 
 |-  ( A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = y } ` A ) = ( 2nd ` A ) )
15 14 exlimivv 
 |-  ( E. w E. v A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = y } ` A ) = ( 2nd ` A ) )
16 1 15 sylbi 
 |-  ( A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = y } ` A ) = ( 2nd ` A ) )
17 vex 
 |-  x e. _V
18 vex 
 |-  y e. _V
19 17 18 pm3.2i 
 |-  ( x e. _V /\ y e. _V )
20 ax6ev 
 |-  E. z z = y
21 19 20 2th 
 |-  ( ( x e. _V /\ y e. _V ) <-> E. z z = y )
22 21 opabbii 
 |-  { <. x , y >. | ( x e. _V /\ y e. _V ) } = { <. x , y >. | E. z z = y }
23 df-xp 
 |-  ( _V X. _V ) = { <. x , y >. | ( x e. _V /\ y e. _V ) }
24 dmoprab 
 |-  dom { <. <. x , y >. , z >. | z = y } = { <. x , y >. | E. z z = y }
25 22 23 24 3eqtr4ri 
 |-  dom { <. <. x , y >. , z >. | z = y } = ( _V X. _V )
26 25 eleq2i 
 |-  ( A e. dom { <. <. x , y >. , z >. | z = y } <-> A e. ( _V X. _V ) )
27 ndmfv 
 |-  ( -. A e. dom { <. <. x , y >. , z >. | z = y } -> ( { <. <. x , y >. , z >. | z = y } ` A ) = (/) )
28 26 27 sylnbir 
 |-  ( -. A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = y } ` A ) = (/) )
29 rnsnn0 
 |-  ( A e. ( _V X. _V ) <-> ran { A } =/= (/) )
30 29 biimpri 
 |-  ( ran { A } =/= (/) -> A e. ( _V X. _V ) )
31 30 necon1bi 
 |-  ( -. A e. ( _V X. _V ) -> ran { A } = (/) )
32 31 unieqd 
 |-  ( -. A e. ( _V X. _V ) -> U. ran { A } = U. (/) )
33 uni0 
 |-  U. (/) = (/)
34 32 33 eqtrdi 
 |-  ( -. A e. ( _V X. _V ) -> U. ran { A } = (/) )
35 28 34 eqtr4d 
 |-  ( -. A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = y } ` A ) = U. ran { A } )
36 2ndval 
 |-  ( 2nd ` A ) = U. ran { A }
37 35 36 eqtr4di 
 |-  ( -. A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = y } ` A ) = ( 2nd ` A ) )
38 16 37 pm2.61i 
 |-  ( { <. <. x , y >. , z >. | z = y } ` A ) = ( 2nd ` A )