Users' Mathboxes 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 41498
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 1053 . . . . . 6 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝐺 ∈ USGraph )
2 uz3m2nn 11565 . . . . . . 7 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℕ)
323ad2ant3 1076 . . . . . 6 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ ℕ)
4 simp2 1054 . . . . . 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 41495 . . . . . 6 ((𝐺 ∈ USGraph ∧ (𝑁 − 2) ∈ ℕ ∧ 𝑋𝑉) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)))
91, 3, 4, 8syl3anc 1317 . . . . 5 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)))
10 ccatws1cl 13197 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word 𝑉𝑋𝑉) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
1110ex 448 . . . . . . . . . . . . . 14 (𝑃 ∈ Word 𝑉 → (𝑋𝑉 → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
12113ad2ant1 1074 . . . . . . . . . . . . 13 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (𝑋𝑉 → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
13123ad2ant1 1074 . . . . . . . . . . . 12 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑋𝑉 → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
1413com12 32 . . . . . . . . . . 11 (𝑋𝑉 → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
15143ad2ant2 1075 . . . . . . . . . 10 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉))
1615imp 443 . . . . . . . . 9 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
176nbgrisvtx 40562 . . . . . . . . . . . . . 14 ((𝐺 ∈ USGraph ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄𝑉)
1817ex 448 . . . . . . . . . . . . 13 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
19 s1cl 13183 . . . . . . . . . . . . 13 (𝑄𝑉 → ⟨“𝑄”⟩ ∈ Word 𝑉)
2018, 19syl6 34 . . . . . . . . . . . 12 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ⟨“𝑄”⟩ ∈ Word 𝑉))
21203ad2ant1 1074 . . . . . . . . . . 11 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ⟨“𝑄”⟩ ∈ Word 𝑉))
2221adantr 479 . . . . . . . . . 10 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ⟨“𝑄”⟩ ∈ Word 𝑉))
2322imp 443 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ⟨“𝑄”⟩ ∈ Word 𝑉)
24 ccatcl 13160 . . . . . . . . 9 (((𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ ⟨“𝑄”⟩ ∈ Word 𝑉) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉)
2516, 23, 24syl2an2r 871 . . . . . . . 8 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉)
26 simpl 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → 𝑃 ∈ Word 𝑉)
2726ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → 𝑃 ∈ Word 𝑉)
2827ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑃 ∈ Word 𝑉)
29 elfzonn0 12337 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 ∈ ℕ0)
3029adantl 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑖 ∈ ℕ0)
31 lencl 13127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℕ0)
32 elfzo0 12333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^((#‘𝑃) − 1)) ↔ (𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)))
33 nn0re 11150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
3433adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → 𝑖 ∈ ℝ)
35 nn0re 11150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((#‘𝑃) ∈ ℕ0 → (#‘𝑃) ∈ ℝ)
36 peano2rem 10199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((#‘𝑃) ∈ ℝ → ((#‘𝑃) − 1) ∈ ℝ)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((#‘𝑃) ∈ ℕ0 → ((#‘𝑃) − 1) ∈ ℝ)
3837adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → ((#‘𝑃) − 1) ∈ ℝ)
3935adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (#‘𝑃) ∈ ℝ)
4034, 38, 393jca 1234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ ∧ (#‘𝑃) ∈ ℝ))
4135ltm1d 10807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((#‘𝑃) ∈ ℕ0 → ((#‘𝑃) − 1) < (#‘𝑃))
4241adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → ((#‘𝑃) − 1) < (#‘𝑃))
43 lttr 9965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ ∧ (#‘𝑃) ∈ ℝ) → ((𝑖 < ((#‘𝑃) − 1) ∧ ((#‘𝑃) − 1) < (#‘𝑃)) → 𝑖 < (#‘𝑃)))
4443expcomd 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ ∧ (#‘𝑃) ∈ ℝ) → (((#‘𝑃) − 1) < (#‘𝑃) → (𝑖 < ((#‘𝑃) − 1) → 𝑖 < (#‘𝑃))))
4540, 42, 44sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (𝑖 < ((#‘𝑃) − 1) → 𝑖 < (#‘𝑃)))
4645impancom 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑖 ∈ ℕ0𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0𝑖 < (#‘𝑃)))
47463adant2 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0𝑖 < (#‘𝑃)))
4832, 47sylbi 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0𝑖 < (#‘𝑃)))
4931, 48syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃)))
5049ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃)))
5150ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃)))
5251imp 443 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑖 < (#‘𝑃))
5328, 30, 523jca 1234 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (#‘𝑃)))
544adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝑋𝑉)
55183ad2ant1 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
5655com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑄𝑉))
5756ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑄𝑉))
5857imp 443 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝑄𝑉)
5954, 58jca 552 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑋𝑉𝑄𝑉))
6059adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑋𝑉𝑄𝑉))
61 ccat2s1fvw 13215 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖) = (𝑃𝑖))
6261eqcomd 2615 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉𝑖 ∈ ℕ0𝑖 < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (𝑃𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖))
6353, 60, 62syl2anc 690 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖))
64 simpl 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑃 ∈ Word 𝑉)
65 peano2nn0 11182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
66653ad2ant1 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)) → (𝑖 + 1) ∈ ℕ0)
6732, 66sylbi 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑖 + 1) ∈ ℕ0)
6867adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑖 + 1) ∈ ℕ0)
69 1red 9911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → 1 ∈ ℝ)
7034, 69, 39ltaddsubd 10478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → ((𝑖 + 1) < (#‘𝑃) ↔ 𝑖 < ((#‘𝑃) − 1)))
7170biimprd 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (𝑖 < ((#‘𝑃) − 1) → (𝑖 + 1) < (#‘𝑃)))
7271impancom 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0 → (𝑖 + 1) < (#‘𝑃)))
73723adant2 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧ 𝑖 < ((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0 → (𝑖 + 1) < (#‘𝑃)))
7432, 73sylbi 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^((#‘𝑃) − 1)) → ((#‘𝑃) ∈ ℕ0 → (𝑖 + 1) < (#‘𝑃)))
7531, 74mpan9 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑖 + 1) < (#‘𝑃))
7664, 68, 753jca 1234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑃 ∈ Word 𝑉𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)))
7776ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))))
7877ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))))
7978ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))))
8079imp 443 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)))
81 ccat2s1fvw 13215 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
8280, 60, 81syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
8382eqcomd 2615 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃‘(𝑖 + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)))
8463, 83preq12d 4219 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → {(𝑃𝑖), (𝑃‘(𝑖 + 1))} = {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))})
8584eleq1d 2671 . . . . . . . . . . . . . . . . . . . 20 (((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → ({(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
8685ralbidva 2967 . . . . . . . . . . . . . . . . . . 19 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
8786biimpd 217 . . . . . . . . . . . . . . . . . 18 ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
8887exp41 635 . . . . . . . . . . . . . . . . 17 (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)))))
8988com15 98 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)))))
9089expd 450 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))))))
91903imp21 1268 . . . . . . . . . . . . . 14 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
92913impib 1253 . . . . . . . . . . . . 13 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
9392impcom 444 . . . . . . . . . . . 12 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
9493imp 443 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)
95 simpll 785 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → 𝑃 ∈ Word 𝑉)
96 oveq1 6533 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((#‘𝑃) = (𝑁 − 2) → ((#‘𝑃) − 1) = ((𝑁 − 2) − 1))
9796adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) = ((𝑁 − 2) − 1))
98 eluzelcn 11533 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℂ)
99 2cnd 10942 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → 2 ∈ ℂ)
100 1cnd 9912 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → 1 ∈ ℂ)
10198, 99, 100subsub4d 10274 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1)))
102 2p1e3 11000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2 + 1) = 3
103102a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘3) → (2 + 1) = 3)
104103oveq2d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3))
105 uznn0sub 11553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → (𝑁 − 3) ∈ ℕ0)
106104, 105eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → (𝑁 − (2 + 1)) ∈ ℕ0)
107101, 106eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) ∈ ℕ0)
108107adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((𝑁 − 2) − 1) ∈ ℕ0)
10997, 108eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . . . . 24 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) ∈ ℕ0)
110109adantll 745 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) ∈ ℕ0)
11131, 41syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) < (#‘𝑃))
112111ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) − 1) < (#‘𝑃))
11395, 110, 1123jca 1234 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ‘3)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))
114113exp31 627 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))))
115114a1dd 47 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))))
1161153ad2ant1 1074 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → (𝑁 ∈ (ℤ‘3) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))))
1171163imp 1248 . . . . . . . . . . . . . . . . . 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 1076 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))
120119imp 443 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))
12118ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ Word 𝑉 ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
122 simpr 475 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → 𝑋𝑉)
123122adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ Word 𝑉 ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉)) → 𝑋𝑉)
124121, 123jctild 563 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ Word 𝑉 ∧ (𝐺 ∈ USGraph ∧ 𝑋𝑉)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉)))
125124ex 448 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉))))
1261253ad2ant1 1074 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉))))
1271263ad2ant1 1074 . . . . . . . . . . . . . . . . . 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 1073 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉𝑄𝑉))))
130129imp31 446 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑋𝑉𝑄𝑉))
131 ccat2s1fvw 13215 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)) = (𝑃‘((#‘𝑃) − 1)))
132120, 130, 131syl2an2r 871 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)) = (𝑃‘((#‘𝑃) − 1)))
133 nn0cn 11151 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝑃) ∈ ℕ0 → (#‘𝑃) ∈ ℂ)
134 ax-1cn 9850 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
135 npcan 10141 . . . . . . . . . . . . . . . . . . . . 21 (((#‘𝑃) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
136133, 134, 135sylancl 692 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝑃) ∈ ℕ0 → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
13731, 136syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ Word 𝑉 → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
1381373ad2ant1 1074 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
1391383ad2ant1 1074 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
140139ad2antlr 758 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((#‘𝑃) − 1) + 1) = (#‘𝑃))
141140fveq2d 6091 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)))
142 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → 𝑃 ∈ Word 𝑉)
143 eqidd 2610 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (#‘𝑃) = (#‘𝑃))
144142, 143jca 552 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)))
145144adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)))
146122ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑋𝑉)
14718ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
148147imp 443 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄𝑉)
149 ccatw2s1p1 13213 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
150145, 146, 148, 149syl12anc 1315 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
151150ex 448 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ USGraph ∧ 𝑋𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋))
152151expcom 449 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
1531523ad2ant1 1074 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
1541533ad2ant1 1074 . . . . . . . . . . . . . . . . . 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 1073 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)))
157156imp31 446 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
158141, 157eqtrd 2643 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1)) = 𝑋)
159132, 158preq12d 4219 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} = {(𝑃‘((#‘𝑃) − 1)), 𝑋})
160 lsw 13152 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
161160adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
162 simpl 471 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → (𝑃‘0) = 𝑋)
163161, 162preq12d 4219 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → {( lastS ‘𝑃), (𝑃‘0)} = {(𝑃‘((#‘𝑃) − 1)), 𝑋})
164163eleq1d 2671 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))
165164biimpd 217 . . . . . . . . . . . . . . . . . . . 20 (((𝑃‘0) = 𝑋𝑃 ∈ Word 𝑉) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))
166165ex 448 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘0) = 𝑋 → (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)))
167166com3l 86 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)))
168167imp 443 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))
1691683adant2 1072 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))
170169a1d 25 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)))
1711703imp 1248 . . . . . . . . . . . . . 14 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)
172171ad2antlr 758 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)
173159, 172eqeltrd 2687 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} ∈ 𝐸)
174 eqid 2609 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (#‘𝑃) = (#‘𝑃)
175174, 149mpanl2 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ Word 𝑉 ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)) = 𝑋)
176 ccatw2s1p2 13214 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1)) = 𝑄)
177174, 176mpanl2 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ Word 𝑉 ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1)) = 𝑄)
178175, 177preq12d 4219 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 ∈ Word 𝑉 ∧ (𝑋𝑉𝑄𝑉)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})
179178expcom 449 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝑉𝑄𝑉) → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))
180179expcom 449 . . . . . . . . . . . . . . . . . . . . . 22 (𝑄𝑉 → (𝑋𝑉 → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
18118, 180syl6 34 . . . . . . . . . . . . . . . . . . . . 21 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋𝑉 → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))))
182181com24 92 . . . . . . . . . . . . . . . . . . . 20 (𝐺 ∈ USGraph → (𝑃 ∈ Word 𝑉 → (𝑋𝑉 → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))))
183182com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ Word 𝑉 → (𝐺 ∈ USGraph → (𝑋𝑉 → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))))
184183impd 445 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
1851843ad2ant1 1074 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
1861853ad2ant1 1074 . . . . . . . . . . . . . . . 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 1073 . . . . . . . . . . . . . 14 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))
189188imp31 446 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})
1907nbusgreledg 40556 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑄, 𝑋} ∈ 𝐸))
191 prcom 4210 . . . . . . . . . . . . . . . . . . 19 {𝑄, 𝑋} = {𝑋, 𝑄}
192191eleq1i 2678 . . . . . . . . . . . . . . . . . 18 ({𝑄, 𝑋} ∈ 𝐸 ↔ {𝑋, 𝑄} ∈ 𝐸)
193192biimpi 204 . . . . . . . . . . . . . . . . 17 ({𝑄, 𝑋} ∈ 𝐸 → {𝑋, 𝑄} ∈ 𝐸)
194190, 193syl6bi 241 . . . . . . . . . . . . . . . 16 (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑄} ∈ 𝐸))
1951943ad2ant1 1074 . . . . . . . . . . . . . . 15 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑄} ∈ 𝐸))
196195adantr 479 . . . . . . . . . . . . . 14 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑄} ∈ 𝐸))
197196imp 443 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑋, 𝑄} ∈ 𝐸)
198189, 197eqeltrd 2687 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} ∈ 𝐸)
199 ovex 6554 . . . . . . . . . . . . 13 ((#‘𝑃) − 1) ∈ V
200 fvex 6097 . . . . . . . . . . . . 13 (#‘𝑃) ∈ V
201 fveq2 6087 . . . . . . . . . . . . . . 15 (𝑖 = ((#‘𝑃) − 1) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)))
202 oveq1 6533 . . . . . . . . . . . . . . . 16 (𝑖 = ((#‘𝑃) − 1) → (𝑖 + 1) = (((#‘𝑃) − 1) + 1))
203202fveq2d 6091 . . . . . . . . . . . . . . 15 (𝑖 = ((#‘𝑃) − 1) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1)))
204201, 203preq12d 4219 . . . . . . . . . . . . . 14 (𝑖 = ((#‘𝑃) − 1) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} = {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))})
205204eleq1d 2671 . . . . . . . . . . . . 13 (𝑖 = ((#‘𝑃) − 1) → ({(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} ∈ 𝐸))
206 fveq2 6087 . . . . . . . . . . . . . . 15 (𝑖 = (#‘𝑃) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)))
207 oveq1 6533 . . . . . . . . . . . . . . . 16 (𝑖 = (#‘𝑃) → (𝑖 + 1) = ((#‘𝑃) + 1))
208207fveq2d 6091 . . . . . . . . . . . . . . 15 (𝑖 = (#‘𝑃) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1)) = (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1)))
209206, 208preq12d 4219 . . . . . . . . . . . . . 14 (𝑖 = (#‘𝑃) → {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} = {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))})
210209eleq1d 2671 . . . . . . . . . . . . 13 (𝑖 = (#‘𝑃) → ({(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} ∈ 𝐸))
211199, 200, 205, 210ralpr 4184 . . . . . . . . . . . 12 (∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) − 1)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(((#‘𝑃) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(#‘𝑃)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘((#‘𝑃) + 1))} ∈ 𝐸))
212173, 198, 211sylanbrc 694 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)
21394, 212jca 552 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
214 2cnd 10942 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((#‘𝑃) ∈ ℕ0 → 2 ∈ ℂ)
215 1cnd 9912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((#‘𝑃) ∈ ℕ0 → 1 ∈ ℂ)
216133, 214, 2153jca 1234 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑃) ∈ ℕ0 → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
21731, 216syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ Word 𝑉 → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
2182173ad2ant1 1074 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
219218adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ))
220 addsubass 10142 . . . . . . . . . . . . . . . . . . . . . 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 10984 . . . . . . . . . . . . . . . . . . . . . 22 (2 − 1) = 1
223222oveq2i 6537 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝑃) + (2 − 1)) = ((#‘𝑃) + 1)
224221, 223syl6eq 2659 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (((#‘𝑃) + 2) − 1) = ((#‘𝑃) + 1))
225224oveq2d 6542 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (0..^(((#‘𝑃) + 2) − 1)) = (0..^((#‘𝑃) + 1)))
226 0zd 11224 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → 0 ∈ ℤ)
22731nn0zd 11314 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℤ)
2282273ad2ant1 1074 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (#‘𝑃) ∈ ℤ)
229228adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (#‘𝑃) ∈ ℤ)
230 eluz2 11527 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁))
231 df-3 10929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 = (2 + 1)
232231breq1i 4584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (3 ≤ 𝑁 ↔ (2 + 1) ≤ 𝑁)
233 2z 11244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2 ∈ ℤ
234 zltp1le 11262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 < 𝑁 ↔ (2 + 1) ≤ 𝑁))
235233, 234mpan 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → (2 < 𝑁 ↔ (2 + 1) ≤ 𝑁))
236235biimprd 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℤ → ((2 + 1) ≤ 𝑁 → 2 < 𝑁))
237232, 236syl5bi 230 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℤ → (3 ≤ 𝑁 → 2 < 𝑁))
238237imp 443 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 2 < 𝑁)
239 zre 11216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
240 2re 10939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℝ
241239, 240jctil 557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℤ → (2 ∈ ℝ ∧ 𝑁 ∈ ℝ))
242241adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (2 ∈ ℝ ∧ 𝑁 ∈ ℝ))
243 posdif 10372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 < 𝑁 ↔ 0 < (𝑁 − 2)))
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (2 < 𝑁 ↔ 0 < (𝑁 − 2)))
245238, 244mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 0 < (𝑁 − 2))
2462453adant1 1071 . . . . . . . . . . . . . . . . . . . . . . . 24 ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 0 < (𝑁 − 2))
247230, 246sylbi 205 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘3) → 0 < (𝑁 − 2))
248247adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → 0 < (𝑁 − 2))
249 breq2 4581 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑃) = (𝑁 − 2) → (0 < (#‘𝑃) ↔ 0 < (𝑁 − 2)))
250249adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → (0 < (#‘𝑃) ↔ 0 < (𝑁 − 2)))
251248, 250mpbird 245 . . . . . . . . . . . . . . . . . . . . 21 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → 0 < (#‘𝑃))
252251adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → 0 < (#‘𝑃))
253 fzosplitprm1 12400 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℤ ∧ (#‘𝑃) ∈ ℤ ∧ 0 < (#‘𝑃)) → (0..^((#‘𝑃) + 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
254226, 229, 252, 253syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (0..^((#‘𝑃) + 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
255225, 254eqtrd 2643 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3))) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
256255expr 640 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2)) → (𝑁 ∈ (ℤ‘3) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
2572563adant3 1073 . . . . . . . . . . . . . . . 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 1076 . . . . . . . . . . . . . 14 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})))
260259imp 443 . . . . . . . . . . . . 13 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
261260adantr 479 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))
262261raleqdv 3120 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
263 ralunb 3755 . . . . . . . . . . 11 (∀𝑖 ∈ ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
264262, 263syl6bb 274 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
265213, 264mpbird 245 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)
266 simp11 1083 . . . . . . . . . . . . . 14 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 𝑃 ∈ Word 𝑉)
267266ad2antlr 758 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑃 ∈ Word 𝑉)
2684ad2antrr 757 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑋𝑉)
26955adantr 479 . . . . . . . . . . . . . 14 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄𝑉))
270269imp 443 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄𝑉)
271 ccatw2s1len 13202 . . . . . . . . . . . . 13 ((𝑃 ∈ Word 𝑉𝑋𝑉𝑄𝑉) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = ((#‘𝑃) + 2))
272267, 268, 270, 271syl3anc 1317 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = ((#‘𝑃) + 2))
273272oveq1d 6541 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1) = (((#‘𝑃) + 2) − 1))
274273oveq2d 6542 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)) = (0..^(((#‘𝑃) + 2) − 1)))
275274raleqdv 3120 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸))
276265, 275mpbird 245 . . . . . . . 8 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸)
277 lswccats1 13211 . . . . . . . . . . . 12 (((𝑃 ++ ⟨“𝑋”⟩) ∈ Word 𝑉𝑄𝑉) → ( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑄)
27810, 277stoic3 1691 . . . . . . . . . . 11 ((𝑃 ∈ Word 𝑉𝑋𝑉𝑄𝑉) → ( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑄)
279267, 268, 270, 278syl3anc 1317 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑄)
2802nngt0d 10913 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘3) → 0 < (𝑁 − 2))
281280, 249syl5ibr 234 . . . . . . . . . . . . . . . 16 ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ‘3) → 0 < (#‘𝑃)))
2822813ad2ant2 1075 . . . . . . . . . . . . . . 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 1076 . . . . . . . . . . . . 13 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 0 < (#‘𝑃)))
285284imp 443 . . . . . . . . . . . 12 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → 0 < (#‘𝑃))
286285adantr 479 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 0 < (#‘𝑃))
287 ccat2s1fst 13216 . . . . . . . . . . 11 (((𝑃 ∈ Word 𝑉 ∧ 0 < (#‘𝑃)) ∧ (𝑋𝑉𝑄𝑉)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0) = (𝑃‘0))
288267, 286, 268, 270, 287syl22anc 1318 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0) = (𝑃‘0))
289279, 288preq12d 4219 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} = {𝑄, (𝑃‘0)})
2901903ad2ant1 1074 . . . . . . . . . . . 12 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑄, 𝑋} ∈ 𝐸))
291290adantr 479 . . . . . . . . . . 11 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑄, 𝑋} ∈ 𝐸))
292291biimpa 499 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑄, 𝑋} ∈ 𝐸)
293 preq2 4212 . . . . . . . . . . . . 13 ((𝑃‘0) = 𝑋 → {𝑄, (𝑃‘0)} = {𝑄, 𝑋})
294293eleq1d 2671 . . . . . . . . . . . 12 ((𝑃‘0) = 𝑋 → ({𝑄, (𝑃‘0)} ∈ 𝐸 ↔ {𝑄, 𝑋} ∈ 𝐸))
2952943ad2ant3 1076 . . . . . . . . . . 11 (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ({𝑄, (𝑃‘0)} ∈ 𝐸 ↔ {𝑄, 𝑋} ∈ 𝐸))
296295ad2antlr 758 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ({𝑄, (𝑃‘0)} ∈ 𝐸 ↔ {𝑄, 𝑋} ∈ 𝐸))
297292, 296mpbird 245 . . . . . . . . 9 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑄, (𝑃‘0)} ∈ 𝐸)
298289, 297eqeltrd 2687 . . . . . . . 8 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸)
29925, 276, 2983jca 1234 . . . . . . 7 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸))
300266ad2antlr 758 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → 𝑃 ∈ Word 𝑉)
3014ad2antrr 757 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → 𝑋𝑉)
302 simpr 475 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → 𝑄𝑉)
303300, 301, 302, 271syl3anc 1317 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = ((#‘𝑃) + 2))
304 oveq1 6533 . . . . . . . . . . . . . . . . . 18 ((#‘𝑃) = (𝑁 − 2) → ((#‘𝑃) + 2) = ((𝑁 − 2) + 2))
305 2cn 10940 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℂ
306 npcan 10141 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑁 − 2) + 2) = 𝑁)
30798, 305, 306sylancl 692 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) + 2) = 𝑁)
308304, 307sylan9eq 2663 . . . . . . . . . . . . . . . . 17 (((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ‘3)) → ((#‘𝑃) + 2) = 𝑁)
309308ex 448 . . . . . . . . . . . . . . . 16 ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ‘3) → ((#‘𝑃) + 2) = 𝑁))
3103093ad2ant2 1075 . . . . . . . . . . . . . . 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 1076 . . . . . . . . . . . . 13 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((#‘𝑃) + 2) = 𝑁))
313312imp 443 . . . . . . . . . . . 12 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → ((#‘𝑃) + 2) = 𝑁)
314313adantr 479 . . . . . . . . . . 11 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → ((#‘𝑃) + 2) = 𝑁)
315303, 314eqtrd 2643 . . . . . . . . . 10 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄𝑉) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)
316315ex 448 . . . . . . . . 9 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄𝑉 → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
317269, 316syld 45 . . . . . . . 8 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
318317imp 443 . . . . . . 7 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)
319299, 318jca 552 . . . . . 6 ((((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
320319exp31 627 . . . . 5 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))))
3219, 320sylbid 228 . . . 4 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))))
322321com23 83 . . 3 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))))
3233223imp 1248 . 2 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁))
324 eluzge3nn 11564 . . . . 5 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℕ)
3256, 7isclwwlksnx 41178 . . . . 5 (𝑁 ∈ ℕ → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
326324, 325syl 17 . . . 4 (𝑁 ∈ (ℤ‘3) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
3273263ad2ant3 1076 . . 3 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
3283273ad2ant1 1074 . 2 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) − 1)){(((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘𝑖), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)), (((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩)) = 𝑁)))
329323, 328mpbird 245 1 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑃 ++ ⟨“𝑋”⟩) ++ ⟨“𝑄”⟩) ∈ (𝑁 ClWWalkSN 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895  {crab 2899  cun 3537  {cpr 4126   class class class wbr 4577  cfv 5789  (class class class)co 6526  cmpt2 6528  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   < clt 9930  cle 9931  cmin 10117  cn 10869  2c2 10919  3c3 10920  0cn0 11141  cz 11212  cuz 11521  ..^cfzo 12291  #chash 12936  Word cword 13094   lastS clsw 13095   ++ cconcat 13096  ⟨“cs1 13097  Vtxcvtx 40210  Edgcedga 40332   USGraph cusgr 40360   NeighbVtx cnbgr 40531   ClWWalkSN cclwwlksn 41165
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10870  df-2 10928  df-3 10929  df-n0 11142  df-z 11213  df-uz 11522  df-rp 11667  df-fz 12155  df-fzo 12292  df-hash 12937  df-word 13102  df-lsw 13103  df-concat 13104  df-s1 13105  df-upgr 40289  df-umgr 40290  df-edga 40333  df-usgr 40362  df-nbgr 40535  df-clwwlks 41166  df-clwwlksn 41167
This theorem is referenced by:  av-numclwlk1lem2foa  41502
  Copyright terms: Public domain W3C validator