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

Theorem frmdsssubm 16243
 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 12511 . . . 4 Word Word
21adantl 464 . . 3 Word Word
3 frmdmnd.m . . . . 5 freeMnd
4 eqid 2400 . . . . 5
53, 4frmdbas 16234 . . . 4 Word
65adantr 463 . . 3 Word
72, 6sseqtr4d 3476 . 2 Word
8 wrd0 12523 . . 3 Word
98a1i 11 . 2 Word
107sselda 3439 . . . . . 6 Word
117sselda 3439 . . . . . 6 Word
1210, 11anim12dan 836 . . . . 5 Word Word
13 eqid 2400 . . . . . 6
143, 4, 13frmdadd 16237 . . . . 5 ++
1512, 14syl 17 . . . 4 Word Word ++
16 ccatcl 12552 . . . . 5 Word Word ++ Word
1716adantl 464 . . . 4 Word Word ++ Word
1815, 17eqeltrd 2488 . . 3 Word Word Word
1918ralrimivva 2822 . 2 Word Word Word
203frmdmnd 16241 . . . 4