Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  frmdsssubm Structured version   Unicode version

Theorem frmdsssubm 14806
 Description: The set of words taking values in a subset is a (free) submonoid of the free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
Hypothesis
Ref Expression
frmdmnd.m freeMnd
Assertion
Ref Expression
frmdsssubm Word SubMnd

Proof of Theorem frmdsssubm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sswrd 11737 . . . 4 Word Word
21adantl 453 . . 3 Word Word
3 frmdmnd.m . . . . 5 freeMnd
4 eqid 2436 . . . . 5
53, 4frmdbas 14797 . . . 4 Word
65adantr 452 . . 3 Word
72, 6sseqtr4d 3385 . 2 Word
8 wrd0 11732 . . 3 Word
98a1i 11 . 2 Word
107sselda 3348 . . . . . 6 Word
117sselda 3348 . . . . . 6 Word
1210, 11anim12dan 811 . . . . 5 Word Word
13 eqid 2436 . . . . . 6
143, 4, 13frmdadd 14800 . . . . 5 concat
1512, 14syl 16 . . . 4 Word Word concat
16 ccatcl 11743 . . . . 5 Word Word concat Word
1716adantl 453 . . . 4 Word Word concat Word
1815, 17eqeltrd 2510 . . 3 Word Word Word
1918ralrimivva 2798 . 2 Word Word Word
203frmdmnd 14804 . . . 4