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