Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  av-numclwwlkovf2ex Structured version   Visualization version   GIF version

Theorem av-numclwwlkovf2ex 41517
 Description: Extending a closed walk starting at a fixed vertex by an additional edge (forth and back). (Contributed by AV, 22-Sep-2018.) (Revised by AV, 28-May-2021.)
Hypotheses
Ref Expression
av-numclwwlkovf.f 𝐹 = (𝑣𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣})
av-numclwwlkffin.v 𝑉 = (Vtx‘𝐺)
av-numclwwlkovfel2.e 𝐸 = (Edg‘𝐺)
Assertion
Ref Expression
av-numclwwlkovf2ex (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺))
Distinct variable groups:   𝑛,𝐺,𝑣,𝑤   𝑛,𝑁,𝑣,𝑤   𝑛,𝑉,𝑣   𝑛,𝑋,𝑣,𝑤   𝑤,𝑉   𝑤,𝑃
Allowed substitution hints:   𝑃(𝑣,𝑛)   𝑄(𝑤,𝑣,𝑛)   𝐸(𝑤,𝑣,𝑛)   𝐹(𝑤,𝑣,𝑛)

Proof of Theorem av-numclwwlkovf2ex
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 simp1 1054 . . . . . 6 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝐺 ∈ USGraph )
2 uz3m2nn 11607 . . . . . . 7 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℕ)
323ad2ant3 1077 . . . . . 6 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ ℕ)
4 simp2 1055 . . . . . 6 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑋𝑉)
5 av-numclwwlkovf.f . . . . . . 7 𝐹 = (𝑣𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣})
6 av-numclwwlkffin.v . . . . . . 7 𝑉 = (Vtx‘𝐺)
7 av-numclwwlkovfel2.e . . . . . . 7 𝐸 = (Edg‘𝐺)
85, 6, 7av-numclwwlkovfel2 41514 . . . . . 6 ((𝐺 ∈ USGraph ∧ (𝑁 − 2) ∈ ℕ ∧ 𝑋𝑉) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)))
91, 3, 4, 8syl3anc 1318 . . . . 5 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)))
10 ccatws1cl 13249 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word 𝑉𝑋𝑉) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
1110ex 449 . . . . . . . . . . . . . 14 (𝑃 ∈ Word 𝑉 → (𝑋𝑉 → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
12113ad2ant1 1075 . . . . . . . . . . . . 13 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (𝑋𝑉 → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
13123ad2ant1 1075 . . . . . . . . . . . 12 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑋𝑉 → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
1413com12 32 . . . . . . . . . . 11 (𝑋𝑉 → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
15143ad2ant2 1076 . . . . . . . . . 10 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
1615imp 444 . . . . . . . . 9 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
176nbgrisvtx 40581 . . . . . . . . . . . . . 14 ((𝐺 ∈ USGraph ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄𝑉)
1817ex 449 . . . . . . . . . . . . 13 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
19 s1cl 13235 . . . . . . . . . . . . 13 (𝑄𝑉 → ⟨“𝑄”⟩ ∈ Word 𝑉)
2018, 19syl6 34 . . . . . . . . . . . 12 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ⟨“𝑄”⟩ ∈ Word 𝑉))
21203ad2ant1 1075 . . . . . . . . . . 11 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ⟨“𝑄”⟩ ∈ Word 𝑉))
2221adantr 480 . . . . . . . . . 10 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ⟨“𝑄”⟩ ∈ Word 𝑉))
2322imp 444 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ⟨“𝑄”⟩ ∈ Word 𝑉)
24 ccatcl 13212 . . . . . . . . 9 (((𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ ⟨“𝑄”⟩ ∈ Word 𝑉) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉)
2516, 23, 24syl2an2r 872 . . . . . . . 8 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉)
26 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → 𝑃 ∈ Word 𝑉)
2726ad2antlr 759 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → 𝑃 ∈ Word 𝑉)
2827ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑃 ∈ Word 𝑉)
29 elfzonn0 12380 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 ∈ ℕ0)
3029adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑖 ∈ ℕ0)
31 lencl 13179 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℕ0)
32 elfzo0 12376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^((#‘𝑃) − 1)) ↔ (𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)))
33 nn0re 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
3433adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → 𝑖 ∈ ℝ)
35 nn0re 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((#‘𝑃) ∈ ℕ0 → (#‘𝑃) ∈ ℝ)
36 peano2rem 10227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((#‘𝑃) ∈ ℝ → ((#‘𝑃) − 1) ∈ ℝ)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((#‘𝑃) ∈ ℕ0 → ((#‘𝑃) − 1) ∈ ℝ)
3837adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → ((#‘𝑃) − 1) ∈ ℝ)
3935adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (#‘𝑃) ∈ ℝ)
4034, 38, 393jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ ∧ (#‘𝑃) ∈ ℝ))
4135ltm1d 10835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((#‘𝑃) ∈ ℕ0 → ((#‘𝑃) − 1) < (#‘𝑃))
4241adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → ((#‘𝑃) − 1) < (#‘𝑃))
43 lttr 9993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ ∧ (#‘𝑃) ∈ ℝ) → ((𝑖 < ((#‘𝑃) − 1) ∧ ((#‘𝑃) − 1) < (#‘𝑃)) → 𝑖 < (#‘𝑃)))
4443expcomd 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ ∧ (#‘𝑃) ∈ ℝ) → (((#‘𝑃) − 1) < (#‘𝑃) → (𝑖 < ((#‘𝑃) − 1) → 𝑖 < (#‘𝑃))))
4540, 42, 44sylc 63 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (𝑖 < ((#‘𝑃) − 1) → 𝑖 < (#‘𝑃)))
4645impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑖 ∈ ℕ0𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0𝑖 < (#‘𝑃)))
47463adant2 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0𝑖 < (#‘𝑃)))
4832, 47sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0𝑖 < (#‘𝑃)))
4931, 48syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃)))
5049ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃)))
5150ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃)))
5251imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑖 < (#‘𝑃))
5328, 30, 523jca 1235 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (#‘𝑃)))
544adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝑋𝑉)
55183ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
5655com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑄𝑉))
5756ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑄𝑉))
5857imp 444 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝑄𝑉)
5954, 58jca 553 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑋𝑉𝑄𝑉))
6059adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑋𝑉𝑄𝑉))
61 ccat2s1fvw 13267 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖) = (𝑃𝑖))
6261eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (𝑃𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖))
6353, 60, 62syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖))
64 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑃 ∈ Word 𝑉)
65 peano2nn0 11210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
66653ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)) → (𝑖 + 1) ∈ ℕ0)
6732, 66sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑖 + 1) ∈ ℕ0)
6867adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑖 + 1) ∈ ℕ0)
69 1red 9934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → 1 ∈ ℝ)
7034, 69, 39ltaddsubd 10506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → ((𝑖 + 1) < (#‘𝑃) ↔ 𝑖 < ((#‘𝑃) − 1)))
7170biimprd 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (𝑖 < ((#‘𝑃) − 1) → (𝑖 + 1) < (#‘𝑃)))
7271impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0 → (𝑖 + 1) < (#‘𝑃)))
73723adant2 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0 → (𝑖 + 1) < (#‘𝑃)))
7432, 73sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0 → (𝑖 + 1) < (#‘𝑃)))
7531, 74mpan9 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑖 + 1) < (#‘𝑃))
7664, 68, 753jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)))
7776ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))))
7877ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))))
7978ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))))
8079imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)))
81 ccat2s1fvw 13267 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
8280, 60, 81syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
8382eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃‘(𝑖 + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)))
8463, 83preq12d 4220 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → {(𝑃𝑖), (𝑃‘(𝑖 + 1))} = {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))})
8584eleq1d 2672 . . . . . . . . . . . . . . . . . . . 20 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → ({(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
8685ralbidva 2968 . . . . . . . . . . . . . . . . . . 19 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
8786biimpd 218 . . . . . . . . . . . . . . . . . 18 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
8887exp41 636 . . . . . . . . . . . . . . . . 17 (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)))))
8988com15 99 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)))))
9089expd 451 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))))))
91903imp21 1269 . . . . . . . . . . . . . 14 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
92913impib 1254 . . . . . . . . . . . . 13 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
9392impcom 445 . . . . . . . . . . . 12 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
9493imp 444 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)
95 simpll 786 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → 𝑃 ∈ Word 𝑉)
96 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((#‘𝑃) = (𝑁 − 2) → ((#‘𝑃) − 1) = ((𝑁 − 2) − 1))
9796adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) = ((𝑁 − 2) − 1))
98 eluzelcn 11575 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℂ)
99 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → 2 ∈ ℂ)
100 1cnd 9935 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → 1 ∈ ℂ)
10198, 99, 100subsub4d 10302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1)))
102 2p1e3 11028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2 + 1) = 3
103102a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘3) → (2 + 1) = 3)
104103oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3))
105 uznn0sub 11595 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → (𝑁 − 3) ∈ ℕ0)
106104, 105eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → (𝑁 − (2 + 1)) ∈ ℕ0)
107101, 106eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) ∈ ℕ0)
108107adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((𝑁 − 2) − 1) ∈ ℕ0)
10997, 108eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . 24 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) ∈ ℕ0)
110109adantll 746 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) ∈ ℕ0)
11131, 41syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) < (#‘𝑃))
112111ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) < (#‘𝑃))
11395, 110, 1123jca 1235 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))
114113exp31 628 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))))
115114a1dd 48 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))))
1161153ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))))
1171163imp 1249 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))
118117com12 32 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))
1191183ad2ant3 1077 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))
120119imp 444 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))
12118ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ Word 𝑉 ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
122 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → 𝑋𝑉)
123122adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ Word 𝑉 ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉)) → 𝑋𝑉)
124121, 123jctild 564 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ Word 𝑉 ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉)))
125124ex 449 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉))))
1261253ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉))))
1271263ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉))))
128127com12 32 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉))))
1291283adant3 1074 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉))))
130129imp31 447 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑋𝑉𝑄𝑉))
131 ccat2s1fvw 13267 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)) = (𝑃‘((#‘𝑃) − 1)))
132120, 130, 131syl2an2r 872 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)) = (𝑃‘((#‘𝑃) − 1)))
133 nn0cn 11179 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝑃) ∈ ℕ0 → (#‘𝑃) ∈ ℂ)
134 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
135 npcan 10169 . . . . . . . . . . . . . . . . . . . . 21 (((#‘𝑃) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
136133, 134, 135sylancl 693 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝑃) ∈ ℕ0 → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
13731, 136syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ Word 𝑉 → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
1381373ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
1391383ad2ant1 1075 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
140139ad2antlr 759 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
141140fveq2d 6107 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)))
142 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → 𝑃 ∈ Word 𝑉)
143 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (#‘𝑃) = (#‘𝑃))
144142, 143jca 553 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)))
145144adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)))
146122ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑋𝑉)
14718ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
148147imp 444 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄𝑉)
149 ccatw2s1p1 13265 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
150145, 146, 148, 149syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
151150ex 449 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋))
152151expcom 450 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
1531523ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
1541533ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
155154com12 32 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
1561553adant3 1074 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
157156imp31 447 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
158141, 157eqtrd 2644 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1)) = 𝑋)
159132, 158preq12d 4220 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} = {(𝑃‘((#‘𝑃) − 1)), 𝑋})
160 lsw 13204 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
161160adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
162 simpl 472 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → (𝑃‘0) = 𝑋)
163161, 162preq12d 4220 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → {( lastS ‘𝑃), (𝑃‘0)} = {(𝑃‘((#‘𝑃) − 1)), 𝑋})
164163eleq1d 2672 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))
165164biimpd 218 . . . . . . . . . . . . . . . . . . . 20 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))
166165ex 449 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘0) = 𝑋 → (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)))
167166com3l 87 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)))
168167imp 444 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))
1691683adant2 1073 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))
170169a1d 25 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)))
1711703imp 1249 . . . . . . . . . . . . . 14 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)
172171ad2antlr 759 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)
173159, 172eqeltrd 2688 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} ∈ 𝐸)
174 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (#‘𝑃) = (#‘𝑃)
175174, 149mpanl2 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ Word 𝑉 ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
176 ccatw2s1p2 13266 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1)) = 𝑄)
177174, 176mpanl2 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ Word 𝑉 ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1)) = 𝑄)
178175, 177preq12d 4220 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 ∈ Word 𝑉 ∧ (𝑋𝑉𝑄𝑉)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})
179178expcom 450 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝑉𝑄𝑉) → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))
180179expcom 450 . . . . . . . . . . . . . . . . . . . . . 22 (𝑄𝑉 → (𝑋𝑉 → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
18118, 180syl6 34 . . . . . . . . . . . . . . . . . . . . 21 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉 → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))))
182181com24 93 . . . . . . . . . . . . . . . . . . . 20 (𝐺 ∈ USGraph → (𝑃 ∈ Word 𝑉 → (𝑋𝑉 → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))))
183182com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ Word 𝑉 → (𝐺 ∈ USGraph → (𝑋𝑉 → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))))
184183impd 446 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
1851843ad2ant1 1075 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
1861853ad2ant1 1075 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
187186com12 32 . . . . . . . . . . . . . . 15 ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
1881873adant3 1074 . . . . . . . . . . . . . 14 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
189188imp31 447 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})
1907nbusgreledg 40575 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑄, 𝑋} ∈ 𝐸))
191 prcom 4211 . . . . . . . . . . . . . . . . . . 19 {𝑄, 𝑋} = {𝑋, 𝑄}
192191eleq1i 2679 . . . . . . . . . . . . . . . . . 18 ({𝑄, 𝑋} ∈ 𝐸 ↔ {𝑋, 𝑄} ∈ 𝐸)
193192biimpi 205 . . . . . . . . . . . . . . . . 17 ({𝑄, 𝑋} ∈ 𝐸 → {𝑋, 𝑄} ∈ 𝐸)
194190, 193syl6bi 242 . . . . . . . . . . . . . . . 16 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑄} ∈ 𝐸))
1951943ad2ant1 1075 . . . . . . . . . . . . . . 15 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑄} ∈ 𝐸))
196195adantr 480 . . . . . . . . . . . . . 14 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑄} ∈ 𝐸))
197196imp 444 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑋, 𝑄} ∈ 𝐸)
198189, 197eqeltrd 2688 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} ∈ 𝐸)
199 ovex 6577 . . . . . . . . . . . . 13 ((#‘𝑃) − 1) ∈ V
200 fvex 6113 . . . . . . . . . . . . 13 (#‘𝑃) ∈ V
201 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑖 = ((#‘𝑃) − 1) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)))
202 oveq1 6556 . . . . . . . . . . . . . . . 16 (𝑖 = ((#‘𝑃) − 1) → (𝑖 + 1) = (((#‘𝑃) − 1) + 1))
203202fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑖 = ((#‘𝑃) − 1) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1)))
204201, 203preq12d 4220 . . . . . . . . . . . . . 14 (𝑖 = ((#‘𝑃) − 1) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} = {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))})
205204eleq1d 2672 . . . . . . . . . . . . 13 (𝑖 = ((#‘𝑃) − 1) → ({(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} ∈ 𝐸))
206 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑖 = (#‘𝑃) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)))
207 oveq1 6556 . . . . . . . . . . . . . . . 16 (𝑖 = (#‘𝑃) → (𝑖 + 1) = ((#‘𝑃) + 1))
208207fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑖 = (#‘𝑃) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1)))
209206, 208preq12d 4220 . . . . . . . . . . . . . 14 (𝑖 = (#‘𝑃) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} = {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))})
210209eleq1d 2672 . . . . . . . . . . . . 13 (𝑖 = (#‘𝑃) → ({(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} ∈ 𝐸))
211199, 200, 205, 210ralpr 4185 . . . . . . . . . . . 12 (∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} ∈ 𝐸))
212173, 198, 211sylanbrc 695 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)
21394, 212jca 553 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
214 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((#‘𝑃) ∈ ℕ0 → 2 ∈ ℂ)
215 1cnd 9935 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((#‘𝑃) ∈ ℕ0 → 1 ∈ ℂ)
216133, 214, 2153jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑃) ∈ ℕ0 → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
21731, 216syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
2182173ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
219218adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
220 addsubass 10170 . . . . . . . . . . . . . . . . . . . . . 22 (((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘𝑃) + 2) − 1) = ((#‘𝑃) + (2 − 1)))
221219, 220syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (((#‘𝑃) + 2) − 1) = ((#‘𝑃) + (2 − 1)))
222 2m1e1 11012 . . . . . . . . . . . . . . . . . . . . . 22 (2 − 1) = 1
223222oveq2i 6560 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝑃) + (2 − 1)) = ((#‘𝑃) + 1)
224221, 223syl6eq 2660 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (((#‘𝑃) + 2) − 1) = ((#‘𝑃) + 1))
225224oveq2d 6565 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (0..^(((#‘𝑃) + 2) − 1)) = (0..^((#‘𝑃) + 1)))
226 0zd 11266 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → 0 ∈ ℤ)
22731nn0zd 11356 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℤ)
2282273ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (#‘𝑃) ∈ ℤ)
229228adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (#‘𝑃) ∈ ℤ)
230 eluz2 11569 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁))
231 df-3 10957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 = (2 + 1)
232231breq1i 4590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (3 ≤ 𝑁 ↔ (2 + 1) ≤ 𝑁)
233 2z 11286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2 ∈ ℤ
234 zltp1le 11304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 < 𝑁 ↔ (2 + 1) ≤ 𝑁))
235233, 234mpan 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → (2 < 𝑁 ↔ (2 + 1) ≤ 𝑁))
236235biimprd 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℤ → ((2 + 1) ≤ 𝑁 → 2 < 𝑁))
237232, 236syl5bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℤ → (3 ≤ 𝑁 → 2 < 𝑁))
238237imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 2 < 𝑁)
239 zre 11258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
240 2re 10967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℝ
241239, 240jctil 558 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℤ → (2 ∈ ℝ ∧ 𝑁 ∈ ℝ))
242241adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (2 ∈ ℝ ∧ 𝑁 ∈ ℝ))
243 posdif 10400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 < 𝑁 ↔ 0 < (𝑁 − 2)))
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (2 < 𝑁 ↔ 0 < (𝑁 − 2)))
245238, 244mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 0 < (𝑁 − 2))
2462453adant1 1072 . . . . . . . . . . . . . . . . . . . . . . . 24 ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 0 < (𝑁 − 2))
247230, 246sylbi 206 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘3) → 0 < (𝑁 − 2))
248247adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → 0 < (𝑁 − 2))
249 breq2 4587 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑃) = (𝑁 − 2) → (0 < (#‘𝑃) ↔ 0 < (𝑁 − 2)))
250249adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → (0 < (#‘𝑃) ↔ 0 < (𝑁 − 2)))
251248, 250mpbird 246 . . . . . . . . . . . . . . . . . . . . 21 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → 0 < (#‘𝑃))
252251adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → 0 < (#‘𝑃))
253 fzosplitprm1 12443 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℤ ∧ (#‘𝑃) ∈ ℤ ∧ 0 < (#‘𝑃)) → (0..^((#‘𝑃) + 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
254226, 229, 252, 253syl3anc 1318 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (0..^((#‘𝑃) + 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
255225, 254eqtrd 2644 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
256255expr 641 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2)) → (𝑁 ∈ (ℤ‘3) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
2572563adant3 1074 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ‘3) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
258257com12 32 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
2592583ad2ant3 1077 . . . . . . . . . . . . . 14 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
260259imp 444 . . . . . . . . . . . . 13 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
261260adantr 480 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
262261raleqdv 3121 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
263 ralunb 3756 . . . . . . . . . . 11 (∀𝑖 ∈ ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
264262, 263syl6bb 275 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
265213, 264mpbird 246 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)
266 simp11 1084 . . . . . . . . . . . . . 14 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 𝑃 ∈ Word 𝑉)
267266ad2antlr 759 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑃 ∈ Word 𝑉)
2684ad2antrr 758 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑋𝑉)
26955adantr 480 . . . . . . . . . . . . . 14 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
270269imp 444 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄𝑉)
271 ccatw2s1len 13254 . . . . . . . . . . . . 13 ((𝑃 ∈ Word 𝑉𝑋𝑉𝑄𝑉) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = ((#‘𝑃) + 2))
272267, 268, 270, 271syl3anc 1318 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = ((#‘𝑃) + 2))
273272oveq1d 6564 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1) = (((#‘𝑃) + 2) − 1))
274273oveq2d 6565 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)) = (0..^(((#‘𝑃) + 2) − 1)))
275274raleqdv 3121 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
276265, 275mpbird 246 . . . . . . . 8 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)
277 lswccats1 13263 . . . . . . . . . . . 12 (((𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉𝑄𝑉) → ( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑄)
27810, 277stoic3 1692 . . . . . . . . . . 11 ((𝑃 ∈ Word 𝑉𝑋𝑉𝑄𝑉) → ( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑄)
279267, 268, 270, 278syl3anc 1318 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑄)
2802nngt0d 10941 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘3) → 0 < (𝑁 − 2))
281280, 249syl5ibr 235 . . . . . . . . . . . . . . . 16 ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ‘3) → 0 < (#‘𝑃)))
2822813ad2ant2 1076 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ‘3) → 0 < (#‘𝑃)))
283282com12 32 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 0 < (#‘𝑃)))
2842833ad2ant3 1077 . . . . . . . . . . . . 13 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 0 < (#‘𝑃)))
285284imp 444 . . . . . . . . . . . 12 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → 0 < (#‘𝑃))
286285adantr 480 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 0 < (#‘𝑃))
287 ccat2s1fst 13268 . . . . . . . . . . 11 (((𝑃 ∈ Word 𝑉 ∧ 0 < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0) = (𝑃‘0))
288267, 286, 268, 270, 287syl22anc 1319 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0) = (𝑃‘0))
289279, 288preq12d 4220 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} = {𝑄, (𝑃‘0)})
2901903ad2ant1 1075 . . . . . . . . . . . 12 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑄, 𝑋} ∈ 𝐸))
291290adantr 480 . . . . . . . . . . 11 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑄, 𝑋} ∈ 𝐸))
292291biimpa 500 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑄, 𝑋} ∈ 𝐸)
293 preq2 4213 . . . . . . . . . . . . 13 ((𝑃‘0) = 𝑋 → {𝑄, (𝑃‘0)} = {𝑄, 𝑋})
294293eleq1d 2672 . . . . . . . . . . . 12 ((𝑃‘0) = 𝑋 → ({𝑄, (𝑃‘0)} ∈ 𝐸 ↔ {𝑄, 𝑋} ∈ 𝐸))
2952943ad2ant3 1077 . . . . . . . . . . 11 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ({𝑄, (𝑃‘0)} ∈ 𝐸 ↔ {𝑄, 𝑋} ∈ 𝐸))
296295ad2antlr 759 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ({𝑄, (𝑃‘0)} ∈ 𝐸 ↔ {𝑄, 𝑋} ∈ 𝐸))
297292, 296mpbird 246 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑄, (𝑃‘0)} ∈ 𝐸)
298289, 297eqeltrd 2688 . . . . . . . 8 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸)
29925, 276, 2983jca 1235 . . . . . . 7 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸))
300266ad2antlr 759 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → 𝑃 ∈ Word 𝑉)
3014ad2antrr 758 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → 𝑋𝑉)
302 simpr 476 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → 𝑄𝑉)
303300, 301, 302, 271syl3anc 1318 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = ((#‘𝑃) + 2))
304 oveq1 6556 . . . . . . . . . . . . . . . . . 18 ((#‘𝑃) = (𝑁 − 2) → ((#‘𝑃) + 2) = ((𝑁 − 2) + 2))
305 2cn 10968 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℂ
306 npcan 10169 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑁 − 2) + 2) = 𝑁)
30798, 305, 306sylancl 693 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) + 2) = 𝑁)
308304, 307sylan9eq 2664 . . . . . . . . . . . . . . . . 17 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) + 2) = 𝑁)
309308ex 449 . . . . . . . . . . . . . . . 16 ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ‘3) → ((#‘𝑃) + 2) = 𝑁))
3103093ad2ant2 1076 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ‘3) → ((#‘𝑃) + 2) = 𝑁))
311310com12 32 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((#‘𝑃) + 2) = 𝑁))
3123113ad2ant3 1077 . . . . . . . . . . . . 13 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((#‘𝑃) + 2) = 𝑁))
313312imp 444 . . . . . . . . . . . 12 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → ((#‘𝑃) + 2) = 𝑁)
314313adantr 480 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → ((#‘𝑃) + 2) = 𝑁)
315303, 314eqtrd 2644 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)
316315ex 449 . . . . . . . . 9 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄𝑉 → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
317269, 316syld 46 . . . . . . . 8 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
318317imp 444 . . . . . . 7 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)
319299, 318jca 553 . . . . . 6 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
320319exp31 628 . . . . 5 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))))
3219, 320sylbid 229 . . . 4 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))))
322321com23 84 . . 3 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))))
3233223imp 1249 . 2 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
324 eluzge3nn 11606 . . . . 5 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℕ)
3256, 7isclwwlksnx 41197 . . . . 5 (𝑁 ∈ ℕ → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
326324, 325syl 17 . . . 4 (𝑁 ∈ (ℤ‘3) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
3273263ad2ant3 1077 . . 3 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
3283273ad2ant1 1075 . 2 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
329323, 328mpbird 246 1 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900   ∪ cun 3538  {cpr 4127   class class class wbr 4583  ‘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  Vtxcvtx 25673  Edgcedga 25792   USGraph cusgr 40379   NeighbVtx cnbgr 40550   ClWWalkSN cclwwlksn 41184 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-fal 1481  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-rmo 2904  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-2o 7448  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-cda 8873  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-upgr 25749  df-umgr 25750  df-edga 25793  df-usgr 40381  df-nbgr 40554  df-clwwlks 41185  df-clwwlksn 41186 This theorem is referenced by:  av-numclwlk1lem2foa  41521
 Copyright terms: Public domain W3C validator