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	syl5eq	|- ( ( A e. S /\ B e. S /\ C e. S ) -> <" A B C "> = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )