Metamath Proof Explorer
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 𝐼 ) |