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 = (/) )