Metamath Proof Explorer


Theorem pfxn0

Description: A prefix consisting of at least one symbol is not empty. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 2-May-2020)

Ref Expression
Assertion pfxn0 WWordVLLWWprefixL

Proof

Step Hyp Ref Expression
1 lbfzo0 00..^LL
2 ne0i 00..^L0..^L
3 1 2 sylbir L0..^L
4 3 3ad2ant2 WWordVLLW0..^L
5 simp1 WWordVLLWWWordV
6 nnnn0 LL0
7 6 3ad2ant2 WWordVLLWL0
8 lencl WWordVW0
9 8 3ad2ant1 WWordVLLWW0
10 simp3 WWordVLLWLW
11 elfz2nn0 L0WL0W0LW
12 7 9 10 11 syl3anbrc WWordVLLWL0W
13 pfxf WWordVL0WWprefixL:0..^LV
14 5 12 13 syl2anc WWordVLLWWprefixL:0..^LV
15 f0dom0 WprefixL:0..^LV0..^L=WprefixL=
16 15 bicomd WprefixL:0..^LVWprefixL=0..^L=
17 14 16 syl WWordVLLWWprefixL=0..^L=
18 17 necon3bid WWordVLLWWprefixL0..^L
19 4 18 mpbird WWordVLLWWprefixL