Metamath Proof Explorer

Theorem s2prop

Description: A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017)

Ref Expression
Assertion s2prop 
|- ( ( A e. S /\ B e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )

Proof

Step Hyp Ref Expression
1 df-s2 
 |-  <" A B "> = ( <" A "> ++ <" B "> )
2 s1cl 
 |-  ( A e. S -> <" A "> e. Word S )
3 cats1un 
 |-  ( ( <" A "> e. Word S /\ B e. S ) -> ( <" A "> ++ <" B "> ) = ( <" A "> u. { <. ( # ` <" A "> ) , B >. } ) )
4 2 3 sylan 
 |-  ( ( A e. S /\ B e. S ) -> ( <" A "> ++ <" B "> ) = ( <" A "> u. { <. ( # ` <" A "> ) , B >. } ) )
5 s1val 
 |-  ( A e. S -> <" A "> = { <. 0 , A >. } )
6 5 adantr 
 |-  ( ( A e. S /\ B e. S ) -> <" A "> = { <. 0 , A >. } )
7 6 uneq1d 
 |-  ( ( A e. S /\ B e. S ) -> ( <" A "> u. { <. ( # ` <" A "> ) , B >. } ) = ( { <. 0 , A >. } u. { <. ( # ` <" A "> ) , B >. } ) )
8 df-pr 
 |-  { <. 0 , A >. , <. ( # ` <" A "> ) , B >. } = ( { <. 0 , A >. } u. { <. ( # ` <" A "> ) , B >. } )
9 s1len 
 |-  ( # ` <" A "> ) = 1
10 9 a1i 
 |-  ( ( A e. S /\ B e. S ) -> ( # ` <" A "> ) = 1 )
11 10 opeq1d 
 |-  ( ( A e. S /\ B e. S ) -> <. ( # ` <" A "> ) , B >. = <. 1 , B >. )
12 11 preq2d 
 |-  ( ( A e. S /\ B e. S ) -> { <. 0 , A >. , <. ( # ` <" A "> ) , B >. } = { <. 0 , A >. , <. 1 , B >. } )
13 8 12 eqtr3id 
 |-  ( ( A e. S /\ B e. S ) -> ( { <. 0 , A >. } u. { <. ( # ` <" A "> ) , B >. } ) = { <. 0 , A >. , <. 1 , B >. } )
14 4 7 13 3eqtrd 
 |-  ( ( A e. S /\ B e. S ) -> ( <" A "> ++ <" B "> ) = { <. 0 , A >. , <. 1 , B >. } )
15 1 14 syl5eq 
 |-  ( ( A e. S /\ B e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )