Metamath Proof Explorer

Theorem wwlksnextproplem3

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

Ref Expression
Hypotheses wwlksnextprop.x ⊢ X = N + 1 WWalksN G
wwlksnextprop.e ⊢ E = Edg ⁡ G
wwlksnextprop.y ⊢ Y = w ∈ N WWalksN G | w ⁡ 0 = P
Assertion wwlksnextproplem3 ⊢ W ∈ X ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 ∈ Y

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢ X = N + 1 WWalksN G
2 wwlksnextprop.e ⊢ E = Edg ⁡ G
3 wwlksnextprop.y ⊢ Y = w ∈ N WWalksN G | w ⁡ 0 = P
4 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
5 iswwlksn ⊢ N + 1 ∈ ℕ 0 → W ∈ N + 1 WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1
6 4 5 syl ⊢ N ∈ ℕ 0 → W ∈ N + 1 WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1
7 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
8 7 wwlkbp ⊢ W ∈ WWalks ⁡ G → G ∈ V ∧ W ∈ Word Vtx ⁡ G
9 lencl ⊢ W ∈ Word Vtx ⁡ G → W ∈ ℕ 0
10 eqcom ⊢ W = N + 1 + 1 ↔ N + 1 + 1 = W
11 nn0cn ⊢ W ∈ ℕ 0 → W ∈ ℂ
12 11 adantr ⊢ W ∈ ℕ 0 ∧ N ∈ ℕ 0 → W ∈ ℂ
13 1cnd ⊢ W ∈ ℕ 0 ∧ N ∈ ℕ 0 → 1 ∈ ℂ
14 nn0cn ⊢ N + 1 ∈ ℕ 0 → N + 1 ∈ ℂ
15 4 14 syl ⊢ N ∈ ℕ 0 → N + 1 ∈ ℂ
16 15 adantl ⊢ W ∈ ℕ 0 ∧ N ∈ ℕ 0 → N + 1 ∈ ℂ
17 subadd2 ⊢ W ∈ ℂ ∧ 1 ∈ ℂ ∧ N + 1 ∈ ℂ → W − 1 = N + 1 ↔ N + 1 + 1 = W
18 17 bicomd ⊢ W ∈ ℂ ∧ 1 ∈ ℂ ∧ N + 1 ∈ ℂ → N + 1 + 1 = W ↔ W − 1 = N + 1
19 12 13 16 18 syl3anc ⊢ W ∈ ℕ 0 ∧ N ∈ ℕ 0 → N + 1 + 1 = W ↔ W − 1 = N + 1
20 10 19 bitrid ⊢ W ∈ ℕ 0 ∧ N ∈ ℕ 0 → W = N + 1 + 1 ↔ W − 1 = N + 1
21 eqcom ⊢ W − 1 = N + 1 ↔ N + 1 = W − 1
22 21 biimpi ⊢ W − 1 = N + 1 → N + 1 = W − 1
23 20 22 biimtrdi ⊢ W ∈ ℕ 0 ∧ N ∈ ℕ 0 → W = N + 1 + 1 → N + 1 = W − 1
24 23 ex ⊢ W ∈ ℕ 0 → N ∈ ℕ 0 → W = N + 1 + 1 → N + 1 = W − 1
25 24 com23 ⊢ W ∈ ℕ 0 → W = N + 1 + 1 → N ∈ ℕ 0 → N + 1 = W − 1
26 9 25 syl ⊢ W ∈ Word Vtx ⁡ G → W = N + 1 + 1 → N ∈ ℕ 0 → N + 1 = W − 1
27 8 26 simpl2im ⊢ W ∈ WWalks ⁡ G → W = N + 1 + 1 → N ∈ ℕ 0 → N + 1 = W − 1
28 27 imp31 ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 = W − 1
29 28 oveq2d ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W prefix N + 1 = W prefix W − 1
30 simpll ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ∈ WWalks ⁡ G
31 nn0ge0 ⊢ N ∈ ℕ 0 → 0 ≤ N
32 2re ⊢ 2 ∈ ℝ
33 32 a1i ⊢ N ∈ ℕ 0 → 2 ∈ ℝ
34 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
35 33 34 addge02d ⊢ N ∈ ℕ 0 → 0 ≤ N ↔ 2 ≤ N + 2
36 31 35 mpbid ⊢ N ∈ ℕ 0 → 2 ≤ N + 2
37 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
38 1cnd ⊢ N ∈ ℕ 0 → 1 ∈ ℂ
39 37 38 38 addassd ⊢ N ∈ ℕ 0 → N + 1 + 1 = N + 1 + 1
40 1p1e2 ⊢ 1 + 1 = 2
41 40 a1i ⊢ N ∈ ℕ 0 → 1 + 1 = 2
42 41 oveq2d ⊢ N ∈ ℕ 0 → N + 1 + 1 = N + 2
43 39 42 eqtrd ⊢ N ∈ ℕ 0 → N + 1 + 1 = N + 2
44 36 43 breqtrrd ⊢ N ∈ ℕ 0 → 2 ≤ N + 1 + 1
45 44 adantl ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → 2 ≤ N + 1 + 1
46 breq2 ⊢ W = N + 1 + 1 → 2 ≤ W ↔ 2 ≤ N + 1 + 1
47 46 ad2antlr ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → 2 ≤ W ↔ 2 ≤ N + 1 + 1
48 45 47 mpbird ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → 2 ≤ W
49 wwlksm1edg ⊢ W ∈ WWalks ⁡ G ∧ 2 ≤ W → W prefix W − 1 ∈ WWalks ⁡ G
50 30 48 49 syl2anc ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W prefix W − 1 ∈ WWalks ⁡ G
51 29 50 eqeltrd ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W prefix N + 1 ∈ WWalks ⁡ G
52 51 expcom ⊢ N ∈ ℕ 0 → W ∈ WWalks ⁡ G ∧ W = N + 1 + 1 → W prefix N + 1 ∈ WWalks ⁡ G
53 6 52 sylbid ⊢ N ∈ ℕ 0 → W ∈ N + 1 WWalksN G → W prefix N + 1 ∈ WWalks ⁡ G
54 53 com12 ⊢ W ∈ N + 1 WWalksN G → N ∈ ℕ 0 → W prefix N + 1 ∈ WWalks ⁡ G
55 54 adantr ⊢ W ∈ N + 1 WWalksN G ∧ W ⁡ 0 = P → N ∈ ℕ 0 → W prefix N + 1 ∈ WWalks ⁡ G
56 55 imp ⊢ W ∈ N + 1 WWalksN G ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 ∈ WWalks ⁡ G
57 7 2 wwlknp ⊢ W ∈ N + 1 WWalksN G → W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E
58 simpll ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G
59 peano2nn0 ⊢ N + 1 ∈ ℕ 0 → N + 1 + 1 ∈ ℕ 0
60 4 59 syl ⊢ N ∈ ℕ 0 → N + 1 + 1 ∈ ℕ 0
61 peano2re ⊢ N ∈ ℝ → N + 1 ∈ ℝ
62 34 61 syl ⊢ N ∈ ℕ 0 → N + 1 ∈ ℝ
63 62 lep1d ⊢ N ∈ ℕ 0 → N + 1 ≤ N + 1 + 1
64 elfz2nn0 ⊢ N + 1 ∈ 0 … N + 1 + 1 ↔ N + 1 ∈ ℕ 0 ∧ N + 1 + 1 ∈ ℕ 0 ∧ N + 1 ≤ N + 1 + 1
65 4 60 63 64 syl3anbrc ⊢ N ∈ ℕ 0 → N + 1 ∈ 0 … N + 1 + 1
66 65 adantl ⊢ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 ∈ 0 … N + 1 + 1
67 oveq2 ⊢ W = N + 1 + 1 → 0 … W = 0 … N + 1 + 1
68 67 adantr ⊢ W = N + 1 + 1 ∧ N ∈ ℕ 0 → 0 … W = 0 … N + 1 + 1
69 66 68 eleqtrrd ⊢ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 ∈ 0 … W
70 69 adantll ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 ∈ 0 … W
71 58 70 jca ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 0 … W
72 71 ex ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 0 … W
73 72 3adant3 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 0 … W
74 57 73 syl ⊢ W ∈ N + 1 WWalksN G → N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 0 … W
75 74 adantr ⊢ W ∈ N + 1 WWalksN G ∧ W ⁡ 0 = P → N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 0 … W
76 75 imp ⊢ W ∈ N + 1 WWalksN G ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 0 … W
77 pfxlen ⊢ W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 0 … W → W prefix N + 1 = N + 1
78 76 77 syl ⊢ W ∈ N + 1 WWalksN G ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 = N + 1
79 56 78 jca ⊢ W ∈ N + 1 WWalksN G ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 ∈ WWalks ⁡ G ∧ W prefix N + 1 = N + 1
80 iswwlksn ⊢ N ∈ ℕ 0 → W prefix N + 1 ∈ N WWalksN G ↔ W prefix N + 1 ∈ WWalks ⁡ G ∧ W prefix N + 1 = N + 1
81 80 adantl ⊢ W ∈ N + 1 WWalksN G ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 ∈ N WWalksN G ↔ W prefix N + 1 ∈ WWalks ⁡ G ∧ W prefix N + 1 = N + 1
82 79 81 mpbird ⊢ W ∈ N + 1 WWalksN G ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 ∈ N WWalksN G
83 82 exp31 ⊢ W ∈ N + 1 WWalksN G → W ⁡ 0 = P → N ∈ ℕ 0 → W prefix N + 1 ∈ N WWalksN G
84 83 1 eleq2s ⊢ W ∈ X → W ⁡ 0 = P → N ∈ ℕ 0 → W prefix N + 1 ∈ N WWalksN G
85 84 3imp ⊢ W ∈ X ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 ∈ N WWalksN G
86 1 wwlksnextproplem1 ⊢ W ∈ X ∧ N ∈ ℕ 0 → W prefix N + 1 ⁡ 0 = W ⁡ 0
87 86 3adant2 ⊢ W ∈ X ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 ⁡ 0 = W ⁡ 0
88 simp2 ⊢ W ∈ X ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W ⁡ 0 = P
89 87 88 eqtrd ⊢ W ∈ X ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 ⁡ 0 = P
90 fveq1 ⊢ w = W prefix N + 1 → w ⁡ 0 = W prefix N + 1 ⁡ 0
91 90 eqeq1d ⊢ w = W prefix N + 1 → w ⁡ 0 = P ↔ W prefix N + 1 ⁡ 0 = P
92 91 3 elrab2 ⊢ W prefix N + 1 ∈ Y ↔ W prefix N + 1 ∈ N WWalksN G ∧ W prefix N + 1 ⁡ 0 = P
93 85 89 92 sylanbrc ⊢ W ∈ X ∧ W ⁡ 0 = P ∧ N ∈ ℕ 0 → W prefix N + 1 ∈ Y