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 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } = { 𝐴 , 𝐶 , 𝐸 }