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 𝑀 = ( freeMnd ‘ 𝐼 )
frmdbas.b 𝐵 = ( Base ‘ 𝑀 )
Assertion frmdelbas ( 𝑋𝐵𝑋 ∈ Word 𝐼 )

Proof

Step Hyp Ref Expression
1 frmdbas.m 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdbas.b 𝐵 = ( Base ‘ 𝑀 )
3 id ( 𝑋𝐵𝑋𝐵 )
4 1 2 elbasfv ( 𝑋𝐵𝐼 ∈ V )
5 1 2 frmdbas ( 𝐼 ∈ V → 𝐵 = Word 𝐼 )
6 4 5 syl ( 𝑋𝐵𝐵 = Word 𝐼 )
7 3 6 eleqtrd ( 𝑋𝐵𝑋 ∈ Word 𝐼 )