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 = 1 st A

Proof

Step Hyp Ref Expression
1 elvv A V × V w 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 V , y V x = x y z | z = x
6 5 eqcomi x y z | z = x = x V , y V x
7 vex w V
8 4 6 7 ovmpoa w V v 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 V
13 7 12 op1std A = w v 1 st A = w
14 11 13 eqtr4d A = w v x y z | z = x A = 1 st A
15 14 exlimivv w v A = w v x y z | z = x A = 1 st A
16 1 15 sylbi A V × V x y z | z = x A = 1 st A
17 vex x V
18 vex y V
19 17 18 pm3.2i x V y V
20 ax6ev z z = x
21 19 20 2th x V y V z z = x
22 21 opabbii x y | x V y V = x y | z z = x
23 df-xp V × V = x y | x V y V
24 dmoprab dom x y z | z = x = x y | z z = x
25 22 23 24 3eqtr4ri dom x y z | z = x = V × V
26 25 eleq2i A dom x y z | z = x A V × V
27 ndmfv ¬ A dom x y z | z = x x y z | z = x A =
28 26 27 sylnbir ¬ A V × V x y z | z = x A =
29 dmsnn0 A V × V dom A
30 29 biimpri dom A A V × V
31 30 necon1bi ¬ A V × V dom A =
32 31 unieqd ¬ A V × V dom A =
33 uni0 =
34 32 33 eqtrdi ¬ A V × V dom A =
35 28 34 eqtr4d ¬ A V × V x y z | z = x A = dom A
36 1stval 1 st A = dom A
37 35 36 eqtr4di ¬ A V × V x y z | z = x A = 1 st A
38 16 37 pm2.61i x y z | z = x A = 1 st A