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

Metamath Proof Explorer

Theorem frmdsssubm

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)

Ref Expression
Hypothesis frmdmnd.m 
|- M = ( freeMnd ` I )
Assertion frmdsssubm 
|- ( ( I e. V /\ J C_ I ) -> Word J e. ( SubMnd ` M ) )

Proof

Step Hyp Ref Expression
1 frmdmnd.m 
 |-  M = ( freeMnd ` I )
2 sswrd 
 |-  ( J C_ I -> Word J C_ Word I )
3 2 adantl 
 |-  ( ( I e. V /\ J C_ I ) -> Word J C_ Word I )
4 eqid 
 |-  ( Base ` M ) = ( Base ` M )
5 1 4 frmdbas 
 |-  ( I e. V -> ( Base ` M ) = Word I )
6 5 adantr 
 |-  ( ( I e. V /\ J C_ I ) -> ( Base ` M ) = Word I )
7 3 6 sseqtrrd 
 |-  ( ( I e. V /\ J C_ I ) -> Word J C_ ( Base ` M ) )
8 wrd0 
 |-  (/) e. Word J
9 8 a1i 
 |-  ( ( I e. V /\ J C_ I ) -> (/) e. Word J )
10 7 sselda 
 |-  ( ( ( I e. V /\ J C_ I ) /\ x e. Word J ) -> x e. ( Base ` M ) )
11 7 sselda 
 |-  ( ( ( I e. V /\ J C_ I ) /\ y e. Word J ) -> y e. ( Base ` M ) )
12 10 11 anim12dan 
 |-  ( ( ( I e. V /\ J C_ I ) /\ ( x e. Word J /\ y e. Word J ) ) -> ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) )
13 eqid 
 |-  ( +g ` M ) = ( +g ` M )
14 1 4 13 frmdadd 
 |-  ( ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( x ( +g ` M ) y ) = ( x ++ y ) )
15 12 14 syl 
 |-  ( ( ( I e. V /\ J C_ I ) /\ ( x e. Word J /\ y e. Word J ) ) -> ( x ( +g ` M ) y ) = ( x ++ y ) )
16 ccatcl 
 |-  ( ( x e. Word J /\ y e. Word J ) -> ( x ++ y ) e. Word J )
17 16 adantl 
 |-  ( ( ( I e. V /\ J C_ I ) /\ ( x e. Word J /\ y e. Word J ) ) -> ( x ++ y ) e. Word J )
18 15 17 eqeltrd 
 |-  ( ( ( I e. V /\ J C_ I ) /\ ( x e. Word J /\ y e. Word J ) ) -> ( x ( +g ` M ) y ) e. Word J )
19 18 ralrimivva 
 |-  ( ( I e. V /\ J C_ I ) -> A. x e. Word J A. y e. Word J ( x ( +g ` M ) y ) e. Word J )
20 1 frmdmnd 
 |-  ( I e. V -> M e. Mnd )
21 20 adantr 
 |-  ( ( I e. V /\ J C_ I ) -> M e. Mnd )
22 1 frmd0 
 |-  (/) = ( 0g ` M )
23 4 22 13 issubm 
 |-  ( M e. Mnd -> ( Word J e. ( SubMnd ` M ) <-> ( Word J C_ ( Base ` M ) /\ (/) e. Word J /\ A. x e. Word J A. y e. Word J ( x ( +g ` M ) y ) e. Word J ) ) )
24 21 23 syl 
 |-  ( ( I e. V /\ J C_ I ) -> ( Word J e. ( SubMnd ` M ) <-> ( Word J C_ ( Base ` M ) /\ (/) e. Word J /\ A. x e. Word J A. y e. Word J ( x ( +g ` M ) y ) e. Word J ) ) )
25 7 9 19 24 mpbir3and 
 |-  ( ( I e. V /\ J C_ I ) -> Word J e. ( SubMnd ` M ) )