dmtpop

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

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

Metamath Proof Explorer