Theorem dmpropg

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

	Ref	Expression
Assertion	dmpropg	$$⊢\left(B\in V\wedge D\in W\right)\to \mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{A,C\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmsnopg	$$⊢B\in V\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$
2		dmsnopg	$$⊢D\in W\to \mathrm{dom}\left\{⟨C,D⟩\right\}=\left\{C\right\}$$
3		uneq12	$$⊢\left(\mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}\wedge \mathrm{dom}\left\{⟨C,D⟩\right\}=\left\{C\right\}\right)\to \mathrm{dom}\left\{⟨A,B⟩\right\}\cup \mathrm{dom}\left\{⟨C,D⟩\right\}=\left\{A\right\}\cup \left\{C\right\}$$
4	1 2 3	syl2an	$$⊢\left(B\in V\wedge D\in W\right)\to \mathrm{dom}\left\{⟨A,B⟩\right\}\cup \mathrm{dom}\left\{⟨C,D⟩\right\}=\left\{A\right\}\cup \left\{C\right\}$$
5		df-pr	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}$$
6	5	dmeqi	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}=\mathrm{dom}\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)$$
7		dmun	$$⊢\mathrm{dom}\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)=\mathrm{dom}\left\{⟨A,B⟩\right\}\cup \mathrm{dom}\left\{⟨C,D⟩\right\}$$
8	6 7	eqtri	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}=\mathrm{dom}\left\{⟨A,B⟩\right\}\cup \mathrm{dom}\left\{⟨C,D⟩\right\}$$
9		df-pr	$$⊢\left\{A,C\right\}=\left\{A\right\}\cup \left\{C\right\}$$
10	4 8 9	3eqtr4g	$$⊢\left(B\in V\wedge D\in W\right)\to \mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{A,C\right\}$$