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	syl5eq	|- ( ( ( 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 } ) ) )