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