Metamath Proof Explorer

Theorem clwwlknonex2

Description: Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 28-Mar-2022)

Ref Expression
Hypotheses clwwlknonex2.v ⊢ V = Vtx ⁡ G
clwwlknonex2.e ⊢ E = Edg ⁡ G
Assertion clwwlknonex2 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ X Y ∈ E ∧ W ∈ X ClWWalksNOn ⁡ G N − 2 → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ N ClWWalksN G

Proof

Step Hyp Ref Expression
1 clwwlknonex2.v ⊢ V = Vtx ⁡ G
2 clwwlknonex2.e ⊢ E = Edg ⁡ G
3 uz3m2nn ⊢ N ∈ ℤ ≥ 3 → N − 2 ∈ ℕ
4 3 nnne0d ⊢ N ∈ ℤ ≥ 3 → N − 2 ≠ 0
5 4 3ad2ant3 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 → N − 2 ≠ 0
6 1 2 clwwlknonel ⊢ N − 2 ≠ 0 → W ∈ X ClWWalksNOn ⁡ G N − 2 ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X
7 5 6 syl ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 → W ∈ X ClWWalksNOn ⁡ G N − 2 ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X
8 simpr11 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → W ∈ Word V
9 8 adantr ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ∈ Word V
10 simpll1 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → X ∈ V
11 simpll2 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → Y ∈ V
12 ccatw2s1cl ⊢ W ∈ Word V ∧ X ∈ V ∧ Y ∈ V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V
13 9 10 11 12 syl3anc ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V
14 1 2 clwwlknonex2lem2 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → ∀ i ∈ 0 ..^ W − 1 ∪ W − 1 W W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E
15 simp11 ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → W ∈ Word V
16 15 ad2antlr ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ∈ Word V
17 ccatw2s1len ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
18 16 17 syl ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
19 18 oveq1d ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 = W + 2 - 1
20 19 oveq2d ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 = 0 ..^ W + 2 - 1
21 simp3 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 → N ∈ ℤ ≥ 3
22 simp2 ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → W = N − 2
23 21 22 anim12i ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → N ∈ ℤ ≥ 3 ∧ W = N − 2
24 23 adantr ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → N ∈ ℤ ≥ 3 ∧ W = N − 2
25 clwwlknonex2lem1 ⊢ N ∈ ℤ ≥ 3 ∧ W = N − 2 → 0 ..^ W + 2 - 1 = 0 ..^ W − 1 ∪ W − 1 W
26 24 25 syl ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → 0 ..^ W + 2 - 1 = 0 ..^ W − 1 ∪ W − 1 W
27 20 26 eqtrd ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 = 0 ..^ W − 1 ∪ W − 1 W
28 27 raleqdv ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ↔ ∀ i ∈ 0 ..^ W − 1 ∪ W − 1 W W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E
29 14 28 mpbird ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E
30 ccatws1cl ⊢ W ∈ Word V ∧ X ∈ V → W ++ ⟨“ X ”⟩ ∈ Word V
31 lswccats1 ⊢ W ++ ⟨“ X ”⟩ ∈ Word V ∧ Y ∈ V → lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = Y
32 30 31 stoic3 ⊢ W ∈ Word V ∧ X ∈ V ∧ Y ∈ V → lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = Y
33 16 10 11 32 syl3anc ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = Y
34 3 nngt0d ⊢ N ∈ ℤ ≥ 3 → 0 < N − 2
35 breq2 ⊢ W = N − 2 → 0 < W ↔ 0 < N − 2
36 34 35 syl5ibr ⊢ W = N − 2 → N ∈ ℤ ≥ 3 → 0 < W
37 36 3ad2ant2 ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → N ∈ ℤ ≥ 3 → 0 < W
38 37 com12 ⊢ N ∈ ℤ ≥ 3 → W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → 0 < W
39 38 3ad2ant3 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 → W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → 0 < W
40 39 imp ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → 0 < W
41 40 adantr ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → 0 < W
42 ccat2s1fst ⊢ W ∈ Word V ∧ 0 < W → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = W ⁡ 0
43 16 41 42 syl2anc ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = W ⁡ 0
44 33 43 preq12d ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = Y W ⁡ 0
45 prcom ⊢ X Y = Y X
46 45 eleq1i ⊢ X Y ∈ E ↔ Y X ∈ E
47 46 biimpi ⊢ X Y ∈ E → Y X ∈ E
48 47 adantl ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → Y X ∈ E
49 preq2 ⊢ W ⁡ 0 = X → Y W ⁡ 0 = Y X
50 49 eleq1d ⊢ W ⁡ 0 = X → Y W ⁡ 0 ∈ E ↔ Y X ∈ E
51 50 3ad2ant3 ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → Y W ⁡ 0 ∈ E ↔ Y X ∈ E
52 51 ad2antlr ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → Y W ⁡ 0 ∈ E ↔ Y X ∈ E
53 48 52 mpbird ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → Y W ⁡ 0 ∈ E
54 44 53 eqeltrd ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E
55 13 29 54 3jca ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E
56 17 3ad2ant1 ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
57 56 3ad2ant1 ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
58 57 ad2antlr ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
59 oveq1 ⊢ W = N − 2 → W + 2 = N - 2 + 2
60 eluzelcn ⊢ N ∈ ℤ ≥ 3 → N ∈ ℂ
61 2cn ⊢ 2 ∈ ℂ
62 npcan ⊢ N ∈ ℂ ∧ 2 ∈ ℂ → N - 2 + 2 = N
63 60 61 62 sylancl ⊢ N ∈ ℤ ≥ 3 → N - 2 + 2 = N
64 59 63 sylan9eq ⊢ W = N − 2 ∧ N ∈ ℤ ≥ 3 → W + 2 = N
65 64 ex ⊢ W = N − 2 → N ∈ ℤ ≥ 3 → W + 2 = N
66 65 3ad2ant2 ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → N ∈ ℤ ≥ 3 → W + 2 = N
67 66 com12 ⊢ N ∈ ℤ ≥ 3 → W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → W + 2 = N
68 67 3ad2ant3 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 → W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → W + 2 = N
69 68 imp ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → W + 2 = N
70 69 adantr ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W + 2 = N
71 58 70 eqtrd ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
72 55 71 jca ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E ∧ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
73 72 exp31 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 → W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X → X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E ∧ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
74 7 73 sylbid ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 → W ∈ X ClWWalksNOn ⁡ G N − 2 → X Y ∈ E → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E ∧ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
75 74 com23 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 → X Y ∈ E → W ∈ X ClWWalksNOn ⁡ G N − 2 → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E ∧ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
76 75 3imp ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ X Y ∈ E ∧ W ∈ X ClWWalksNOn ⁡ G N − 2 → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E ∧ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
77 eluzge3nn ⊢ N ∈ ℤ ≥ 3 → N ∈ ℕ
78 1 2 isclwwlknx ⊢ N ∈ ℕ → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ N ClWWalksN G ↔ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E ∧ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
79 77 78 syl ⊢ N ∈ ℤ ≥ 3 → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ N ClWWalksN G ↔ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E ∧ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
80 79 3ad2ant3 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ N ClWWalksN G ↔ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E ∧ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
81 80 3ad2ant1 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ X Y ∈ E ∧ W ∈ X ClWWalksNOn ⁡ G N − 2 → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ N ClWWalksN G ↔ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V ∧ ∀ i ∈ 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ − 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E ∧ lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 ∈ E ∧ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
82 76 81 mpbird ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ X Y ∈ E ∧ W ∈ X ClWWalksNOn ⁡ G N − 2 → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ N ClWWalksN G