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 + 1 WWalksN G
Assertion wwlksnextproplem1 ⊢ W ∈ X ∧ N ∈ ℕ 0 → W prefix N + 1 ⁡ 0 = W ⁡ 0

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢ X = N + 1 WWalksN G
2 wwlknbp1 ⊢ W ∈ N + 1 WWalksN G → N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1
3 simpl2 ⊢ N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G
4 peano2nn0 ⊢ N + 1 ∈ ℕ 0 → N + 1 + 1 ∈ ℕ 0
5 4 3ad2ant1 ⊢ N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → W ∈ ℕ 0 ↔ N + 1 + 1 ∈ ℕ 0
8 5 7 mpbird ⊢ N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → W ∈ ℕ 0
9 8 adantr ⊢ N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ∈ ℕ 0
10 simpr ⊢ N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → N + 1 ≤ W ↔ N + 1 ≤ N + 1 + 1
16 13 15 mpbird ⊢ N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → N + 1 ≤ W
17 16 adantr ⊢ N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 ∈ 1 … W
22 3 21 jca ⊢ N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W
23 22 ex ⊢ N + 1 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W
24 2 23 syl ⊢ W ∈ N + 1 WWalksN G → N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W
25 24 1 eleq2s ⊢ W ∈ X → N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W
26 25 imp ⊢ W ∈ X ∧ N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W
27 pfxfv0 ⊢ W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W → W prefix N + 1 ⁡ 0 = W ⁡ 0
28 26 27 syl ⊢ W ∈ X ∧ N ∈ ℕ 0 → W prefix N + 1 ⁡ 0 = W ⁡ 0