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 e. Word (/) <-> W = (/) )

Proof

Step Hyp Ref Expression
1 wrdf
 |-  ( W e. Word (/) -> W : ( 0 ..^ ( # ` W ) ) --> (/) )
2 f00
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> (/) <-> ( W = (/) /\ ( 0 ..^ ( # ` W ) ) = (/) ) )
3 2 simplbi
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> (/) -> W = (/) )
4 1 3 syl
 |-  ( W e. Word (/) -> W = (/) )
5 wrd0
 |-  (/) e. Word (/)
6 eleq1
 |-  ( W = (/) -> ( W e. Word (/) <-> (/) e. Word (/) ) )
7 5 6 mpbiri
 |-  ( W = (/) -> W e. Word (/) )
8 4 7 impbii
 |-  ( W e. Word (/) <-> W = (/) )