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 14 27 raleqtrrdv ⊢ 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
29 ccatws1cl ⊢ W ∈ Word V ∧ X ∈ V → W ++ ⟨“ X ”⟩ ∈ Word V
30 lswccats1 ⊢ W ++ ⟨“ X ”⟩ ∈ Word V ∧ Y ∈ V → lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = Y
31 29 30 stoic3 ⊢ W ∈ Word V ∧ X ∈ V ∧ Y ∈ V → lastS ⁡ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = Y
32 16 10 11 31 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
33 3 nngt0d ⊢ N ∈ ℤ ≥ 3 → 0 < N − 2
34 breq2 ⊢ W = N − 2 → 0 < W ↔ 0 < N − 2
35 33 34 imbitrrid ⊢ W = N − 2 → N ∈ ℤ ≥ 3 → 0 < W
36 35 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
37 36 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
38 37 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
39 38 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
40 39 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
41 ccat2s1fst ⊢ W ∈ Word V ∧ 0 < W → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = W ⁡ 0
42 16 40 41 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
43 32 42 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
44 prcom ⊢ X Y = Y X
45 44 eleq1i ⊢ X Y ∈ E ↔ Y X ∈ E
46 45 biimpi ⊢ X Y ∈ E → Y X ∈ E
47 46 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
48 preq2 ⊢ W ⁡ 0 = X → Y W ⁡ 0 = Y X
49 48 eleq1d ⊢ W ⁡ 0 = X → Y W ⁡ 0 ∈ E ↔ Y X ∈ E
50 49 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
51 50 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
52 47 51 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
53 43 52 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
54 13 28 53 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
55 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
56 55 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
57 56 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
58 oveq1 ⊢ W = N − 2 → W + 2 = N - 2 + 2
59 eluzelcn ⊢ N ∈ ℤ ≥ 3 → N ∈ ℂ
60 2cn ⊢ 2 ∈ ℂ
61 npcan ⊢ N ∈ ℂ ∧ 2 ∈ ℂ → N - 2 + 2 = N
62 59 60 61 sylancl ⊢ N ∈ ℤ ≥ 3 → N - 2 + 2 = N
63 58 62 sylan9eq ⊢ W = N − 2 ∧ N ∈ ℤ ≥ 3 → W + 2 = N
64 63 ex ⊢ W = N − 2 → N ∈ ℤ ≥ 3 → W + 2 = N
65 64 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
66 65 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
67 66 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
68 67 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
69 68 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
70 57 69 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
71 54 70 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
72 71 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
73 7 72 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
74 73 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
75 74 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
76 eluzge3nn ⊢ N ∈ ℤ ≥ 3 → N ∈ ℕ
77 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
78 76 77 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
79 78 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
80 79 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
81 75 80 mpbird ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ X Y ∈ E ∧ W ∈ X ClWWalksNOn ⁡ G N − 2 → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ N ClWWalksN G