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

Metamath Proof Explorer

Theorem dmtpop

Description: The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011)

Ref Expression
Hypotheses dmsnop.1 ⊢ 𝐵 ∈ V
dmprop.1 ⊢ 𝐷 ∈ V
dmtpop.1 ⊢ 𝐹 ∈ V
Assertion dmtpop dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } = { 𝐴 , 𝐶 , 𝐸 }

Proof

Step Hyp Ref Expression
1 dmsnop.1 ⊢ 𝐵 ∈ V
2 dmprop.1 ⊢ 𝐷 ∈ V
3 dmtpop.1 ⊢ 𝐹 ∈ V
4 df-tp ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ } )
5 4 dmeqi ⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } = dom ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ } )
6 dmun ⊢ dom ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ { ⟨ 𝐸 , 𝐹 ⟩ } ) = ( dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ dom { ⟨ 𝐸 , 𝐹 ⟩ } )
7 1 2 dmprop ⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐴 , 𝐶 }
8 3 dmsnop ⊢ dom { ⟨ 𝐸 , 𝐹 ⟩ } = { 𝐸 }
9 7 8 uneq12i ⊢ ( dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∪ dom { ⟨ 𝐸 , 𝐹 ⟩ } ) = ( { 𝐴 , 𝐶 } ∪ { 𝐸 } )
10 5 6 9 3eqtri ⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } = ( { 𝐴 , 𝐶 } ∪ { 𝐸 } )
11 df-tp ⊢ { 𝐴 , 𝐶 , 𝐸 } = ( { 𝐴 , 𝐶 } ∪ { 𝐸 } )
12 10 11 eqtr4i ⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } = { 𝐴 , 𝐶 , 𝐸 }