Theorem dmtpop

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

	Ref	Expression
Hypotheses	dmsnop.1	$$⊢B\in \mathrm{V}$$
	dmprop.1	$$⊢D\in \mathrm{V}$$
	dmtpop.1	$$⊢F\in \mathrm{V}$$
Assertion	dmtpop	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩,⟨E,F⟩\right\}=\left\{A,C,E\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmsnop.1	$$⊢B\in \mathrm{V}$$
2		dmprop.1	$$⊢D\in \mathrm{V}$$
3		dmtpop.1	$$⊢F\in \mathrm{V}$$
4		df-tp	$$⊢\left\{⟨A,B⟩,⟨C,D⟩,⟨E,F⟩\right\}=\left\{⟨A,B⟩,⟨C,D⟩\right\}\cup \left\{⟨E,F⟩\right\}$$
5	4	dmeqi	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩,⟨E,F⟩\right\}=\mathrm{dom}\left(\left\{⟨A,B⟩,⟨C,D⟩\right\}\cup \left\{⟨E,F⟩\right\}\right)$$
6		dmun	$$⊢\mathrm{dom}\left(\left\{⟨A,B⟩,⟨C,D⟩\right\}\cup \left\{⟨E,F⟩\right\}\right)=\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}\cup \mathrm{dom}\left\{⟨E,F⟩\right\}$$
7	1 2	dmprop	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{A,C\right\}$$
8	3	dmsnop	$$⊢\mathrm{dom}\left\{⟨E,F⟩\right\}=\left\{E\right\}$$
9	7 8	uneq12i	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}\cup \mathrm{dom}\left\{⟨E,F⟩\right\}=\left\{A,C\right\}\cup \left\{E\right\}$$
10	5 6 9	3eqtri	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩,⟨E,F⟩\right\}=\left\{A,C\right\}\cup \left\{E\right\}$$
11		df-tp	$$⊢\left\{A,C,E\right\}=\left\{A,C\right\}\cup \left\{E\right\}$$
12	10 11	eqtr4i	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩,⟨E,F⟩\right\}=\left\{A,C,E\right\}$$