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:XY
s2co.2 φAX
s2co.3 φBX
Assertion s2co φF⟨“AB”⟩=⟨“FAFB”⟩

Proof

Step Hyp Ref Expression
1 s2co.1 φF:XY
2 s2co.2 φAX
3 s2co.3 φBX
4 df-s2 ⟨“AB”⟩=⟨“A”⟩++⟨“B”⟩
5 2 s1cld φ⟨“A”⟩WordX
6 s1co AXF:XYF⟨“A”⟩=⟨“FA”⟩
7 2 1 6 syl2anc φF⟨“A”⟩=⟨“FA”⟩
8 df-s2 ⟨“FAFB”⟩=⟨“FA”⟩++⟨“FB”⟩
9 4 5 3 1 7 8 cats1co φF⟨“AB”⟩=⟨“FAFB”⟩