Theorem s3tpop

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

	Ref	Expression
Assertion	s3tpop	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		df-s3	⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ )
2		s2cl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑆 )
3		cats1un	⊢ ( ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ ) = ( ⟨“ 𝐴 𝐵 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) )
4	2 3	stoic3	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ ) = ( ⟨“ 𝐴 𝐵 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) )
5		s2prop	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
6	5	3adant3	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
7		s2len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 2
8	7	opeq1i	⊢ ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ = ⟨ 2 , 𝐶 ⟩
9	8	sneqi	⊢ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } = { ⟨ 2 , 𝐶 ⟩ }
10	9	a1i	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } = { ⟨ 2 , 𝐶 ⟩ } )
11	6 10	uneq12d	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( ⟨“ 𝐴 𝐵 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) , 𝐶 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ } ) )
12		df-tp	⊢ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ } )
13	12	eqcomi	⊢ ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ } ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ }
14	13	a1i	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ } ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } )
15	4 11 14	3eqtrd	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } )
16	1 15	eqtrid	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } )