Metamath Proof Explorer


Theorem frmdelbas

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 )

Proof

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 )