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