This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 >. } )