clwlksfclwwlkOLD - Metamath Proof Explorer

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

Theorem clwlksfclwwlkOLD 27357

Description: Obsolete version of clwlkclwwlkf 27263 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
clwlksfclwwlkOLD.1	⊢ 𝐴 = (1^st ‘𝑐)
clwlksfclwwlkOLD.2	⊢ 𝐵 = (2^nd ‘𝑐)
clwlksfclwwlkOLD.c	⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘𝐴) = 𝑁}
clwlksfclwwlkOLD.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.

Step	Hyp	Ref	Expression
1		clwlksfclwwlkOLD.c	. . . . . 6 ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘𝐴) = 𝑁}
2	1	rabeq2i 3346	. . . . 5 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁))
3		fusgrusgr 26509	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
4		usgrupgr 26371	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
5	3, 4	syl 17	. . . . . . . . . . 11 ⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ UPGraph)
6	5	adantr 472	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ UPGraph)
7		eqid 2765	. . . . . . . . . . 11 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
8		eqid 2765	. . . . . . . . . . 11 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
9		clwlksfclwwlkOLD.1	. . . . . . . . . . 11 ⊢ 𝐴 = (1^st ‘𝑐)
10		clwlksfclwwlkOLD.2	. . . . . . . . . . 11 ⊢ 𝐵 = (2^nd ‘𝑐)
11	7, 8, 9, 10	upgrclwlkcompim 26989	. . . . . . . . . 10 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
12	6, 11	sylan 575	. . . . . . . . 9 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
13		lencl 13512	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word dom (iEdg‘𝐺) → (♯‘𝐴) ∈ ℕ₀)
14		clwlksfclwwlkOLD.f	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩))
15	9, 10, 1, 14	clwlksfclwwlk2wrdOLD 27353	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ 𝐶 → 𝐵 ∈ Word (Vtx‘𝐺))
16	15	ad2antlr 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
17		swrdcl 13629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺))
18	16, 17	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺))
19		ffz0iswrd 13520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → 𝐵 ∈ Word (Vtx‘𝐺))
20	19	3ad2ant1 1163	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
21		prmnn 15684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑁 ∈ ℙ → 𝑁 ∈ ℕ)
22	21	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ)
23	22	3ad2ant3 1165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ)
24		oveq2 6854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐴) = 𝑁 → (0...(♯‘𝐴)) = (0...𝑁))
25	24	feq2d 6211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐴) = 𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ↔ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)))
26	22	nnnn0d 11603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ₀)
27		ffz0hash 13439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1))
28	26, 27	sylan 575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1))
29	28	ex 401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → (♯‘𝐵) = (𝑁 + 1)))
30	21	nnred 11296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑁 ∈ ℙ → 𝑁 ∈ ℝ)
31	30	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ∈ ℝ)
32	31	lep1d 11214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (𝑁 + 1))
33		breq2 4815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((♯‘𝐵) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
34	33	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
35	32, 34	mpbird 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (♯‘𝐵))
36	35	ex 401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑁 ∈ ℙ → ((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵)))
37	36	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → ((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵)))
38	29, 37	syldc 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵)))
39	25, 38	syl6bi 244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐴) = 𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵))))
40	39	3imp21 1141	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ≤ (♯‘𝐵))
41		swrdn0OLD 13641	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝐵)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
42	20, 23, 40, 41	syl3anc 1490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
43		opeq2 4562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐴) = 𝑁 → ⟨0, (♯‘𝐴)⟩ = ⟨0, 𝑁⟩)
44	43	oveq2d 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) = (𝐵 substr ⟨0, 𝑁⟩))
45	44	neeq1d 2996	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝐴) = 𝑁 → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
46	45	3ad2ant2 1164	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
47	42, 46	mpbird 248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)
48	47	3exp 1148	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)))
49	48	ad2antlr 718	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)))
50	49	imp 395	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
51	50	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
52	51	imp 395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)
53	18, 52	jca 507	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
54		simp-5r 807	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 𝐴 ∈ Word dom (iEdg‘𝐺))
55	3	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ USGraph)
56	54, 55	anim12ci 607	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)))
57		simp-5r 807	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺))
58		prmuz2 15704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℙ → 𝑁 ∈ (ℤ_≥‘2))
59		ffz0hash 13439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1))
60	59	adantlr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1))
61		eluz2 11899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)))
62		2re 11351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 2 ∈ ℝ
63	62	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((♯‘𝐴) ∈ ℤ → 2 ∈ ℝ)
64		zre 11633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ ℝ)
65		peano2re 10468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((♯‘𝐴) ∈ ℝ → ((♯‘𝐴) + 1) ∈ ℝ)
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) + 1) ∈ ℝ)
67	63, 64, 66	3jca 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ ℤ → (2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ))
68	67	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ))
69		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ (♯‘𝐴))
70	64	lep1d 11214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ≤ ((♯‘𝐴) + 1))
71	70	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (♯‘𝐴) ≤ ((♯‘𝐴) + 1))
72		letr 10390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) → ((2 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ ((♯‘𝐴) + 1)) → 2 ≤ ((♯‘𝐴) + 1)))
73	72	imp 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) ∧ (2 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ ((♯‘𝐴) + 1))) → 2 ≤ ((♯‘𝐴) + 1))
74	68, 69, 71, 73	syl12anc 865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ ((♯‘𝐴) + 1))
75	74	3adant1 1160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((2 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ ((♯‘𝐴) + 1))
76	61, 75	sylbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘2) → 2 ≤ ((♯‘𝐴) + 1))
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → ((♯‘𝐴) ∈ (ℤ_≥‘2) → 2 ≤ ((♯‘𝐴) + 1)))
78		eleq1 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 = (♯‘𝐴) → (𝑁 ∈ (ℤ_≥‘2) ↔ (♯‘𝐴) ∈ (ℤ_≥‘2)))
79	78	eqcoms 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ_≥‘2) ↔ (♯‘𝐴) ∈ (ℤ_≥‘2)))
80	79	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ_≥‘2) ↔ (♯‘𝐴) ∈ (ℤ_≥‘2)))
81		breq2 4815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝐵) = ((♯‘𝐴) + 1) → (2 ≤ (♯‘𝐵) ↔ 2 ≤ ((♯‘𝐴) + 1)))
82	81	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (2 ≤ (♯‘𝐵) ↔ 2 ≤ ((♯‘𝐴) + 1)))
83	77, 80, 82	3imtr4d 285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵)))
84	83	ex 401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐵) = ((♯‘𝐴) + 1) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵))))
85	60, 84	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵))))
86	85	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵))))
87	86	imp 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵)))
88	87	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵)))
89	58, 88	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℙ → (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (♯‘𝐵)))
90	89	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (♯‘𝐵)))
91	90	impcom 396	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 2 ≤ (♯‘𝐵))
92		simp-4r 803	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
93	7, 8	usgrf 26344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐺 ∈ USGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2})
94	93	anim1i 608	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2} ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)))
95		clwlkclwwlklem2 27247	. . . . . . . . . . . . . . . . . . . . . . . . 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‘𝐺)))
96	94, 95	syl3an1 1202	. . . . . . . . . . . . . . . . . . . . . . . 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 252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((lastS‘𝐵) = (𝐵‘0) ↔ (lastS‘𝐵) = (𝐵‘0))
98		edgval 26234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
99	98	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))
100	99	ralbii 3127	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))
101	98	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺) ↔ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))
102	97, 100, 101	3anbi123i 1194	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))
103	96, 102	sylibr 225	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (♯‘𝐵)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)))
104	56, 57, 91, 92, 103	syl121anc 1494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)))
105	9, 10, 1, 14	clwlksfclwwlk1hashOLD 27355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 ∈ 𝐶 → (♯‘𝐴) ∈ (0...(♯‘𝐵)))
106		simp2 1167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝐵 ∈ Word (Vtx‘𝐺))
107		simp1 1166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (♯‘𝐴) ∈ (0...(♯‘𝐵)))
108		elfzelz 12556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (♯‘𝐴) ∈ ℤ)
109		peano2zm 11673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) − 1) ∈ ℤ)
110		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ ℤ)
111	64	lem1d 11216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) − 1) ≤ (♯‘𝐴))
112		eluz2 11899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘((♯‘𝐴) − 1)) ↔ (((♯‘𝐴) − 1) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴)))
113	109, 110, 111, 112	syl3anbrc 1443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ (ℤ_≥‘((♯‘𝐴) − 1)))
114		fzoss2 12711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘((♯‘𝐴) − 1)) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
115	108, 113, 114	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
116	115	sselda 3763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈ (0..^(♯‘𝐴)))
117	116	3adant2 1161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈ (0..^(♯‘𝐴)))
118		swrd0fvOLD 13652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖) = (𝐵‘𝑖))
119	106, 107, 117, 118	syl3anc 1490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖) = (𝐵‘𝑖))
120	119	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵‘𝑖) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖))
121		elfzom1elp1fzo 12750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
122	108, 121	sylan 575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
123	122	3adant2 1161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
124		swrd0fvOLD 13652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)) = (𝐵‘(𝑖 + 1)))
125	124	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)))
126	106, 107, 123, 125	syl3anc 1490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)))
127	120, 126	preq12d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})
128	127	3exp 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → (𝑖 ∈ (0..^((♯‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})))
129	105, 15, 128	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝐶 → (𝑖 ∈ (0..^((♯‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))}))
130	129	imp 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})
131	130	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
132	131	ralbidva 3132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ∈ 𝐶 → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
133	132	ad2antlr 718	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
134	9, 10, 1, 14	clwlksfclwwlk2sswdOLD 27356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝐶 → (♯‘𝐴) = (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)))
135	134	oveq1d 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝐶 → ((♯‘𝐴) − 1) = ((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1))
136	135	ad2antlr 718	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((♯‘𝐴) − 1) = ((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1))
137	136	oveq2d 6862	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (0..^((♯‘𝐴) − 1)) = (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)))
138	137	raleqdv 3292	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ 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‘𝐺)))
139	133, 138	bitrd 270	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ 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 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ ↔ (♯‘𝐴) ∈ ℙ))
141	140	biimpd 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ → (♯‘𝐴) ∈ ℙ))
142	141	eqcoms 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (♯‘𝐴) ∈ ℙ))
143		prmnn 15684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((♯‘𝐴) ∈ ℙ → (♯‘𝐴) ∈ ℕ)
144		elfz2nn0 12645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((♯‘𝐴) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)))
145		1zzd 11661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → 1 ∈ ℤ)
146		nn0z 11653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((♯‘𝐵) ∈ ℕ₀ → (♯‘𝐵) ∈ ℤ)
147	146	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → (♯‘𝐵) ∈ ℤ)
148		nn0z 11653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((♯‘𝐴) ∈ ℕ₀ → (♯‘𝐴) ∈ ℤ)
149	148	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → (♯‘𝐴) ∈ ℤ)
150	145, 147, 149	3jca 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
151	150	3adant3 1162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
152	151	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
153		simp3 1168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))
154		nnge1 11308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((♯‘𝐴) ∈ ℕ → 1 ≤ (♯‘𝐴))
155	153, 154	anim12ci 607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵)))
156	152, 155	jca 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
157	144, 156	sylanb 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
158		elfz2 12547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ (1...(♯‘𝐵)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
159	157, 158	sylibr 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (♯‘𝐴) ∈ (1...(♯‘𝐵)))
160		swrd0fvlswOLD 13656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = (𝐵‘((♯‘𝐴) − 1)))
161	160	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (𝐵‘((♯‘𝐴) − 1)) = (lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)))
162		swrd0fv0OLD 13653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0) = (𝐵‘0))
163	162	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (𝐵‘0) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0))
164	161, 163	preq12d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})
165	164	expcom 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((♯‘𝐴) ∈ (1...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
166	159, 165	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
167	166	ex 401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → ((♯‘𝐴) ∈ ℕ → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
168	167	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → ((♯‘𝐴) ∈ ℕ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
169	105, 15, 168	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 ∈ 𝐶 → ((♯‘𝐴) ∈ ℕ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
170	143, 169	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐴) ∈ ℙ → (𝑐 ∈ 𝐶 → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
171	142, 170	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (𝑐 ∈ 𝐶 → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
172	171	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
173	172	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
174	173	imp 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
175	174	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℙ → (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
176	175	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
177	176	impcom 396	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})
178	177	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ({(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺) ↔ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
179	139, 178	3anbi23d 1563	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ 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‘𝐺))))
180	104, 179	mpbid 223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ 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 1182	. . . . . . . . . . . . . . . . . . . . 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‘𝐺)))
182	180, 181	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ 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 1116	. . . . . . . . . . . . . . . . . . . 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‘𝐺))))
184	53, 182, 183	sylanbrc 578	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ 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 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
186	7, 185	isclwwlk 27231	. . . . . . . . . . . . . . . . . . 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‘𝐺)))
187	184, 186	sylibr 225	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (ClWWalks‘𝐺))
188	134	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 ↔ (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
189	188	biimpcd 240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
190	189	adantl 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
191	190	imp 395	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁)
192	191	adantr 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁)
193		isclwwlkn 27286	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (ClWWalks‘𝐺) ∧ (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
194	187, 192, 193	sylanbrc 578	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))
195	194	exp31 410	. . . . . . . . . . . . . . . 16 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
196	195	exp41 425	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))))
197	13, 196	mpancom 679	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Word dom (iEdg‘𝐺) → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))))
198	197	imp 395	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))))
199	198	3impib 1144	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
200	199	com12 32	. . . . . . . . . . 11 ⊢ ((♯‘𝐴) = 𝑁 → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
201	200	com14 96	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
202	201	adantr 472	. . . . . . . . 9 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
203	12, 202	mpd 15	. . . . . . . 8 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
204	203	expcom 402	. . . . . . 7 ⊢ (𝑐 ∈ (ClWalks‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
205	204	com24 95	. . . . . 6 ⊢ (𝑐 ∈ (ClWalks‘𝐺) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
206	205	imp 395	. . . . 5 ⊢ ((𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
207	2, 206	sylbi 208	. . . 4 ⊢ (𝑐 ∈ 𝐶 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
208	207	pm2.43i 52	. . 3 ⊢ (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))
209	208	impcom 396	. 2 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ 𝐶) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))
210	209, 14	fmptd 6578	1 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 ∧ w3a 1107 = wceq 1652 ∈ wcel 2155 ≠ wne 2937 ∀wral 3055 {crab 3059 ∖ cdif 3731 ⊆ wss 3734 ∅c0 4081 𝒫 cpw 4317 {csn 4336 {cpr 4338 ⟨cop 4342 class class class wbr 4811 ↦ cmpt 4890 dom cdm 5279 ran crn 5280 ⟶wf 6066 –1-1→wf1 6067 ‘cfv 6070 (class class class)co 6846 1^st c1st 7368 2^nd c2nd 7369 ℝcr 10192 0cc0 10193 1c1 10194 + caddc 10196 ≤ cle 10333 − cmin 10525 ℕcn 11279 2c2 11332 ℕ₀cn0 11543 ℤcz 11629 ℤ_≥cuz 11893 ...cfz 12540 ..^cfzo 12680 ♯chash 13328 Word cword 13493 lastSclsw 13541 substr csubstr 13624 ℙcprime 15681 Vtxcvtx 26181 iEdgciedg 26182 Edgcedg 26232 UPGraphcupgr 26268 USGraphcusgr 26338 FinUSGraphcfusgr 26503 ClWalkscclwlks 26978 ClWWalkscclwwlk 27228 ClWWalksN cclwwlkn 27280

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4932 ax-sep 4943 ax-nul 4951 ax-pow 5003 ax-pr 5064 ax-un 7151 ax-cnex 10249 ax-resscn 10250 ax-1cn 10251 ax-icn 10252 ax-addcl 10253 ax-addrcl 10254 ax-mulcl 10255 ax-mulrcl 10256 ax-mulcom 10257 ax-addass 10258 ax-mulass 10259 ax-distr 10260 ax-i2m1 10261 ax-1ne0 10262 ax-1rid 10263 ax-rnegex 10264 ax-rrecex 10265 ax-cnre 10266 ax-pre-lttri 10267 ax-pre-lttrn 10268 ax-pre-ltadd 10269 ax-pre-mulgt0 10270 ax-pre-sup 10271

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-ifp 1086 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3599 df-csb 3694 df-dif 3737 df-un 3739 df-in 3741 df-ss 3748 df-pss 3750 df-nul 4082 df-if 4246 df-pw 4319 df-sn 4337 df-pr 4339 df-tp 4341 df-op 4343 df-uni 4597 df-int 4636 df-iun 4680 df-br 4812 df-opab 4874 df-mpt 4891 df-tr 4914 df-id 5187 df-eprel 5192 df-po 5200 df-so 5201 df-fr 5238 df-we 5240 df-xp 5285 df-rel 5286 df-cnv 5287 df-co 5288 df-dm 5289 df-rn 5290 df-res 5291 df-ima 5292 df-pred 5867 df-ord 5913 df-on 5914 df-lim 5915 df-suc 5916 df-iota 6033 df-fun 6072 df-fn 6073 df-f 6074 df-f1 6075 df-fo 6076 df-f1o 6077 df-fv 6078 df-riota 6807 df-ov 6849 df-oprab 6850 df-mpt2 6851 df-om 7268 df-1st 7370 df-2nd 7371 df-wrecs 7614 df-recs 7676 df-rdg 7714 df-1o 7768 df-2o 7769 df-oadd 7772 df-er 7951 df-map 8066 df-pm 8067 df-en 8165 df-dom 8166 df-sdom 8167 df-fin 8168 df-sup 8559 df-card 9020 df-cda 9247 df-pnf 10334 df-mnf 10335 df-xr 10336 df-ltxr 10337 df-le 10338 df-sub 10527 df-neg 10528 df-div 10944 df-nn 11280 df-2 11340 df-3 11341 df-n0 11544 df-xnn0 11616 df-z 11630 df-uz 11894 df-rp 12036 df-fz 12541 df-fzo 12681 df-seq 13016 df-exp 13075 df-hash 13329 df-word 13494 df-lsw 13542 df-substr 13625 df-cj 14140 df-re 14141 df-im 14142 df-sqrt 14276 df-abs 14277 df-dvds 15282 df-prm 15682 df-edg 26233 df-uhgr 26246 df-upgr 26270 df-uspgr 26339 df-usgr 26340 df-fusgr 26504 df-wlks 26802 df-clwlks 26979 df-clwwlk 27229 df-clwwlkn 27282

This theorem is referenced by: clwlksfoclwwlkOLD 27358 clwlksf1clwwlkOLD 27364

W3C validator