Description: An element of the base set of a free monoid is a string on the generators. (Contributed by Mario Carneiro, 27-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frmdbas.m | |- M = ( freeMnd ` I ) |
|
frmdbas.b | |- B = ( Base ` M ) |
||
Assertion | frmdelbas | |- ( X e. B -> X e. Word I ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frmdbas.m | |- M = ( freeMnd ` I ) |
|
2 | frmdbas.b | |- B = ( Base ` M ) |
|
3 | id | |- ( X e. B -> X e. B ) |
|
4 | 1 2 | elbasfv | |- ( X e. B -> I e. _V ) |
5 | 1 2 | frmdbas | |- ( I e. _V -> B = Word I ) |
6 | 4 5 | syl | |- ( X e. B -> B = Word I ) |
7 | 3 6 | eleqtrd | |- ( X e. B -> X e. Word I ) |