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 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	⊢ 𝐴 = (1^st ‘𝑐)
clwlksfclwwlk.2	⊢ 𝐵 = (2^nd ‘𝑐)
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.

Step	Hyp	Ref	Expression
1		clwlksfclwwlk.c	. . . . . 6 ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘𝐴) = 𝑁}
2	1	rabeq2i 3347	. . . . 5 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁))
3		fusgrusgr 26437	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
4		usgrupgr 26299	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
5	3, 4	syl 17	. . . . . . . . . . 11 ⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ UPGraph)
6	5	adantr 466	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ UPGraph)
7		eqid 2771	. . . . . . . . . . 11 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
8		eqid 2771	. . . . . . . . . . 11 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
9		clwlksfclwwlk.1	. . . . . . . . . . 11 ⊢ 𝐴 = (1^st ‘𝑐)
10		clwlksfclwwlk.2	. . . . . . . . . . 11 ⊢ 𝐵 = (2^nd ‘𝑐)
11	7, 8, 9, 10	upgrclwlkcompim 26912	. . . . . . . . . 10 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
12	6, 11	sylan 569	. . . . . . . . 9 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
13		lencl 13520	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word dom (iEdg‘𝐺) → (♯‘𝐴) ∈ ℕ₀)
14		clwlksfclwwlk.f	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩))
15	9, 10, 1, 14	clwlksfclwwlk2wrdOLD 27239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ 𝐶 → 𝐵 ∈ Word (Vtx‘𝐺))
16	15	ad2antlr 706	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
17		swrdcl 13627	. . . . . . . . . . . . . . . . . . . . . 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 13528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → 𝐵 ∈ Word (Vtx‘𝐺))
20	19	3ad2ant1 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
21		prmnn 15595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑁 ∈ ℙ → 𝑁 ∈ ℕ)
22	21	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ)
23	22	3ad2ant3 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ)
24		oveq2 6801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐴) = 𝑁 → (0...(♯‘𝐴)) = (0...𝑁))
25	24	feq2d 6171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐴) = 𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ↔ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)))
26	22	nnnn0d 11553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ₀)
27		ffz0hash 13433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1))
28	26, 27	sylan 569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1))
29	28	ex 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → (♯‘𝐵) = (𝑁 + 1)))
30	21	nnred 11237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑁 ∈ ℙ → 𝑁 ∈ ℝ)
31	30	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ∈ ℝ)
32	31	lep1d 11157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (𝑁 + 1))
33		breq2 4790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((♯‘𝐵) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
34	33	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
35	32, 34	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (♯‘𝐵))
36	35	ex 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑁 ∈ ℙ → ((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵)))
37	36	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → ((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵)))
38	29, 37	syldc 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵)))
39	25, 38	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐴) = 𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵))))
40	39	3imp21 1105	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ≤ (♯‘𝐵))
41		swrdn0 13639	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝐵)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
42	20, 23, 40, 41	syl3anc 1476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
43		opeq2 4540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐴) = 𝑁 → ⟨0, (♯‘𝐴)⟩ = ⟨0, 𝑁⟩)
44	43	oveq2d 6809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) = (𝐵 substr ⟨0, 𝑁⟩))
45	44	neeq1d 3002	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝐴) = 𝑁 → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
46	45	3ad2ant2 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
47	42, 46	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)
48	47	3exp 1112	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)))
49	48	ad2antlr 706	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)))
50	49	imp 393	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
51	50	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
52	51	imp 393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)
53	18, 52	jca 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
54		simp-5r 774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 𝐴 ∈ Word dom (iEdg‘𝐺))
55	3	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ USGraph)
56	54, 55	anim12ci 601	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)))
57		simp-5r 774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺))
58		prmuz2 15615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℙ → 𝑁 ∈ (ℤ_≥‘2))
59		ffz0hash 13433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1))
60	59	adantlr 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1))
61		eluz2 11894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)))
62		2re 11292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 2 ∈ ℝ
63	62	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((♯‘𝐴) ∈ ℤ → 2 ∈ ℝ)
64		zre 11583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ ℝ)
65		peano2re 10411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((♯‘𝐴) ∈ ℝ → ((♯‘𝐴) + 1) ∈ ℝ)
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) + 1) ∈ ℝ)
67	63, 64, 66	3jca 1122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ ℤ → (2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ))
68	67	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ))
69		simpr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ (♯‘𝐴))
70	64	lep1d 11157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ≤ ((♯‘𝐴) + 1))
71	70	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (♯‘𝐴) ≤ ((♯‘𝐴) + 1))
72		letr 10333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) → ((2 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ ((♯‘𝐴) + 1)) → 2 ≤ ((♯‘𝐴) + 1)))
73	72	imp 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) ∧ (2 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ ((♯‘𝐴) + 1))) → 2 ≤ ((♯‘𝐴) + 1))
74	68, 69, 71, 73	syl12anc 1474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ ((♯‘𝐴) + 1))
75	74	3adant1 1124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((2 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ ((♯‘𝐴) + 1))
76	61, 75	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘2) → 2 ≤ ((♯‘𝐴) + 1))
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → ((♯‘𝐴) ∈ (ℤ_≥‘2) → 2 ≤ ((♯‘𝐴) + 1)))
78		eleq1 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 = (♯‘𝐴) → (𝑁 ∈ (ℤ_≥‘2) ↔ (♯‘𝐴) ∈ (ℤ_≥‘2)))
79	78	eqcoms 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ_≥‘2) ↔ (♯‘𝐴) ∈ (ℤ_≥‘2)))
80	79	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ_≥‘2) ↔ (♯‘𝐴) ∈ (ℤ_≥‘2)))
81		breq2 4790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝐵) = ((♯‘𝐴) + 1) → (2 ≤ (♯‘𝐵) ↔ 2 ≤ ((♯‘𝐴) + 1)))
82	81	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (2 ≤ (♯‘𝐵) ↔ 2 ≤ ((♯‘𝐴) + 1)))
83	77, 80, 82	3imtr4d 283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵)))
84	83	ex 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐵) = ((♯‘𝐴) + 1) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵))))
85	60, 84	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵))))
86	85	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵))))
87	86	imp 393	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ_≥‘2) → 2 ≤ (♯‘𝐵)))
88	87	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (♯‘𝐵)))
91	90	impcom 394	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 2 ≤ (♯‘𝐵))
92		simp-4r 770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
93	7, 8	usgrf 26272	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐺 ∈ USGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2})
94	93	anim1i 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‘𝐺)))
96	94, 95	syl3an1 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‘𝐺)
99	98	eleq2i 2842	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))
100	99	ralbii 3129	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))
101	98	eleq2i 2842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺) ↔ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))
102	97, 100, 101	3anbi123i 1158	. . . . . . . . . . . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . . . . . . . . . . . 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 1481	. . . . . . . . . . . . . . . . . . . . . 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 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 ⊢ ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ ℤ)
111	64	lem1d 11159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) − 1) ≤ (♯‘𝐴))
112		eluz2 11894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘((♯‘𝐴) − 1)) ↔ (((♯‘𝐴) − 1) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴)))
113	109, 110, 111, 112	syl3anbrc 1428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ (ℤ_≥‘((♯‘𝐴) − 1)))
114		fzoss2 12704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘((♯‘𝐴) − 1)) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
115	108, 113, 114	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
116	115	sselda 3752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈ (0..^(♯‘𝐴)))
117	116	3adant2 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈ (0..^(♯‘𝐴)))
118		swrd0fv 13648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖) = (𝐵‘𝑖))
119	106, 107, 117, 118	syl3anc 1476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖) = (𝐵‘𝑖))
120	119	eqcomd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵‘𝑖) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖))
121		elfzom1elp1fzo 12743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((♯‘𝐴) ∈ ℤ ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
122	108, 121	sylan 569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
123	122	3adant2 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
124		swrd0fv 13648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)) = (𝐵‘(𝑖 + 1)))
125	124	eqcomd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)))
126	106, 107, 123, 125	syl3anc 1476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)))
127	120, 126	preq12d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})
128	127	3exp 1112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 393	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})
131	130	eleq1d 2835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
132	131	ralbidva 3134	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ∈ 𝐶 → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
133	132	ad2antlr 706	. . . . . . . . . . . . . . . . . . . . . . . 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 27242	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝐶 → (♯‘𝐴) = (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)))
135	134	oveq1d 6808	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝐶 → ((♯‘𝐴) − 1) = ((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1))
136	135	ad2antlr 706	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((♯‘𝐴) − 1) = ((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1))
137	136	oveq2d 6809	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (0..^((♯‘𝐴) − 1)) = (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)))
138	137	raleqdv 3293	. . . . . . . . . . . . . . . . . . . . . . . 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 268	. . . . . . . . . . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ ↔ (♯‘𝐴) ∈ ℙ))
141	140	biimpd 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ → (♯‘𝐴) ∈ ℙ))
142	141	eqcoms 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (♯‘𝐴) ∈ ℙ))
143		prmnn 15595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((♯‘𝐴) ∈ ℙ → (♯‘𝐴) ∈ ℕ)
144		elfz2nn0 12638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((♯‘𝐴) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)))
145		1zzd 11610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → 1 ∈ ℤ)
146		nn0z 11602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((♯‘𝐵) ∈ ℕ₀ → (♯‘𝐵) ∈ ℤ)
147	146	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → (♯‘𝐵) ∈ ℤ)
148		nn0z 11602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((♯‘𝐴) ∈ ℕ₀ → (♯‘𝐴) ∈ ℤ)
149	148	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → (♯‘𝐴) ∈ ℤ)
150	145, 147, 149	3jca 1122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
151	150	3adant3 1126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
152	151	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
153		simp3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))
154		nnge1 11248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((♯‘𝐴) ∈ ℕ → 1 ≤ (♯‘𝐴))
155	153, 154	anim12ci 601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵)))
156	152, 155	jca 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
157	144, 156	sylanb 570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
158		elfz2 12540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((♯‘𝐴) ∈ (1...(♯‘𝐵)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
159	157, 158	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (♯‘𝐴) ∈ (1...(♯‘𝐵)))
160		swrd0fvlsw 13652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = (𝐵‘((♯‘𝐴) − 1)))
161	160	eqcomd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (𝐵‘((♯‘𝐴) − 1)) = (lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)))
162		swrd0fv0 13649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0) = (𝐵‘0))
163	162	eqcomd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (𝐵‘0) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0))
164	161, 163	preq12d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})
165	164	expcom 398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
174	173	imp 393	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
177	176	impcom 394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})
178	177	eleq1d 2835	. . . . . . . . . . . . . . . . . . . . . . 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 1550	. . . . . . . . . . . . . . . . . . . . . 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 222	. . . . . . . . . . . . . . . . . . . . 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 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‘𝐺)))
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 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‘𝐺))))
184	53, 182, 183	sylanbrc 572	. . . . . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
186	7, 185	isclwwlk 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‘𝐺)))
187	184, 186	sylibr 224	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (ClWWalks‘𝐺))
188	134	eqeq1d 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 ↔ (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
189	188	biimpcd 239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
190	189	adantl 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
191	190	imp 393	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁)
192	191	adantr 466	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁)
193		isclwwlkn 27180	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (ClWWalks‘𝐺) ∧ (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
194	187, 192, 193	sylanbrc 572	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))
195	194	exp31 406	. . . . . . . . . . . . . . . 16 ⊢ ((((((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
196	195	exp41 421	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))))
197	13, 196	mpancom 668	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Word dom (iEdg‘𝐺) → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))))
198	197	imp 393	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))))
199	198	3impib 1108	. . . . . . . . . . . 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 466	. . . . . . . . 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 398	. . . . . . 7 ⊢ (𝑐 ∈ (ClWalks‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
205	204	com24 95	. . . . . 6 ⊢ (𝑐 ∈ (ClWalks‘𝐺) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
206	205	imp 393	. . . . 5 ⊢ ((𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
207	2, 206	sylbi 207	. . . 4 ⊢ (𝑐 ∈ 𝐶 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
208	207	pm2.43i 52	. . 3 ⊢ (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))
209	208	impcom 394	. 2 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ 𝐶) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))
210	209, 14	fmptd 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-1→wf1 6028 ‘cfv 6031 (class class class)co 6793 1^st c1st 7313 2^nd c2nd 7314 ℝcr 10137 0cc0 10138 1c1 10139 + caddc 10141 ≤ cle 10277 − cmin 10468 ℕcn 11222 2c2 11272 ℕ₀cn0 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

W3C validator