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

Metamath Proof Explorer

Theorem 0wrd0

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

Ref Expression
Assertion 0wrd0 ⊢ W ∈ Word ∅ ↔ W = ∅

Proof

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