Metamath Proof Explorer

Theorem 1st2val

Description: Value of an alternate definition of the 1st function. (Contributed by NM, 14-Oct-2004) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Assertion 1st2val 
|- ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` 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 = x } ` A ) = ( { <. <. x , y >. , z >. | z = x } ` <. w , v >. ) )
3 df-ov 
 |-  ( w { <. <. x , y >. , z >. | z = x } v ) = ( { <. <. x , y >. , z >. | z = x } ` <. w , v >. )
4 simpl 
 |-  ( ( x = w /\ y = v ) -> x = w )
5 mpov 
 |-  ( x e. _V , y e. _V |-> x ) = { <. <. x , y >. , z >. | z = x }
6 5 eqcomi 
 |-  { <. <. x , y >. , z >. | z = x } = ( x e. _V , y e. _V |-> x )
7 vex 
 |-  w e. _V
8 4 6 7 ovmpoa 
 |-  ( ( w e. _V /\ v e. _V ) -> ( w { <. <. x , y >. , z >. | z = x } v ) = w )
9 8 el2v 
 |-  ( w { <. <. x , y >. , z >. | z = x } v ) = w
10 3 9 eqtr3i 
 |-  ( { <. <. x , y >. , z >. | z = x } ` <. w , v >. ) = w
11 2 10 eqtrdi 
 |-  ( A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = x } ` A ) = w )
12 vex 
 |-  v e. _V
13 7 12 op1std 
 |-  ( A = <. w , v >. -> ( 1st ` A ) = w )
14 11 13 eqtr4d 
 |-  ( A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A ) )
15 14 exlimivv 
 |-  ( E. w E. v A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A ) )
16 1 15 sylbi 
 |-  ( A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` 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 = x
21 19 20 2th 
 |-  ( ( x e. _V /\ y e. _V ) <-> E. z z = x )
22 21 opabbii 
 |-  { <. x , y >. | ( x e. _V /\ y e. _V ) } = { <. x , y >. | E. z z = x }
23 df-xp 
 |-  ( _V X. _V ) = { <. x , y >. | ( x e. _V /\ y e. _V ) }
24 dmoprab 
 |-  dom { <. <. x , y >. , z >. | z = x } = { <. x , y >. | E. z z = x }
25 22 23 24 3eqtr4ri 
 |-  dom { <. <. x , y >. , z >. | z = x } = ( _V X. _V )
26 25 eleq2i 
 |-  ( A e. dom { <. <. x , y >. , z >. | z = x } <-> A e. ( _V X. _V ) )
27 ndmfv 
 |-  ( -. A e. dom { <. <. x , y >. , z >. | z = x } -> ( { <. <. x , y >. , z >. | z = x } ` A ) = (/) )
28 26 27 sylnbir 
 |-  ( -. A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = x } ` A ) = (/) )
29 dmsnn0 
 |-  ( A e. ( _V X. _V ) <-> dom { A } =/= (/) )
30 29 biimpri 
 |-  ( dom { A } =/= (/) -> A e. ( _V X. _V ) )
31 30 necon1bi 
 |-  ( -. A e. ( _V X. _V ) -> dom { A } = (/) )
32 31 unieqd 
 |-  ( -. A e. ( _V X. _V ) -> U. dom { A } = U. (/) )
33 uni0 
 |-  U. (/) = (/)
34 32 33 eqtrdi 
 |-  ( -. A e. ( _V X. _V ) -> U. dom { A } = (/) )
35 28 34 eqtr4d 
 |-  ( -. A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = x } ` A ) = U. dom { A } )
36 1stval 
 |-  ( 1st ` A ) = U. dom { A }
37 35 36 eqtr4di 
 |-  ( -. A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A ) )
38 16 37 pm2.61i 
 |-  ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A )