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

Metamath Proof Explorer

Theorem 1stval

Description: The value of the function that extracts the first member of an ordered pair. (Contributed by NM, 9-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion 1stval ( 1st ‘ 𝐴 ) = ∪ dom { 𝐴 }

Proof

Step Hyp Ref Expression
1 sneq ⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
2 1 dmeqd ⊢ ( 𝑥 = 𝐴 → dom { 𝑥 } = dom { 𝐴 } )
3 2 unieqd ⊢ ( 𝑥 = 𝐴 → ∪ dom { 𝑥 } = ∪ dom { 𝐴 } )
4 df-1st ⊢ 1st = ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } )
5 snex ⊢ { 𝐴 } ∈ V
6 5 dmex ⊢ dom { 𝐴 } ∈ V
7 6 uniex ⊢ ∪ dom { 𝐴 } ∈ V
8 3 4 7 fvmpt ⊢ ( 𝐴 ∈ V → ( 1st ‘ 𝐴 ) = ∪ dom { 𝐴 } )
9 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( 1st ‘ 𝐴 ) = ∅ )
10 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
11 10 biimpi ⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
12 11 dmeqd ⊢ ( ¬ 𝐴 ∈ V → dom { 𝐴 } = dom ∅ )
13 dm0 ⊢ dom ∅ = ∅
14 12 13 eqtrdi ⊢ ( ¬ 𝐴 ∈ V → dom { 𝐴 } = ∅ )
15 14 unieqd ⊢ ( ¬ 𝐴 ∈ V → ∪ dom { 𝐴 } = ∪ ∅ )
16 uni0 ⊢ ∪ ∅ = ∅
17 15 16 eqtrdi ⊢ ( ¬ 𝐴 ∈ V → ∪ dom { 𝐴 } = ∅ )
18 9 17 eqtr4d ⊢ ( ¬ 𝐴 ∈ V → ( 1st ‘ 𝐴 ) = ∪ dom { 𝐴 } )
19 8 18 pm2.61i ⊢ ( 1st ‘ 𝐴 ) = ∪ dom { 𝐴 }