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 ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ = { ⟨ 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 , 𝐶 ⟩ } )