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

Metamath Proof Explorer

Theorem s2prop

Description: A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017)

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

Proof

Step Hyp Ref Expression
1 df-s2 ⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )
2 s1cl ⊢ ( 𝐴 ∈ 𝑆 → ⟨“ 𝐴 ”⟩ ∈ Word 𝑆 )
3 cats1un ⊢ ( ( ⟨“ 𝐴 ”⟩ ∈ Word 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) = ( ⟨“ 𝐴 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) )
4 2 3 sylan ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) = ( ⟨“ 𝐴 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) )
5 s1val ⊢ ( 𝐴 ∈ 𝑆 → ⟨“ 𝐴 ”⟩ = { ⟨ 0 , 𝐴 ⟩ } )
6 5 adantr ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 ”⟩ = { ⟨ 0 , 𝐴 ⟩ } )
7 6 uneq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨“ 𝐴 ”⟩ ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) )
8 df-pr ⊢ { ⟨ 0 , 𝐴 ⟩ , ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } = ( { ⟨ 0 , 𝐴 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } )
9 s1len ⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1
10 9 a1i ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1 )
11 10 opeq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ = ⟨ 1 , 𝐵 ⟩ )
12 11 preq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
13 8 12 eqtr3id ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( { ⟨ 0 , 𝐴 ⟩ } ∪ { ⟨ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) , 𝐵 ⟩ } ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
14 4 7 13 3eqtrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
15 1 14 eqtrid ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )