This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }