Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  numclwwlkovf2ex Structured version   Visualization version   GIF version

Theorem numclwwlkovf2ex 26613
 Description: Extending a closed walk starting at a fixed vertex by an additional edge (forth and back). (Contributed by AV, 22-Sep-2018.) (Proof shortened by AV, 23-Oct-2018.)
Hypotheses
Ref Expression
numclwwlk.c 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))
numclwwlk.f 𝐹 = (𝑣𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶𝑛) ∣ (𝑤‘0) = 𝑣})
Assertion
Ref Expression
numclwwlkovf2ex (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝐶𝑁))
Distinct variable groups:   𝑛,𝐸   𝑛,𝑁   𝑛,𝑉   𝑤,𝐶   𝑤,𝑁   𝐶,𝑛,𝑣,𝑤   𝑣,𝑁   𝑛,𝑋,𝑣,𝑤   𝑣,𝑉   𝑤,𝐸   𝑤,𝑉   𝑤,𝐹   𝑤,𝑃   𝑤,𝑄
Allowed substitution hints:   𝑃(𝑣,𝑛)   𝑄(𝑣,𝑛)   𝐸(𝑣)   𝐹(𝑣,𝑛)

Proof of Theorem numclwwlkovf2ex
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 simp1 1054 . . . . . . 7 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑉 USGrph 𝐸)
2 uzuzle23 11605 . . . . . . . . 9 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ (ℤ‘2))
3 uznn0sub 11595 . . . . . . . . 9 (𝑁 ∈ (ℤ‘2) → (𝑁 − 2) ∈ ℕ0)
42, 3syl 17 . . . . . . . 8 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℕ0)
543ad2ant3 1077 . . . . . . 7 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ ℕ0)
6 simp2 1055 . . . . . . 7 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑋𝑉)
7 numclwwlk.c . . . . . . . 8 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))
8 numclwwlk.f . . . . . . . 8 𝐹 = (𝑣𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶𝑛) ∣ (𝑤‘0) = 𝑣})
97, 8numclwwlkovfel2 26610 . . . . . . 7 ((𝑉 USGrph 𝐸 ∧ (𝑁 − 2) ∈ ℕ0𝑋𝑉) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)))
101, 5, 6, 9syl3anc 1318 . . . . . 6 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)))
11 ccatws1cl 13249 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ Word 𝑉𝑋𝑉) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
1211ex 449 . . . . . . . . . . . . . . . 16 (𝑃 ∈ Word 𝑉 → (𝑋𝑉 → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
13123ad2ant1 1075 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → (𝑋𝑉 → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
14133ad2ant1 1075 . . . . . . . . . . . . . 14 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑋𝑉 → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
1514com12 32 . . . . . . . . . . . . 13 (𝑋𝑉 → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
16153ad2ant2 1076 . . . . . . . . . . . 12 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
1716imp 444 . . . . . . . . . . 11 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
1817adantr 480 . . . . . . . . . 10 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
19 nbgraisvtx 25960 . . . . . . . . . . . . . 14 (𝑉 USGrph 𝐸 → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → 𝑄𝑉))
20 s1cl 13235 . . . . . . . . . . . . . 14 (𝑄𝑉 → ⟨“𝑄”⟩ ∈ Word 𝑉)
2119, 20syl6 34 . . . . . . . . . . . . 13 (𝑉 USGrph 𝐸 → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ⟨“𝑄”⟩ ∈ Word 𝑉))
22213ad2ant1 1075 . . . . . . . . . . . 12 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ⟨“𝑄”⟩ ∈ Word 𝑉))
2322adantr 480 . . . . . . . . . . 11 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ⟨“𝑄”⟩ ∈ Word 𝑉))
2423imp 444 . . . . . . . . . 10 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ⟨“𝑄”⟩ ∈ Word 𝑉)
25 ccatcl 13212 . . . . . . . . . 10 (((𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ ⟨“𝑄”⟩ ∈ Word 𝑉) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉)
2618, 24, 25syl2anc 691 . . . . . . . . 9 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉)
27 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → 𝑃 ∈ Word 𝑉)
2827ad2antlr 759 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → 𝑃 ∈ Word 𝑉)
2928ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑃 ∈ Word 𝑉)
30 elfzonn0 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 ∈ ℕ0)
3130adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑖 ∈ ℕ0)
32 lencl 13179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℕ0)
33 elfzo0 12376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^((#‘𝑃) − 1)) ↔ (𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)))
34 nn0re 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
3534adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → 𝑖 ∈ ℝ)
36 nn0re 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((#‘𝑃) ∈ ℕ0 → (#‘𝑃) ∈ ℝ)
37 peano2rem 10227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((#‘𝑃) ∈ ℝ → ((#‘𝑃) − 1) ∈ ℝ)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((#‘𝑃) ∈ ℕ0 → ((#‘𝑃) − 1) ∈ ℝ)
3938adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → ((#‘𝑃) − 1) ∈ ℝ)
4036adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (#‘𝑃) ∈ ℝ)
4135, 39, 403jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ ∧ (#‘𝑃) ∈ ℝ))
4236ltm1d 10835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((#‘𝑃) ∈ ℕ0 → ((#‘𝑃) − 1) < (#‘𝑃))
4342adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → ((#‘𝑃) − 1) < (#‘𝑃))
44 lttr 9993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ ∧ (#‘𝑃) ∈ ℝ) → ((𝑖 < ((#‘𝑃) − 1) ∧ ((#‘𝑃) − 1) < (#‘𝑃)) → 𝑖 < (#‘𝑃)))
4544expcomd 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ ∧ (#‘𝑃) ∈ ℝ) → (((#‘𝑃) − 1) < (#‘𝑃) → (𝑖 < ((#‘𝑃) − 1) → 𝑖 < (#‘𝑃))))
4641, 43, 45sylc 63 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (𝑖 < ((#‘𝑃) − 1) → 𝑖 < (#‘𝑃)))
4746impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0𝑖 < (#‘𝑃)))
48473adant2 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0𝑖 < (#‘𝑃)))
4933, 48sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0𝑖 < (#‘𝑃)))
5032, 49syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃)))
5150ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃)))
5251ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃)))
5352imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑖 < (#‘𝑃))
5429, 31, 533jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (#‘𝑃)))
556adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝑋𝑉)
56193ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → 𝑄𝑉))
5756com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑄𝑉))
5857ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑄𝑉))
5958imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝑄𝑉)
6055, 59jca 553 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑋𝑉𝑄𝑉))
6160adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑋𝑉𝑄𝑉))
62 ccat2s1fvw 13267 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖) = (𝑃𝑖))
6362eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑃 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (𝑃𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖))
6454, 61, 63syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖))
65 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑃 ∈ Word 𝑉)
66 peano2nn0 11210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
67663ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)) → (𝑖 + 1) ∈ ℕ0)
6833, 67sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑖 + 1) ∈ ℕ0)
6968adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑖 + 1) ∈ ℕ0)
70 1red 9934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → 1 ∈ ℝ)
7135, 70, 40ltaddsubd 10506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → ((𝑖 + 1) < (#‘𝑃) ↔ 𝑖 < ((#‘𝑃) − 1)))
7271biimprd 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (𝑖 < ((#‘𝑃) − 1) → (𝑖 + 1) < (#‘𝑃)))
7372impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ ℕ0𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0 → (𝑖 + 1) < (#‘𝑃)))
74733adant2 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0 → (𝑖 + 1) < (#‘𝑃)))
7533, 74sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0 → (𝑖 + 1) < (#‘𝑃)))
7632, 75mpan9 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑖 + 1) < (#‘𝑃))
7765, 69, 763jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)))
7877ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))))
7978ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))))
8079ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))))
8180imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)))
82 ccat2s1fvw 13267 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
8381, 61, 82syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
8483eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃‘(𝑖 + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)))
8564, 84preq12d 4220 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → {(𝑃𝑖), (𝑃‘(𝑖 + 1))} = {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))})
8685eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → ({(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
8786ralbidva 2968 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
8887biimpd 218 . . . . . . . . . . . . . . . . . . . 20 ((((𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
8988exp41 636 . . . . . . . . . . . . . . . . . . 19 (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸)))))
9089com15 99 . . . . . . . . . . . . . . . . . 18 (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸)))))
9190expd 451 . . . . . . . . . . . . . . . . 17 (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))))))
9291com12 32 . . . . . . . . . . . . . . . 16 (𝑃 ∈ Word 𝑉 → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))))))
93923imp 1249 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))))
94933impib 1254 . . . . . . . . . . . . . 14 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸)))
9594impcom 445 . . . . . . . . . . . . 13 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
9695imp 444 . . . . . . . . . . . 12 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
97 simpll 786 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → 𝑃 ∈ Word 𝑉)
98 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝑃) = (𝑁 − 2) → ((#‘𝑃) − 1) = ((𝑁 − 2) − 1))
9998adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) = ((𝑁 − 2) − 1))
100 eluzelcn 11575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℂ)
101 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘3) → 2 ∈ ℂ)
102 1cnd 9935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘3) → 1 ∈ ℂ)
103100, 101, 102subsub4d 10302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1)))
104 2p1e3 11028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (2 + 1) = 3
105104a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ (ℤ‘3) → (2 + 1) = 3)
106105oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3))
107 uznn0sub 11595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘3) → (𝑁 − 3) ∈ ℕ0)
108106, 107eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘3) → (𝑁 − (2 + 1)) ∈ ℕ0)
109103, 108eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) ∈ ℕ0)
110109adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((𝑁 − 2) − 1) ∈ ℕ0)
11199, 110eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) ∈ ℕ0)
112111adantll 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) ∈ ℕ0)
11332, 42syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) < (#‘𝑃))
114113ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) < (#‘𝑃))
11597, 112, 1143jca 1235 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))
116115exp31 628 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))))
117116a1dd 48 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))))
1181173ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))))
1191183imp 1249 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))
120119com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))
1211203ad2ant3 1077 . . . . . . . . . . . . . . . . . 18 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))
122121imp 444 . . . . . . . . . . . . . . . . 17 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))
123122adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))
12419ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ Word 𝑉 ∧ (𝑉 USGrph 𝐸𝑋𝑉)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → 𝑄𝑉))
125 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑉 USGrph 𝐸𝑋𝑉) → 𝑋𝑉)
126125adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ Word 𝑉 ∧ (𝑉 USGrph 𝐸𝑋𝑉)) → 𝑋𝑉)
127124, 126jctild 564 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ Word 𝑉 ∧ (𝑉 USGrph 𝐸𝑋𝑉)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (𝑋𝑉𝑄𝑉)))
128127ex 449 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ Word 𝑉 → ((𝑉 USGrph 𝐸𝑋𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (𝑋𝑉𝑄𝑉))))
1291283ad2ant1 1075 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((𝑉 USGrph 𝐸𝑋𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (𝑋𝑉𝑄𝑉))))
1301293ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (𝑋𝑉𝑄𝑉))))
131130com12 32 . . . . . . . . . . . . . . . . . 18 ((𝑉 USGrph 𝐸𝑋𝑉) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (𝑋𝑉𝑄𝑉))))
1321313adant3 1074 . . . . . . . . . . . . . . . . 17 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (𝑋𝑉𝑄𝑉))))
133132imp31 447 . . . . . . . . . . . . . . . 16 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (𝑋𝑉𝑄𝑉))
134 ccat2s1fvw 13267 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)) = (𝑃‘((#‘𝑃) − 1)))
135123, 133, 134syl2anc 691 . . . . . . . . . . . . . . 15 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)) = (𝑃‘((#‘𝑃) − 1)))
136 nn0cn 11179 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝑃) ∈ ℕ0 → (#‘𝑃) ∈ ℂ)
137 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
138 npcan 10169 . . . . . . . . . . . . . . . . . . . . . 22 (((#‘𝑃) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
139136, 137, 138sylancl 693 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝑃) ∈ ℕ0 → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
14032, 139syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ Word 𝑉 → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
1411403ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
1421413ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
143142ad2antlr 759 . . . . . . . . . . . . . . . . 17 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
144143fveq2d 6107 . . . . . . . . . . . . . . . 16 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)))
145 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 USGrph 𝐸𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → 𝑃 ∈ Word 𝑉)
146 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 USGrph 𝐸𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (#‘𝑃) = (#‘𝑃))
147145, 146jca 553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑉 USGrph 𝐸𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)))
148147adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑉 USGrph 𝐸𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)))
149125ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑉 USGrph 𝐸𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → 𝑋𝑉)
15019ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑉 USGrph 𝐸𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → 𝑄𝑉))
151150imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑉 USGrph 𝐸𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → 𝑄𝑉)
152 ccatw2s1p1 13265 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
153148, 149, 151, 152syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑉 USGrph 𝐸𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
154153ex 449 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑉 USGrph 𝐸𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋))
155154expcom 450 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ Word 𝑉 → ((𝑉 USGrph 𝐸𝑋𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
1561553ad2ant1 1075 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((𝑉 USGrph 𝐸𝑋𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
1571563ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
158157com12 32 . . . . . . . . . . . . . . . . . 18 ((𝑉 USGrph 𝐸𝑋𝑉) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
1591583adant3 1074 . . . . . . . . . . . . . . . . 17 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
160159imp31 447 . . . . . . . . . . . . . . . 16 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
161144, 160eqtrd 2644 . . . . . . . . . . . . . . 15 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1)) = 𝑋)
162135, 161preq12d 4220 . . . . . . . . . . . . . 14 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} = {(𝑃‘((#‘𝑃) − 1)), 𝑋})
163 lsw 13204 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
164163adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
165 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → (𝑃‘0) = 𝑋)
166164, 165preq12d 4220 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → {( lastS ‘𝑃), (𝑃‘0)} = {(𝑃‘((#‘𝑃) − 1)), 𝑋})
167166eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ ran 𝐸))
168167biimpd 218 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ ran 𝐸))
169168ex 449 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘0) = 𝑋 → (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ ran 𝐸)))
170169com3l 87 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ ran 𝐸)))
171170imp 444 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ ran 𝐸))
1721713adant2 1073 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ ran 𝐸))
173172a1d 25 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ ran 𝐸)))
1741733imp 1249 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ ran 𝐸)
175174ad2antlr 759 . . . . . . . . . . . . . 14 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ ran 𝐸)
176162, 175eqeltrd 2688 . . . . . . . . . . . . 13 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} ∈ ran 𝐸)
177 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (#‘𝑃) = (#‘𝑃)
178177, 152mpanl2 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ Word 𝑉 ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
179 ccatw2s1p2 13266 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1)) = 𝑄)
180177, 179mpanl2 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ Word 𝑉 ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1)) = 𝑄)
181178, 180preq12d 4220 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ Word 𝑉 ∧ (𝑋𝑉𝑄𝑉)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})
182181expcom 450 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝑉𝑄𝑉) → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))
183182expcom 450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑄𝑉 → (𝑋𝑉 → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
18419, 183syl6 34 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 USGrph 𝐸 → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (𝑋𝑉 → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))))
185184com24 93 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 USGrph 𝐸 → (𝑃 ∈ Word 𝑉 → (𝑋𝑉 → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))))
186185com12 32 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ Word 𝑉 → (𝑉 USGrph 𝐸 → (𝑋𝑉 → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))))
187186impd 446 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ Word 𝑉 → ((𝑉 USGrph 𝐸𝑋𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
1881873ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((𝑉 USGrph 𝐸𝑋𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
1891883ad2ant1 1075 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝑉 USGrph 𝐸𝑋𝑉) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
190189com12 32 . . . . . . . . . . . . . . . 16 ((𝑉 USGrph 𝐸𝑋𝑉) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
1911903adant3 1074 . . . . . . . . . . . . . . 15 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
192191imp31 447 . . . . . . . . . . . . . 14 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})
193 nbgraeledg 25959 . . . . . . . . . . . . . . . . . 18 (𝑉 USGrph 𝐸 → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ↔ {𝑄, 𝑋} ∈ ran 𝐸))
194 prcom 4211 . . . . . . . . . . . . . . . . . . . 20 {𝑄, 𝑋} = {𝑋, 𝑄}
195194eleq1i 2679 . . . . . . . . . . . . . . . . . . 19 ({𝑄, 𝑋} ∈ ran 𝐸 ↔ {𝑋, 𝑄} ∈ ran 𝐸)
196195biimpi 205 . . . . . . . . . . . . . . . . . 18 ({𝑄, 𝑋} ∈ ran 𝐸 → {𝑋, 𝑄} ∈ ran 𝐸)
197193, 196syl6bi 242 . . . . . . . . . . . . . . . . 17 (𝑉 USGrph 𝐸 → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {𝑋, 𝑄} ∈ ran 𝐸))
1981973ad2ant1 1075 . . . . . . . . . . . . . . . 16 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {𝑋, 𝑄} ∈ ran 𝐸))
199198adantr 480 . . . . . . . . . . . . . . 15 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → {𝑋, 𝑄} ∈ ran 𝐸))
200199imp 444 . . . . . . . . . . . . . 14 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {𝑋, 𝑄} ∈ ran 𝐸)
201192, 200eqeltrd 2688 . . . . . . . . . . . . 13 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} ∈ ran 𝐸)
202 ovex 6577 . . . . . . . . . . . . . 14 ((#‘𝑃) − 1) ∈ V
203 fvex 6113 . . . . . . . . . . . . . 14 (#‘𝑃) ∈ V
204 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑖 = ((#‘𝑃) − 1) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)))
205 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑖 = ((#‘𝑃) − 1) → (𝑖 + 1) = (((#‘𝑃) − 1) + 1))
206205fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑖 = ((#‘𝑃) − 1) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1)))
207204, 206preq12d 4220 . . . . . . . . . . . . . . 15 (𝑖 = ((#‘𝑃) − 1) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} = {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))})
208207eleq1d 2672 . . . . . . . . . . . . . 14 (𝑖 = ((#‘𝑃) − 1) → ({(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} ∈ ran 𝐸))
209 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑖 = (#‘𝑃) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)))
210 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑖 = (#‘𝑃) → (𝑖 + 1) = ((#‘𝑃) + 1))
211210fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑖 = (#‘𝑃) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1)))
212209, 211preq12d 4220 . . . . . . . . . . . . . . 15 (𝑖 = (#‘𝑃) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} = {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))})
213212eleq1d 2672 . . . . . . . . . . . . . 14 (𝑖 = (#‘𝑃) → ({(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} ∈ ran 𝐸))
214202, 203, 208, 213ralpr 4185 . . . . . . . . . . . . 13 (∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ({(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} ∈ ran 𝐸 ∧ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} ∈ ran 𝐸))
215176, 201, 214sylanbrc 695 . . . . . . . . . . . 12 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
21696, 215jca 553 . . . . . . . . . . 11 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
217 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((#‘𝑃) ∈ ℕ0 → 2 ∈ ℂ)
218 1cnd 9935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((#‘𝑃) ∈ ℕ0 → 1 ∈ ℂ)
219136, 217, 2183jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((#‘𝑃) ∈ ℕ0 → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
22032, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
2212203ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
222221adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
223 addsubass 10170 . . . . . . . . . . . . . . . . . . . . . . 23 (((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘𝑃) + 2) − 1) = ((#‘𝑃) + (2 − 1)))
224222, 223syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (((#‘𝑃) + 2) − 1) = ((#‘𝑃) + (2 − 1)))
225 2m1e1 11012 . . . . . . . . . . . . . . . . . . . . . . 23 (2 − 1) = 1
226225oveq2i 6560 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝑃) + (2 − 1)) = ((#‘𝑃) + 1)
227224, 226syl6eq 2660 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (((#‘𝑃) + 2) − 1) = ((#‘𝑃) + 1))
228227oveq2d 6565 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (0..^(((#‘𝑃) + 2) − 1)) = (0..^((#‘𝑃) + 1)))
229 0zd 11266 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → 0 ∈ ℤ)
23032nn0zd 11356 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℤ)
2312303ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → (#‘𝑃) ∈ ℤ)
232231adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (#‘𝑃) ∈ ℤ)
233 eluz2 11569 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁))
234 df-3 10957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3 = (2 + 1)
235234breq1i 4590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (3 ≤ 𝑁 ↔ (2 + 1) ≤ 𝑁)
236 2z 11286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ ℤ
237 zltp1le 11304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 < 𝑁 ↔ (2 + 1) ≤ 𝑁))
238236, 237mpan 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℤ → (2 < 𝑁 ↔ (2 + 1) ≤ 𝑁))
239238biimprd 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → ((2 + 1) ≤ 𝑁 → 2 < 𝑁))
240235, 239syl5bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℤ → (3 ≤ 𝑁 → 2 < 𝑁))
241240imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 2 < 𝑁)
242 zre 11258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
243 2re 10967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2 ∈ ℝ
244242, 243jctil 558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → (2 ∈ ℝ ∧ 𝑁 ∈ ℝ))
245244adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (2 ∈ ℝ ∧ 𝑁 ∈ ℝ))
246 posdif 10400 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 < 𝑁 ↔ 0 < (𝑁 − 2)))
247245, 246syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (2 < 𝑁 ↔ 0 < (𝑁 − 2)))
248241, 247mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 0 < (𝑁 − 2))
2492483adant1 1072 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 0 < (𝑁 − 2))
250233, 249sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘3) → 0 < (𝑁 − 2))
251250adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → 0 < (𝑁 − 2))
252 breq2 4587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((#‘𝑃) = (𝑁 − 2) → (0 < (#‘𝑃) ↔ 0 < (𝑁 − 2)))
253252adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → (0 < (#‘𝑃) ↔ 0 < (𝑁 − 2)))
254251, 253mpbird 246 . . . . . . . . . . . . . . . . . . . . . 22 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → 0 < (#‘𝑃))
255254adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → 0 < (#‘𝑃))
256 fzosplitprm1 12443 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℤ ∧ (#‘𝑃) ∈ ℤ ∧ 0 < (#‘𝑃)) → (0..^((#‘𝑃) + 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
257229, 232, 255, 256syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (0..^((#‘𝑃) + 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
258228, 257eqtrd 2644 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
259258expr 641 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2)) → (𝑁 ∈ (ℤ‘3) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
2602593adant3 1074 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ‘3) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
261260com12 32 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
2622613ad2ant3 1077 . . . . . . . . . . . . . . 15 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
263262imp 444 . . . . . . . . . . . . . 14 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
264263adantr 480 . . . . . . . . . . . . 13 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
265264raleqdv 3121 . . . . . . . . . . . 12 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
266 ralunb 3756 . . . . . . . . . . . 12 (∀𝑖 ∈ ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
267265, 266syl6bb 275 . . . . . . . . . . 11 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸)))
268216, 267mpbird 246 . . . . . . . . . 10 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
269 simp11 1084 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 𝑃 ∈ Word 𝑉)
270269ad2antlr 759 . . . . . . . . . . . . . 14 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → 𝑃 ∈ Word 𝑉)
2716ad2antrr 758 . . . . . . . . . . . . . 14 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → 𝑋𝑉)
27256adantr 480 . . . . . . . . . . . . . . 15 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → 𝑄𝑉))
273272imp 444 . . . . . . . . . . . . . 14 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → 𝑄𝑉)
274 ccatw2s1len 13254 . . . . . . . . . . . . . 14 ((𝑃 ∈ Word 𝑉𝑋𝑉𝑄𝑉) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = ((#‘𝑃) + 2))
275270, 271, 273, 274syl3anc 1318 . . . . . . . . . . . . 13 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = ((#‘𝑃) + 2))
276275oveq1d 6564 . . . . . . . . . . . 12 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1) = (((#‘𝑃) + 2) − 1))
277276oveq2d 6565 . . . . . . . . . . 11 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)) = (0..^(((#‘𝑃) + 2) − 1)))
278277raleqdv 3121 . . . . . . . . . 10 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
279268, 278mpbird 246 . . . . . . . . 9 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
280 lswccats1 13263 . . . . . . . . . . . . 13 (((𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉𝑄𝑉) → ( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑄)
28111, 280stoic3 1692 . . . . . . . . . . . 12 ((𝑃 ∈ Word 𝑉𝑋𝑉𝑄𝑉) → ( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑄)
282270, 271, 273, 281syl3anc 1318 . . . . . . . . . . 11 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑄)
283 uz3m2nn 11607 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℕ)
284283nngt0d 10941 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘3) → 0 < (𝑁 − 2))
285284, 252syl5ibr 235 . . . . . . . . . . . . . . . . 17 ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ‘3) → 0 < (#‘𝑃)))
2862853ad2ant2 1076 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ‘3) → 0 < (#‘𝑃)))
287286com12 32 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 0 < (#‘𝑃)))
2882873ad2ant3 1077 . . . . . . . . . . . . . 14 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 0 < (#‘𝑃)))
289288imp 444 . . . . . . . . . . . . 13 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → 0 < (#‘𝑃))
290289adantr 480 . . . . . . . . . . . 12 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → 0 < (#‘𝑃))
291 ccat2s1fst 13268 . . . . . . . . . . . 12 (((𝑃 ∈ Word 𝑉 ∧ 0 < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0) = (𝑃‘0))
292270, 290, 271, 273, 291syl22anc 1319 . . . . . . . . . . 11 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0) = (𝑃‘0))
293282, 292preq12d 4220 . . . . . . . . . 10 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} = {𝑄, (𝑃‘0)})
2941933ad2ant1 1075 . . . . . . . . . . . . 13 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ↔ {𝑄, 𝑋} ∈ ran 𝐸))
295294adantr 480 . . . . . . . . . . . 12 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ↔ {𝑄, 𝑋} ∈ ran 𝐸))
296295biimpa 500 . . . . . . . . . . 11 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {𝑄, 𝑋} ∈ ran 𝐸)
297 preq2 4213 . . . . . . . . . . . . . 14 ((𝑃‘0) = 𝑋 → {𝑄, (𝑃‘0)} = {𝑄, 𝑋})
298297eleq1d 2672 . . . . . . . . . . . . 13 ((𝑃‘0) = 𝑋 → ({𝑄, (𝑃‘0)} ∈ ran 𝐸 ↔ {𝑄, 𝑋} ∈ ran 𝐸))
2992983ad2ant3 1077 . . . . . . . . . . . 12 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ({𝑄, (𝑃‘0)} ∈ ran 𝐸 ↔ {𝑄, 𝑋} ∈ ran 𝐸))
300299ad2antlr 759 . . . . . . . . . . 11 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ({𝑄, (𝑃‘0)} ∈ ran 𝐸 ↔ {𝑄, 𝑋} ∈ ran 𝐸))
301296, 300mpbird 246 . . . . . . . . . 10 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {𝑄, (𝑃‘0)} ∈ ran 𝐸)
302293, 301eqeltrd 2688 . . . . . . . . 9 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸)
30326, 279, 3023jca 1235 . . . . . . . 8 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸))
304269ad2antlr 759 . . . . . . . . . . . . 13 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → 𝑃 ∈ Word 𝑉)
3056ad2antrr 758 . . . . . . . . . . . . 13 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → 𝑋𝑉)
306 simpr 476 . . . . . . . . . . . . 13 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → 𝑄𝑉)
307304, 305, 306, 274syl3anc 1318 . . . . . . . . . . . 12 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = ((#‘𝑃) + 2))
308 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 ((#‘𝑃) = (𝑁 − 2) → ((#‘𝑃) + 2) = ((𝑁 − 2) + 2))
309 2cn 10968 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℂ
310 npcan 10169 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑁 − 2) + 2) = 𝑁)
311100, 309, 310sylancl 693 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) + 2) = 𝑁)
312308, 311sylan9eq 2664 . . . . . . . . . . . . . . . . . 18 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) + 2) = 𝑁)
313312ex 449 . . . . . . . . . . . . . . . . 17 ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ‘3) → ((#‘𝑃) + 2) = 𝑁))
3143133ad2ant2 1076 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ‘3) → ((#‘𝑃) + 2) = 𝑁))
315314com12 32 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((#‘𝑃) + 2) = 𝑁))
3163153ad2ant3 1077 . . . . . . . . . . . . . 14 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((#‘𝑃) + 2) = 𝑁))
317316imp 444 . . . . . . . . . . . . 13 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → ((#‘𝑃) + 2) = 𝑁)
318317adantr 480 . . . . . . . . . . . 12 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → ((#‘𝑃) + 2) = 𝑁)
319307, 318eqtrd 2644 . . . . . . . . . . 11 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)
320319ex 449 . . . . . . . . . 10 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄𝑉 → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
321272, 320syld 46 . . . . . . . . 9 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
322321imp 444 . . . . . . . 8 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)
323303, 322jca 553 . . . . . . 7 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋)) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
324323exp31 628 . . . . . 6 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))))
32510, 324sylbid 229 . . . . 5 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))))
326325com23 84 . . . 4 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))))
3273263imp 1249 . . 3 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
328 usgrav 25867 . . . . . 6 (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))
329 eluzge2nn0 11603 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℕ0)
3302, 329syl 17 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℕ0)
331330anim2i 591 . . . . . . . . 9 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ (ℤ‘3)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0))
332 df-3an 1033 . . . . . . . . 9 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0))
333331, 332sylibr 223 . . . . . . . 8 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ (ℤ‘3)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0))
334 isclwwlkn 26297 . . . . . . . 8 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
335333, 334syl 17 . . . . . . 7 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ (ℤ‘3)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
336 isclwwlk 26296 . . . . . . . . 9 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑉 ClWWalks 𝐸) ↔ (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸)))
337336adantr 480 . . . . . . . 8 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ (ℤ‘3)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑉 ClWWalks 𝐸) ↔ (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸)))
338337anbi1d 737 . . . . . . 7 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ (ℤ‘3)) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
339335, 338bitrd 267 . . . . . 6 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ (ℤ‘3)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
340328, 339sylan 487 . . . . 5 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
3413403adant2 1073 . . . 4 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
3423413ad2ant1 1075 . . 3 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ ran 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
343327, 342mpbird 246 . 2 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))
3447numclwwlkfvc 26604 . . . . 5 (𝑁 ∈ ℕ0 → (𝐶𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁))
345330, 344syl 17 . . . 4 (𝑁 ∈ (ℤ‘3) → (𝐶𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁))
3463453ad2ant3 1077 . . 3 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝐶𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁))
3473463ad2ant1 1075 . 2 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → (𝐶𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁))
348343, 347eleqtrrd 2691 1 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝐶𝑁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900  Vcvv 3173   ∪ cun 3538  {cpr 4127  ⟨cop 4131   class class class wbr 4583   ↦ cmpt 4643  ran crn 5039  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  2c2 10947  3c3 10948  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ..^cfzo 12334  #chash 12979  Word cword 13146   lastS clsw 13147   ++ cconcat 13148  ⟨“cs1 13149   USGrph cusg 25859   Neighbors cnbgra 25946   ClWWalks cclwwlk 26276   ClWWalksN cclwwlkn 26277 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154  df-lsw 13155  df-concat 13156  df-s1 13157  df-usgra 25862  df-nbgra 25949  df-clwwlk 26279  df-clwwlkn 26280 This theorem is referenced by:  numclwlk1lem2foa  26618
 Copyright terms: Public domain W3C validator