Metamath Proof Explorer

Theorem wwlksnextproplem1

Description: Lemma 1 for wwlksnextprop . (Contributed by Alexander van der Vekens, 31-Jul-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypothesis wwlksnextprop.x ⊢X=N+1WWalksNG
Assertion wwlksnextproplem1 ⊢W∈X∧N∈ℕ0→WprefixN+1⁡0=W⁡0

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢X=N+1WWalksNG
2 wwlknbp1 ⊢W∈N+1WWalksNG→N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1
3 simpl2 ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W∈WordVtx⁡G
4 peano2nn0 ⊢N+1∈ℕ0→N+1+1∈ℕ0
5 4 3ad2ant1 ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→N+1+1∈ℕ0
6 eleq1 ⊢W=N+1+1→W∈ℕ0↔N+1+1∈ℕ0
7 6 3ad2ant3 ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→W∈ℕ0↔N+1+1∈ℕ0
8 5 7 mpbird ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→W∈ℕ0
9 8 adantr ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W∈ℕ0
10 simpr ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N∈ℕ0
11 nn0re ⊢N+1∈ℕ0→N+1∈ℝ
12 11 lep1d ⊢N+1∈ℕ0→N+1≤N+1+1
13 12 3ad2ant1 ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→N+1≤N+1+1
14 breq2 ⊢W=N+1+1→N+1≤W↔N+1≤N+1+1
15 14 3ad2ant3 ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→N+1≤W↔N+1≤N+1+1
16 13 15 mpbird ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→N+1≤W
17 16 adantr ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1≤W
18 nn0p1elfzo ⊢N∈ℕ0∧W∈ℕ0∧N+1≤W→N∈0..^W
19 10 9 17 18 syl3anc ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N∈0..^W
20 fz0add1fz1 ⊢W∈ℕ0∧N∈0..^W→N+1∈1…W
21 9 19 20 syl2anc ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1∈1…W
22 3 21 jca ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W∈WordVtx⁡G∧N+1∈1…W
23 22 ex ⊢N+1∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→N∈ℕ0→W∈WordVtx⁡G∧N+1∈1…W
24 2 23 syl ⊢W∈N+1WWalksNG→N∈ℕ0→W∈WordVtx⁡G∧N+1∈1…W
25 24 1 eleq2s ⊢W∈X→N∈ℕ0→W∈WordVtx⁡G∧N+1∈1…W
26 25 imp ⊢W∈X∧N∈ℕ0→W∈WordVtx⁡G∧N+1∈1…W
27 pfxfv0 ⊢W∈WordVtx⁡G∧N+1∈1…W→WprefixN+1⁡0=W⁡0
28 26 27 syl ⊢W∈X∧N∈ℕ0→WprefixN+1⁡0=W⁡0