Theorem dmtpop

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

	Ref	Expression
Hypotheses	dmsnop.1	|- B e. _V
	dmprop.1	|- D e. _V
	dmtpop.1	|- F e. _V
Assertion	dmtpop	|- dom { <. A , B >. , <. C , D >. , <. E , F >. } = { A , C , E }

Proof

Step	Hyp	Ref	Expression
1		dmsnop.1	|- B e. _V
2		dmprop.1	|- D e. _V
3		dmtpop.1	|- F e. _V
4		df-tp	|- { <. A , B >. , <. C , D >. , <. E , F >. } = ( { <. A , B >. , <. C , D >. } u. { <. E , F >. } )
5	4	dmeqi	|- dom { <. A , B >. , <. C , D >. , <. E , F >. } = dom ( { <. A , B >. , <. C , D >. } u. { <. E , F >. } )
6		dmun	|- dom ( { <. A , B >. , <. C , D >. } u. { <. E , F >. } ) = ( dom { <. A , B >. , <. C , D >. } u. 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 >. } u. dom { <. E , F >. } ) = ( { A , C } u. { E } )
10	5 6 9	3eqtri	|- dom { <. A , B >. , <. C , D >. , <. E , F >. } = ( { A , C } u. { E } )
11		df-tp	|- { A , C , E } = ( { A , C } u. { E } )
12	10 11	eqtr4i	|- dom { <. A , B >. , <. C , D >. , <. E , F >. } = { A , C , E }