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

Metamath Proof Explorer

Theorem wrd0

Description: The empty set is a word (theempty word, frequently denoted ε in this context). This corresponds to the definition in Section 9.1 of AhoHopUll p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 13-May-2020)

		Ref	Expression
	Assertion	wrd0	⊢ ∅ ∈ Word 𝑆

Proof

Step	Hyp	Ref	Expression
1		f0	⊢ ∅ : ∅ ⟶ 𝑆
2		iswrddm0	⊢ ( ∅ : ∅ ⟶ 𝑆 → ∅ ∈ Word 𝑆 )
3	1 2	ax-mp	⊢ ∅ ∈ Word 𝑆