This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 elvv ⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑤 ∃ 𝑣 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ )
2 fveq2 ⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ ⟨ 𝑤 , 𝑣 ⟩ ) )
3 df-ov ⊢ ( 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } 𝑣 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ ⟨ 𝑤 , 𝑣 ⟩ )
4 simpl ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑣 ) → 𝑥 = 𝑤 )
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 7 12 op1std ⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( 1st ‘ 𝐴 ) = 𝑤 )
14 11 13 eqtr4d ⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 ) )
15 14 exlimivv ⊢ ( ∃ 𝑤 ∃ 𝑣 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 ) )
16 1 15 sylbi ⊢ ( 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 ) )
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 dmsnn0 ⊢ ( 𝐴 ∈ ( V × V ) ↔ dom { 𝐴 } ≠ ∅ )
30 29 biimpri ⊢ ( dom { 𝐴 } ≠ ∅ → 𝐴 ∈ ( V × V ) )
31 30 necon1bi ⊢ ( ¬ 𝐴 ∈ ( V × V ) → dom { 𝐴 } = ∅ )
32 31 unieqd ⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ dom { 𝐴 } = ∪ ∅ )
33 uni0 ⊢ ∪ ∅ = ∅
34 32 33 eqtrdi ⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ dom { 𝐴 } = ∅ )
35 28 34 eqtr4d ⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ∪ dom { 𝐴 } )
36 1stval ⊢ ( 1st ‘ 𝐴 ) = ∪ dom { 𝐴 }
37 35 36 eqtr4di ⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 ) )
38 16 37 pm2.61i ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 )