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

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 𝐼 )