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