Theorem 0wrd0

Description: The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018)

	Ref	Expression
Assertion	0wrd0	⊢ ( 𝑊 ∈ Word ∅ ↔ 𝑊 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		wrdf	⊢ ( 𝑊 ∈ Word ∅ → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ∅ )
2		f00	⊢ ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ∅ ↔ ( 𝑊 = ∅ ∧ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ∅ ) )
3	2	simplbi	⊢ ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ∅ → 𝑊 = ∅ )
4	1 3	syl	⊢ ( 𝑊 ∈ Word ∅ → 𝑊 = ∅ )
5		wrd0	⊢ ∅ ∈ Word ∅
6		eleq1	⊢ ( 𝑊 = ∅ → ( 𝑊 ∈ Word ∅ ↔ ∅ ∈ Word ∅ ) )
7	5 6	mpbiri	⊢ ( 𝑊 = ∅ → 𝑊 ∈ Word ∅ )
8	4 7	impbii	⊢ ( 𝑊 ∈ Word ∅ ↔ 𝑊 = ∅ )