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

Theorem clwlksfclwwlkOLD 27243
Description: Obsolete version of clwlkclwwlkf 27158 as of 23-May-2022. (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
clwlksfclwwlk.1 𝐴 = (1st𝑐)
clwlksfclwwlk.2 𝐵 = (2nd𝑐)
clwlksfclwwlk.c 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘𝐴) = 𝑁}
clwlksfclwwlk.f 𝐹 = (𝑐𝐶 ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩))
Assertion
Ref Expression
clwlksfclwwlkOLD ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺))
Distinct variable groups:   𝐺,𝑐   𝑁,𝑐   𝐶,𝑐
Allowed substitution hints:   𝐴(𝑐)   𝐵(𝑐)   𝐹(𝑐)

Proof of Theorem clwlksfclwwlkOLD
Dummy variables 𝑖 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 clwlksfclwwlk.c . . . . . 6 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘𝐴) = 𝑁}
21rabeq2i 3347 . . . . 5 (𝑐𝐶 ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁))
3 fusgrusgr 26437 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
4 usgrupgr 26299 . . . . . . . . . . . 12 (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
53, 4syl 17 . . . . . . . . . . 11 (𝐺 ∈ FinUSGraph → 𝐺 ∈ UPGraph)
65adantr 466 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ UPGraph)
7 eqid 2771 . . . . . . . . . . 11 (Vtx‘𝐺) = (Vtx‘𝐺)
8 eqid 2771 . . . . . . . . . . 11 (iEdg‘𝐺) = (iEdg‘𝐺)
9 clwlksfclwwlk.1 . . . . . . . . . . 11 𝐴 = (1st𝑐)
10 clwlksfclwwlk.2 . . . . . . . . . . 11 𝐵 = (2nd𝑐)
117, 8, 9, 10upgrclwlkcompim 26912 . . . . . . . . . 10 ((𝐺 ∈ UPGraph ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
126, 11sylan 569 . . . . . . . . 9 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
13 lencl 13520 . . . . . . . . . . . . . . 15 (𝐴 ∈ Word dom (iEdg‘𝐺) → (♯‘𝐴) ∈ ℕ0)
14 clwlksfclwwlk.f . . . . . . . . . . . . . . . . . . . . . . . 24 𝐹 = (𝑐𝐶 ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩))
159, 10, 1, 14clwlksfclwwlk2wrdOLD 27239 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝐶𝐵 ∈ Word (Vtx‘𝐺))
1615ad2antlr 706 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
17 swrdcl 13627 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ∈ Word (Vtx‘𝐺) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺))
1816, 17syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺))
19 ffz0iswrd 13528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → 𝐵 ∈ Word (Vtx‘𝐺))
20193ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
21 prmnn 15595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℙ → 𝑁 ∈ ℕ)
2221adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ)
23223ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ)
24 oveq2 6801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((♯‘𝐴) = 𝑁 → (0...(♯‘𝐴)) = (0...𝑁))
2524feq2d 6171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((♯‘𝐴) = 𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ↔ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)))
2622nnnn0d 11553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ0)
27 ffz0hash 13433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑁 ∈ ℕ0𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1))
2826, 27sylan 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1))
2928ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → (♯‘𝐵) = (𝑁 + 1)))
3021nnred 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑁 ∈ ℙ → 𝑁 ∈ ℝ)
3130adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ∈ ℝ)
3231lep1d 11157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (𝑁 + 1))
33 breq2 4790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((♯‘𝐵) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
3433adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
3532, 34mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (♯‘𝐵))
3635ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 ∈ ℙ → ((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵)))
3736adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → ((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵)))
3829, 37syldc 48 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵)))
3925, 38syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝐴) = 𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵))))
40393imp21 1105 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ≤ (♯‘𝐵))
41 swrdn0 13639 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝐵)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
4220, 23, 40, 41syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
43 opeq2 4540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((♯‘𝐴) = 𝑁 → ⟨0, (♯‘𝐴)⟩ = ⟨0, 𝑁⟩)
4443oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) = (𝐵 substr ⟨0, 𝑁⟩))
4544neeq1d 3002 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((♯‘𝐴) = 𝑁 → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
46453ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
4742, 46mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)
48473exp 1112 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)))
4948ad2antlr 706 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)))
5049imp 393 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
5150adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
5251imp 393 . . . . . . . . . . . . . . . . . . . . 21 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)
5318, 52jca 501 . . . . . . . . . . . . . . . . . . . 20 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
54 simp-5r 774 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → 𝐴 ∈ Word dom (iEdg‘𝐺))
553adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ USGraph)
5654, 55anim12ci 601 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)))
57 simp-5r 774 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺))
58 prmuz2 15615 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℙ → 𝑁 ∈ (ℤ‘2))
59 ffz0hash 13433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((♯‘𝐴) ∈ ℕ0𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1))
6059adantlr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1))
61 eluz2 11894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((♯‘𝐴) ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)))
62 2re 11292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2 ∈ ℝ
6362a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((♯‘𝐴) ∈ ℤ → 2 ∈ ℝ)
64 zre 11583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ ℝ)
65 peano2re 10411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((♯‘𝐴) ∈ ℝ → ((♯‘𝐴) + 1) ∈ ℝ)
6664, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) + 1) ∈ ℝ)
6763, 64, 663jca 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → (2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ))
6867adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ))
69 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ (♯‘𝐴))
7064lep1d 11157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ≤ ((♯‘𝐴) + 1))
7170adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (♯‘𝐴) ≤ ((♯‘𝐴) + 1))
72 letr 10333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) → ((2 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ ((♯‘𝐴) + 1)) → 2 ≤ ((♯‘𝐴) + 1)))
7372imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) ∧ (2 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ ((♯‘𝐴) + 1))) → 2 ≤ ((♯‘𝐴) + 1))
7468, 69, 71, 73syl12anc 1474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ ((♯‘𝐴) + 1))
75743adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((2 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ ((♯‘𝐴) + 1))
7661, 75sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((♯‘𝐴) ∈ (ℤ‘2) → 2 ≤ ((♯‘𝐴) + 1))
7776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → ((♯‘𝐴) ∈ (ℤ‘2) → 2 ≤ ((♯‘𝐴) + 1)))
78 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 = (♯‘𝐴) → (𝑁 ∈ (ℤ‘2) ↔ (♯‘𝐴) ∈ (ℤ‘2)))
7978eqcoms 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) ↔ (♯‘𝐴) ∈ (ℤ‘2)))
8079adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ‘2) ↔ (♯‘𝐴) ∈ (ℤ‘2)))
81 breq2 4790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((♯‘𝐵) = ((♯‘𝐴) + 1) → (2 ≤ (♯‘𝐵) ↔ 2 ≤ ((♯‘𝐴) + 1)))
8281adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (2 ≤ (♯‘𝐵) ↔ 2 ≤ ((♯‘𝐴) + 1)))
8377, 80, 823imtr4d 283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵)))
8483ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((♯‘𝐵) = ((♯‘𝐴) + 1) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵))))
8560, 84syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵))))
8685adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵))))
8786imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵)))
8887adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵)))
8958, 88syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℙ → (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → 2 ≤ (♯‘𝐵)))
9089adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → 2 ≤ (♯‘𝐵)))
9190impcom 394 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 2 ≤ (♯‘𝐵))
92 simp-4r 770 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
937, 8usgrf 26272 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ USGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2})
9493anim1i 602 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2} ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)))
95 clwlkclwwlklem2 27150 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2} ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (♯‘𝐵)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))
9694, 95syl3an1 1166 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (♯‘𝐵)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))
97 biid 251 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((lastS‘𝐵) = (𝐵‘0) ↔ (lastS‘𝐵) = (𝐵‘0))
98 edgval 26162 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Edg‘𝐺) = ran (iEdg‘𝐺)
9998eleq2i 2842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))
10099ralbii 3129 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))
10198eleq2i 2842 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺) ↔ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))
10297, 100, 1013anbi123i 1158 . . . . . . . . . . . . . . . . . . . . . . . 24 (((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))
10396, 102sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (♯‘𝐵)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)))
10456, 57, 91, 92, 103syl121anc 1481 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)))
1059, 10, 1, 14clwlksfclwwlk1hashOLD 27241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐𝐶 → (♯‘𝐴) ∈ (0...(♯‘𝐵)))
106 simp2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝐵 ∈ Word (Vtx‘𝐺))
107 simp1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (♯‘𝐴) ∈ (0...(♯‘𝐵)))
108 elfzelz 12549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (♯‘𝐴) ∈ ℤ)
109 peano2zm 11622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) − 1) ∈ ℤ)
110 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ ℤ)
11164lem1d 11159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) − 1) ≤ (♯‘𝐴))
112 eluz2 11894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)) ↔ (((♯‘𝐴) − 1) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴)))
113109, 110, 111, 112syl3anbrc 1428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)))
114 fzoss2 12704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
115108, 113, 1143syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
116115sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈ (0..^(♯‘𝐴)))
1171163adant2 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈ (0..^(♯‘𝐴)))
118 swrd0fv 13648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖) = (𝐵𝑖))
119106, 107, 117, 118syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖) = (𝐵𝑖))
120119eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵𝑖) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖))
121 elfzom1elp1fzo 12743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((♯‘𝐴) ∈ ℤ ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
122108, 121sylan 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
1231223adant2 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
124 swrd0fv 13648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)) = (𝐵‘(𝑖 + 1)))
125124eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)))
126106, 107, 123, 125syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)))
127120, 126preq12d 4412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})
1281273exp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → (𝑖 ∈ (0..^((♯‘𝐴) − 1)) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})))
129105, 15, 128sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐𝐶 → (𝑖 ∈ (0..^((♯‘𝐴) − 1)) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))}))
130129imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐𝐶𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})
131130eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝐶𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
132131ralbidva 3134 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐𝐶 → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
133132ad2antlr 706 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
1349, 10, 1, 14clwlksfclwwlk2sswdOLD 27242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐𝐶 → (♯‘𝐴) = (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)))
135134oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐𝐶 → ((♯‘𝐴) − 1) = ((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1))
136135ad2antlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((♯‘𝐴) − 1) = ((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1))
137136oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (0..^((♯‘𝐴) − 1)) = (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)))
138137raleqdv 3293 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
139133, 138bitrd 268 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
140 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ ↔ (♯‘𝐴) ∈ ℙ))
141140biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ → (♯‘𝐴) ∈ ℙ))
142141eqcoms 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((♯‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (♯‘𝐴) ∈ ℙ))
143 prmnn 15595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((♯‘𝐴) ∈ ℙ → (♯‘𝐴) ∈ ℕ)
144 elfz2nn0 12638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)))
145 1zzd 11610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → 1 ∈ ℤ)
146 nn0z 11602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((♯‘𝐵) ∈ ℕ0 → (♯‘𝐵) ∈ ℤ)
147146adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → (♯‘𝐵) ∈ ℤ)
148 nn0z 11602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((♯‘𝐴) ∈ ℕ0 → (♯‘𝐴) ∈ ℤ)
149148adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → (♯‘𝐴) ∈ ℤ)
150145, 147, 1493jca 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
1511503adant3 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
152151adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
153 simp3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))
154 nnge1 11248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((♯‘𝐴) ∈ ℕ → 1 ≤ (♯‘𝐴))
155153, 154anim12ci 601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵)))
156152, 155jca 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
157144, 156sylanb 570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
158 elfz2 12540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ (1...(♯‘𝐵)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
159157, 158sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (♯‘𝐴) ∈ (1...(♯‘𝐵)))
160 swrd0fvlsw 13652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = (𝐵‘((♯‘𝐴) − 1)))
161160eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (𝐵‘((♯‘𝐴) − 1)) = (lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)))
162 swrd0fv0 13649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0) = (𝐵‘0))
163162eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (𝐵‘0) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0))
164161, 163preq12d 4412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})
165164expcom 398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐴) ∈ (1...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
166159, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
167166ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → ((♯‘𝐴) ∈ ℕ → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
168167com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → ((♯‘𝐴) ∈ ℕ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
169105, 15, 168sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐𝐶 → ((♯‘𝐴) ∈ ℕ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
170143, 169syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((♯‘𝐴) ∈ ℙ → (𝑐𝐶 → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
171142, 170syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((♯‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (𝑐𝐶 → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
172171com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
173172adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
174173imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
175174com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℙ → (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
176175adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
177176impcom 394 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})
178177eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ({(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺) ↔ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
179139, 1783anbi23d 1550 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺))))
180104, 179mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
181 3simpc 1146 . . . . . . . . . . . . . . . . . . . . 21 (((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)) → (∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
182180, 181syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
183 3anass 1080 . . . . . . . . . . . . . . . . . . . 20 ((((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)) ↔ (((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅) ∧ (∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺))))
18453, 182, 183sylanbrc 572 . . . . . . . . . . . . . . . . . . 19 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
185 eqid 2771 . . . . . . . . . . . . . . . . . . . 20 (Edg‘𝐺) = (Edg‘𝐺)
1867, 185isclwwlk 27134 . . . . . . . . . . . . . . . . . . 19 ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (ClWWalks‘𝐺) ↔ (((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
187184, 186sylibr 224 . . . . . . . . . . . . . . . . . 18 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (ClWWalks‘𝐺))
188134eqeq1d 2773 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐𝐶 → ((♯‘𝐴) = 𝑁 ↔ (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
189188biimpcd 239 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
190189adantl 467 . . . . . . . . . . . . . . . . . . . 20 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐𝐶 → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
191190imp 393 . . . . . . . . . . . . . . . . . . 19 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁)
192191adantr 466 . . . . . . . . . . . . . . . . . 18 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁)
193 isclwwlkn 27180 . . . . . . . . . . . . . . . . . 18 ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (ClWWalks‘𝐺) ∧ (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
194187, 192, 193sylanbrc 572 . . . . . . . . . . . . . . . . 17 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))
195194exp31 406 . . . . . . . . . . . . . . . 16 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
196195exp41 421 . . . . . . . . . . . . . . 15 (((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))))
19713, 196mpancom 668 . . . . . . . . . . . . . 14 (𝐴 ∈ Word dom (iEdg‘𝐺) → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))))
198197imp 393 . . . . . . . . . . . . 13 ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))))
1991983impib 1108 . . . . . . . . . . . 12 (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
200199com12 32 . . . . . . . . . . 11 ((♯‘𝐴) = 𝑁 → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
201200com14 96 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
202201adantr 466 . . . . . . . . 9 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
20312, 202mpd 15 . . . . . . . 8 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (𝑐𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
204203expcom 398 . . . . . . 7 (𝑐 ∈ (ClWalks‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝑐𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
205204com24 95 . . . . . 6 (𝑐 ∈ (ClWalks‘𝐺) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
206205imp 393 . . . . 5 ((𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁) → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
2072, 206sylbi 207 . . . 4 (𝑐𝐶 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
208207pm2.43i 52 . . 3 (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))
209208impcom 394 . 2 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐𝐶) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))
210209, 14fmptd 6527 1 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  {crab 3065  cdif 3720  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316  {cpr 4318  cop 4322   class class class wbr 4786  cmpt 4863  dom cdm 5249  ran crn 5250  wf 6027  1-1wf1 6028  cfv 6031  (class class class)co 6793  1st c1st 7313  2nd c2nd 7314  cr 10137  0cc0 10138  1c1 10139   + caddc 10141  cle 10277  cmin 10468  cn 11222  2c2 11272  0cn0 11494  cz 11579  cuz 11888  ...cfz 12533  ..^cfzo 12673  chash 13321  Word cword 13487  lastSclsw 13488   substr csubstr 13491  cprime 15592  Vtxcvtx 26095  iEdgciedg 26096  Edgcedg 26160  UPGraphcupgr 26196  USGraphcusgr 26266  FinUSGraphcfusgr 26431  ClWalkscclwlks 26901  ClWWalkscclwwlk 27131   ClWWalksN cclwwlkn 27174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-ifp 1050  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-xnn0 11566  df-z 11580  df-uz 11889  df-rp 12036  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-word 13495  df-lsw 13496  df-substr 13499  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-dvds 15190  df-prm 15593  df-edg 26161  df-uhgr 26174  df-upgr 26198  df-uspgr 26267  df-usgr 26268  df-fusgr 26432  df-wlks 26730  df-clwlks 26902  df-clwwlk 27132  df-clwwlkn 27176
This theorem is referenced by:  clwlksfoclwwlkOLD  27244  clwlksf1clwwlkOLD  27250
  Copyright terms: Public domain W3C validator