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 ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd𝐴 )

Proof

Step Hyp Ref Expression
1 elvv ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑤𝑣 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ )
2 fveq2 ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ ⟨ 𝑤 , 𝑣 ⟩ ) )
3 df-ov ( 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } 𝑣 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ ⟨ 𝑤 , 𝑣 ⟩ )
4 simpr ( ( 𝑥 = 𝑤𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
5 mpov ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝑦 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 }
6 5 eqcomi { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝑦 )
7 vex 𝑣 ∈ V
8 4 6 7 ovmpoa ( ( 𝑤 ∈ V ∧ 𝑣 ∈ V ) → ( 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } 𝑣 ) = 𝑣 )
9 8 el2v ( 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } 𝑣 ) = 𝑣
10 3 9 eqtr3i ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ ⟨ 𝑤 , 𝑣 ⟩ ) = 𝑣
11 2 10 eqtrdi ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = 𝑣 )
12 vex 𝑤 ∈ V
13 12 7 op2ndd ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( 2nd𝐴 ) = 𝑣 )
14 11 13 eqtr4d ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd𝐴 ) )
15 14 exlimivv ( ∃ 𝑤𝑣 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd𝐴 ) )
16 1 15 sylbi ( 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd𝐴 ) )
17 vex 𝑥 ∈ V
18 vex 𝑦 ∈ V
19 17 18 pm3.2i ( 𝑥 ∈ V ∧ 𝑦 ∈ V )
20 ax6ev 𝑧 𝑧 = 𝑦
21 19 20 2th ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ↔ ∃ 𝑧 𝑧 = 𝑦 )
22 21 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 𝑧 = 𝑦 }
23 df-xp ( V × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
24 dmoprab dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 𝑧 = 𝑦 }
25 22 23 24 3eqtr4ri dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } = ( V × V )
26 25 eleq2i ( 𝐴 ∈ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ↔ 𝐴 ∈ ( V × V ) )
27 ndmfv ( ¬ 𝐴 ∈ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ∅ )
28 26 27 sylnbir ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ∅ )
29 rnsnn0 ( 𝐴 ∈ ( V × V ) ↔ ran { 𝐴 } ≠ ∅ )
30 29 biimpri ( ran { 𝐴 } ≠ ∅ → 𝐴 ∈ ( V × V ) )
31 30 necon1bi ( ¬ 𝐴 ∈ ( V × V ) → ran { 𝐴 } = ∅ )
32 31 unieqd ( ¬ 𝐴 ∈ ( V × V ) → ran { 𝐴 } = ∅ )
33 uni0 ∅ = ∅
34 32 33 eqtrdi ( ¬ 𝐴 ∈ ( V × V ) → ran { 𝐴 } = ∅ )
35 28 34 eqtr4d ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ran { 𝐴 } )
36 2ndval ( 2nd𝐴 ) = ran { 𝐴 }
37 35 36 eqtr4di ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd𝐴 ) )
38 16 37 pm2.61i ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd𝐴 )