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 )