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

Metamath Proof Explorer

Theorem s2co

Description: Mapping a doubleton word by a function. (Contributed by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses s2co.1 ⊢ φ → F : X ⟶ Y
s2co.2 ⊢ φ → A ∈ X
s2co.3 ⊢ φ → B ∈ X
Assertion s2co ⊢ φ → F ∘ ⟨“ AB ”⟩ = ⟨“ F ⁡ A F ⁡ B ”⟩

Proof

Step Hyp Ref Expression
1 s2co.1 ⊢ φ → F : X ⟶ Y
2 s2co.2 ⊢ φ → A ∈ X
3 s2co.3 ⊢ φ → B ∈ X
4 df-s2 ⊢ ⟨“ AB ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩
5 2 s1cld ⊢ φ → ⟨“ A ”⟩ ∈ Word X
6 s1co ⊢ A ∈ X ∧ F : X ⟶ Y → F ∘ ⟨“ A ”⟩ = ⟨“ F ⁡ A ”⟩
7 2 1 6 syl2anc ⊢ φ → F ∘ ⟨“ A ”⟩ = ⟨“ F ⁡ A ”⟩
8 df-s2 ⊢ ⟨“ F ⁡ A F ⁡ B ”⟩ = ⟨“ F ⁡ A ”⟩ ++ ⟨“ F ⁡ B ”⟩
9 4 5 3 1 7 8 cats1co ⊢ φ → F ∘ ⟨“ AB ”⟩ = ⟨“ F ⁡ A F ⁡ B ”⟩