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

Metamath Proof Explorer

Theorem s4dom

Description: The domain of a length 4 word is the union of two (disjunct) pairs. (Contributed by Alexander van der Vekens, 15-Aug-2017)

Ref Expression
Assertion s4dom 
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( E = <" A B C D "> -> dom E = ( { 0 , 1 } u. { 2 , 3 } ) ) )

Proof

Step Hyp Ref Expression
1 dmeq 
 |-  ( E = <" A B C D "> -> dom E = dom <" A B C D "> )
2 s4prop 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <" A B C D "> = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) )
3 2 dmeqd 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> dom <" A B C D "> = dom ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) )
4 dmun 
 |-  dom ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) = ( dom { <. 0 , A >. , <. 1 , B >. } u. dom { <. 2 , C >. , <. 3 , D >. } )
5 dmpropg 
 |-  ( ( A e. S /\ B e. S ) -> dom { <. 0 , A >. , <. 1 , B >. } = { 0 , 1 } )
6 5 adantr 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> dom { <. 0 , A >. , <. 1 , B >. } = { 0 , 1 } )
7 dmpropg 
 |-  ( ( C e. S /\ D e. S ) -> dom { <. 2 , C >. , <. 3 , D >. } = { 2 , 3 } )
8 7 adantl 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> dom { <. 2 , C >. , <. 3 , D >. } = { 2 , 3 } )
9 6 8 uneq12d 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( dom { <. 0 , A >. , <. 1 , B >. } u. dom { <. 2 , C >. , <. 3 , D >. } ) = ( { 0 , 1 } u. { 2 , 3 } ) )
10 4 9 eqtrid 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> dom ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) = ( { 0 , 1 } u. { 2 , 3 } ) )
11 3 10 eqtrd 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> dom <" A B C D "> = ( { 0 , 1 } u. { 2 , 3 } ) )
12 1 11 sylan9eqr 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ E = <" A B C D "> ) -> dom E = ( { 0 , 1 } u. { 2 , 3 } ) )
13 12 ex 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( E = <" A B C D "> -> dom E = ( { 0 , 1 } u. { 2 , 3 } ) ) )