Metamath Proof Explorer


Theorem s3tpop

Description: A length 3 word is an unordered triple of ordered pairs. (Contributed by AV, 23-Jan-2021)

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

Proof

Step Hyp Ref Expression
1 df-s3
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
2 s2cl
 |-  ( ( A e. S /\ B e. S ) -> <" A B "> e. Word S )
3 cats1un
 |-  ( ( <" A B "> e. Word S /\ C e. S ) -> ( <" A B "> ++ <" C "> ) = ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) )
4 2 3 stoic3
 |-  ( ( A e. S /\ B e. S /\ C e. S ) -> ( <" A B "> ++ <" C "> ) = ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) )
5 s2prop
 |-  ( ( A e. S /\ B e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
6 5 3adant3
 |-  ( ( A e. S /\ B e. S /\ C e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
7 s2len
 |-  ( # ` <" A B "> ) = 2
8 7 opeq1i
 |-  <. ( # ` <" A B "> ) , C >. = <. 2 , C >.
9 8 sneqi
 |-  { <. ( # ` <" A B "> ) , C >. } = { <. 2 , C >. }
10 9 a1i
 |-  ( ( A e. S /\ B e. S /\ C e. S ) -> { <. ( # ` <" A B "> ) , C >. } = { <. 2 , C >. } )
11 6 10 uneq12d
 |-  ( ( A e. S /\ B e. S /\ C e. S ) -> ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. } ) )
12 df-tp
 |-  { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. } )
13 12 eqcomi
 |-  ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. } ) = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. }
14 13 a1i
 |-  ( ( A e. S /\ B e. S /\ C e. S ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. } ) = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )
15 4 11 14 3eqtrd
 |-  ( ( A e. S /\ B e. S /\ C e. S ) -> ( <" A B "> ++ <" C "> ) = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )
16 1 15 eqtrid
 |-  ( ( A e. S /\ B e. S /\ C e. S ) -> <" A B C "> = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )