Metamath Proof Explorer

Theorem s4prop

Description: A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017)

Ref Expression
Assertion 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 >. } ) )

Proof

Step Hyp Ref Expression
1 df-s4 
 |-  <" A B C D "> = ( <" A B C "> ++ <" D "> )
2 simpl 
 |-  ( ( A e. S /\ B e. S ) -> A e. S )
3 2 adantr 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> A e. S )
4 simpr 
 |-  ( ( A e. S /\ B e. S ) -> B e. S )
5 4 adantr 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> B e. S )
6 simpl 
 |-  ( ( C e. S /\ D e. S ) -> C e. S )
7 6 adantl 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> C e. S )
8 3 5 7 s3cld 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <" A B C "> e. Word S )
9 simpr 
 |-  ( ( C e. S /\ D e. S ) -> D e. S )
10 9 adantl 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> D e. S )
11 cats1un 
 |-  ( ( <" A B C "> e. Word S /\ D e. S ) -> ( <" A B C "> ++ <" D "> ) = ( <" A B C "> u. { <. ( # ` <" A B C "> ) , D >. } ) )
12 8 10 11 syl2anc 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <" A B C "> ++ <" D "> ) = ( <" A B C "> u. { <. ( # ` <" A B C "> ) , D >. } ) )
13 df-s3 
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
14 s2cl 
 |-  ( ( A e. S /\ B e. S ) -> <" A B "> e. Word S )
15 14 adantr 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <" A B "> e. Word S )
16 cats1un 
 |-  ( ( <" A B "> e. Word S /\ C e. S ) -> ( <" A B "> ++ <" C "> ) = ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) )
17 15 7 16 syl2anc 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <" A B "> ++ <" C "> ) = ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) )
18 13 17 syl5eq 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <" A B C "> = ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) )
19 s2prop 
 |-  ( ( A e. S /\ B e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
20 19 adantr 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
21 20 uneq1d 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) = ( { <. 0 , A >. , <. 1 , B >. } u. { <. ( # ` <" A B "> ) , C >. } ) )
22 18 21 eqtrd 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <" A B C "> = ( { <. 0 , A >. , <. 1 , B >. } u. { <. ( # ` <" A B "> ) , C >. } ) )
23 22 uneq1d 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <" A B C "> u. { <. ( # ` <" A B C "> ) , D >. } ) = ( ( { <. 0 , A >. , <. 1 , B >. } u. { <. ( # ` <" A B "> ) , C >. } ) u. { <. ( # ` <" A B C "> ) , D >. } ) )
24 12 23 eqtrd 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <" A B C "> ++ <" D "> ) = ( ( { <. 0 , A >. , <. 1 , B >. } u. { <. ( # ` <" A B "> ) , C >. } ) u. { <. ( # ` <" A B C "> ) , D >. } ) )
25 unass 
 |-  ( ( { <. 0 , A >. , <. 1 , B >. } u. { <. ( # ` <" A B "> ) , C >. } ) u. { <. ( # ` <" A B C "> ) , D >. } ) = ( { <. 0 , A >. , <. 1 , B >. } u. ( { <. ( # ` <" A B "> ) , C >. } u. { <. ( # ` <" A B C "> ) , D >. } ) )
26 25 a1i 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( ( { <. 0 , A >. , <. 1 , B >. } u. { <. ( # ` <" A B "> ) , C >. } ) u. { <. ( # ` <" A B C "> ) , D >. } ) = ( { <. 0 , A >. , <. 1 , B >. } u. ( { <. ( # ` <" A B "> ) , C >. } u. { <. ( # ` <" A B C "> ) , D >. } ) ) )
27 df-pr 
 |-  { <. ( # ` <" A B "> ) , C >. , <. ( # ` <" A B C "> ) , D >. } = ( { <. ( # ` <" A B "> ) , C >. } u. { <. ( # ` <" A B C "> ) , D >. } )
28 s2len 
 |-  ( # ` <" A B "> ) = 2
29 28 a1i 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( # ` <" A B "> ) = 2 )
30 29 opeq1d 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <. ( # ` <" A B "> ) , C >. = <. 2 , C >. )
31 s3len 
 |-  ( # ` <" A B C "> ) = 3
32 31 a1i 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( # ` <" A B C "> ) = 3 )
33 32 opeq1d 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <. ( # ` <" A B C "> ) , D >. = <. 3 , D >. )
34 30 33 preq12d 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> { <. ( # ` <" A B "> ) , C >. , <. ( # ` <" A B C "> ) , D >. } = { <. 2 , C >. , <. 3 , D >. } )
35 27 34 syl5eqr 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( { <. ( # ` <" A B "> ) , C >. } u. { <. ( # ` <" A B C "> ) , D >. } ) = { <. 2 , C >. , <. 3 , D >. } )
36 35 uneq2d 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. ( { <. ( # ` <" A B "> ) , C >. } u. { <. ( # ` <" A B C "> ) , D >. } ) ) = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) )
37 24 26 36 3eqtrd 
 |-  ( ( ( 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 >. } ) )
38 1 37 syl5eq 
 |-  ( ( ( 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 >. } ) )