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

Metamath Proof Explorer

Theorem dmpropg

Description: The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion dmpropg ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐴 , 𝐶 } )

Proof

Step Hyp Ref Expression
1 dmsnopg ⊢ ( 𝐵 ∈ 𝑉 → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )
2 dmsnopg ⊢ ( 𝐷 ∈ 𝑊 → dom { ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐶 } )
3 uneq12 ⊢ ( ( dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } ∧ dom { ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐶 } ) → ( dom { ⟨ 𝐴 , 𝐵 ⟩ } ∪ dom { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( { 𝐴 } ∪ { 𝐶 } ) )
4 1 2 3 syl2an ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ( dom { ⟨ 𝐴 , 𝐵 ⟩ } ∪ dom { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( { 𝐴 } ∪ { 𝐶 } ) )
5 df-pr ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
6 5 dmeqi ⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
7 dmun ⊢ dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( dom { ⟨ 𝐴 , 𝐵 ⟩ } ∪ dom { ⟨ 𝐶 , 𝐷 ⟩ } )
8 6 7 eqtri ⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( dom { ⟨ 𝐴 , 𝐵 ⟩ } ∪ dom { ⟨ 𝐶 , 𝐷 ⟩ } )
9 df-pr ⊢ { 𝐴 , 𝐶 } = ( { 𝐴 } ∪ { 𝐶 } )
10 4 8 9 3eqtr4g ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐴 , 𝐶 } )