numclwlk1lem2f1 - Metamath Proof Explorer

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

Theorem numclwlk1lem2f1 27347

Description: 𝑇 is a 1-1 function. (Contributed by AV, 26-Sep-2018.) (Revised by AV, 29-May-2021.) (Proof shortened by AV, 23-Feb-2022.) (Revised by AV, 6-Mar-2022.)

**Hypotheses**
Ref	Expression
extwwlkfab.v	⊢ 𝑉 = (Vtx‘𝐺)
extwwlkfab.c	⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ_≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
extwwlkfab.f	⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))
numclwwlk.t	⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 substr ⟨0, (𝑁 − 2)⟩), (𝑢‘(𝑁 − 1))⟩)

**Assertion**
Ref	Expression
numclwlk1lem2f1	⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → 𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)))

Distinct variable groups: 𝑛,𝐺,𝑣,𝑤 𝑛,𝑉,𝑣,𝑤 𝑛,𝑋,𝑣,𝑤 𝑛,𝑁,𝑣,𝑤 𝑤,𝐹 𝑢,𝐶 𝑢,𝐹 𝑢,𝐺,𝑤 𝑢,𝑁 𝑢,𝑉 𝑢,𝑋 𝑢,𝑇 Allowed substitution hints: 𝐶(𝑤,𝑣,𝑛) 𝑇(𝑤,𝑣,𝑛) 𝐹(𝑣,𝑛)

Proof of Theorem numclwlk1lem2f1 Dummy variables 𝑎 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		extwwlkfab.v	. . 3 ⊢ 𝑉 = (Vtx‘𝐺)
2		extwwlkfab.c	. . 3 ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ_≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
3		extwwlkfab.f	. . 3 ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))
4		numclwwlk.t	. . 3 ⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 substr ⟨0, (𝑁 − 2)⟩), (𝑢‘(𝑁 − 1))⟩)
5	1, 2, 3, 4	numclwlk1lem2f 27345	. 2 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → 𝑇:(𝑋𝐶𝑁)⟶(𝐹 × (𝐺 NeighbVtx 𝑋)))
6	1, 2, 3, 4	numclwlk1lem2fv 27346	. . . . . 6 ⊢ (𝑝 ∈ (𝑋𝐶𝑁) → (𝑇‘𝑝) = ⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩)
7	6	ad2antrl 764	. . . . 5 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇‘𝑝) = ⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩)
8	1, 2, 3, 4	numclwlk1lem2fv 27346	. . . . . 6 ⊢ (𝑎 ∈ (𝑋𝐶𝑁) → (𝑇‘𝑎) = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩)
9	8	ad2antll 765	. . . . 5 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇‘𝑎) = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩)
10	7, 9	eqeq12d 2666	. . . 4 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑎) ↔ ⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩ = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩))
11		ovex 6718	. . . . . 6 ⊢ (𝑝 substr ⟨0, (𝑁 − 2)⟩) ∈ V
12		fvex 6239	. . . . . 6 ⊢ (𝑝‘(𝑁 − 1)) ∈ V
13	11, 12	opth 4974	. . . . 5 ⊢ (⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩ = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩ ↔ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))))
14		uzuzle23 11767	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
15	2	2clwwlkel 27337	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑝 ∈ (𝑋𝐶𝑁) ↔ (𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑝‘(𝑁 − 2)) = 𝑋)))
16		isclwwlknon 27065	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋))
17	16	anbi1i 731	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ↔ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋))
18	15, 17	syl6bb 276	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑝 ∈ (𝑋𝐶𝑁) ↔ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋)))
19	2	2clwwlkel 27337	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑎 ∈ (𝑋𝐶𝑁) ↔ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)))
20		isclwwlknon 27065	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋))
21	20	anbi1i 731	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) ↔ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))
22	19, 21	syl6bb 276	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑎 ∈ (𝑋𝐶𝑁) ↔ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)))
23	18, 22	anbi12d 747	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))))
24	14, 23	sylan2 490	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))))
25	24	3adant1 1099	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))))
26	1	clwwlknbp 26997	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁))
27	26	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁))
28	27	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁))
29		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (𝑝‘0) = 𝑋)
30	29	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘0) = 𝑋)
31		simpr 476	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘(𝑁 − 2)) = 𝑋)
32	29	eqcomd 2657	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → 𝑋 = (𝑝‘0))
33	32	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑝‘0))
34	31, 33	eqtrd 2685	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘(𝑁 − 2)) = (𝑝‘0))
35	28, 30, 34	jca32 557	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))))
36	1	clwwlknbp 26997	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁))
37	36	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁))
38	37	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁))
39		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎‘0) = 𝑋)
40	39	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘0) = 𝑋)
41		simpr 476	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘(𝑁 − 2)) = 𝑋)
42	39	eqcomd 2657	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → 𝑋 = (𝑎‘0))
43	42	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑎‘0))
44	41, 43	eqtrd 2685	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘(𝑁 − 2)) = (𝑎‘0))
45	38, 40, 44	jca32 557	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))
46		eqtr3 2672	. . . . . . . . . . . . . . . . 17 ⊢ (((#‘𝑝) = 𝑁 ∧ (#‘𝑎) = 𝑁) → (#‘𝑝) = (#‘𝑎))
47	46	expcom 450	. . . . . . . . . . . . . . . 16 ⊢ ((#‘𝑎) = 𝑁 → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑎)))
48	47	ad2antlr 763	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑎)))
49	48	com12 32	. . . . . . . . . . . . . 14 ⊢ ((#‘𝑝) = 𝑁 → (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (#‘𝑝) = (#‘𝑎)))
50	49	ad2antlr 763	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (#‘𝑝) = (#‘𝑎)))
51	50	imp 444	. . . . . . . . . . . 12 ⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (#‘𝑝) = (#‘𝑎))
52	35, 45, 51	syl2an 493	. . . . . . . . . . 11 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (#‘𝑝) = (#‘𝑎))
53	52	3ad2ant2 1103	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (#‘𝑝) = (#‘𝑎))
54	27	simprd 478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (#‘𝑝) = 𝑁)
55	54	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (#‘𝑝) = 𝑁)
56	55	eqcomd 2657	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → 𝑁 = (#‘𝑝))
57	56	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑁 = (#‘𝑝))
58	57	oveq1d 6705	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑁 − 2) = ((#‘𝑝) − 2))
59	58	opeq2d 4440	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ⟨0, (𝑁 − 2)⟩ = ⟨0, ((#‘𝑝) − 2)⟩)
60	59	oveq2d 6706	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩))
61	59	oveq2d 6706	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩))
62	60, 61	eqeq12d 2666	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ↔ (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩)))
63	62	biimpcd 239	. . . . . . . . . . . . . 14 ⊢ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩)))
64	63	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩)))
65	64	impcom 445	. . . . . . . . . . . 12 ⊢ (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩))
66	55	oveq1d 6705	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → ((#‘𝑝) − 2) = (𝑁 − 2))
67	66	fveq2d 6233	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘((#‘𝑝) − 2)) = (𝑝‘(𝑁 − 2)))
68	67, 31	eqtrd 2685	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘((#‘𝑝) − 2)) = 𝑋)
69	68	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘((#‘𝑝) − 2)) = 𝑋)
70	41	eqcomd 2657	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑎‘(𝑁 − 2)))
71	70	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑋 = (𝑎‘(𝑁 − 2)))
72	58	fveq2d 6233	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎‘(𝑁 − 2)) = (𝑎‘((#‘𝑝) − 2)))
73	71, 72	eqtrd 2685	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑋 = (𝑎‘((#‘𝑝) − 2)))
74	69, 73	eqtrd 2685	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)))
75	74	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)))
76		lsw 13384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ Word 𝑉 → ( lastS ‘𝑝) = (𝑝‘((#‘𝑝) − 1)))
77		oveq1 6697	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝑝) = 𝑁 → ((#‘𝑝) − 1) = (𝑁 − 1))
78	77	fveq2d 6233	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 1)) = (𝑝‘(𝑁 − 1)))
79	76, 78	sylan9eq 2705	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1)))
80	26, 79	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1)))
81	80	eqcomd 2657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑝‘(𝑁 − 1)) = ( lastS ‘𝑝))
82	81	ad3antrrr 766	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘(𝑁 − 1)) = ( lastS ‘𝑝))
83		lsw 13384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ Word 𝑉 → ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1)))
84	83	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1)))
85		oveq1 6697	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 = (#‘𝑎) → (𝑁 − 1) = ((#‘𝑎) − 1))
86	85	eqcoms 2659	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((#‘𝑎) = 𝑁 → (𝑁 − 1) = ((#‘𝑎) − 1))
87	86	fveq2d 6233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((#‘𝑎) = 𝑁 → (𝑎‘(𝑁 − 1)) = (𝑎‘((#‘𝑎) − 1)))
88	87	eqeq2d 2661	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((#‘𝑎) = 𝑁 → (( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1))))
89	88	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → (( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1))))
90	84, 89	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → ( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)))
91	36, 90	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → ( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)))
92	91	eqcomd 2657	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (𝑎‘(𝑁 − 1)) = ( lastS ‘𝑎))
93	92	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎‘(𝑁 − 1)) = ( lastS ‘𝑎))
94	93	ad2antrl 764	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎‘(𝑁 − 1)) = ( lastS ‘𝑎))
95	82, 94	eqeq12d 2666	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑝) = ( lastS ‘𝑎)))
96	95	biimpd 219	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)) → ( lastS ‘𝑝) = ( lastS ‘𝑎)))
97	96	adantld 482	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → ( lastS ‘𝑝) = ( lastS ‘𝑎)))
98	97	imp 444	. . . . . . . . . . . 12 ⊢ (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → ( lastS ‘𝑝) = ( lastS ‘𝑎))
99	65, 75, 98	3jca 1261	. . . . . . . . . . 11 ⊢ (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → ((𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)))
100	99	3adant1 1099	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → ((𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)))
101	1	clwwlknwrd 26996	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → 𝑝 ∈ Word 𝑉)
102	101	ad3antrrr 766	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑝 ∈ Word 𝑉)
103	102	3ad2ant2 1103	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑝 ∈ Word 𝑉)
104	1	clwwlknwrd 26996	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → 𝑎 ∈ Word 𝑉)
105	104	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → 𝑎 ∈ Word 𝑉)
106	105	ad2antrl 764	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑎 ∈ Word 𝑉)
107	106	3ad2ant2 1103	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑎 ∈ Word 𝑉)
108		clwwlknlen 26994	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (#‘𝑝) = 𝑁)
109		eluz2b1 11797	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁))
110		breq2 4689	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 = (#‘𝑝) → (1 < 𝑁 ↔ 1 < (#‘𝑝)))
111	110	eqcoms 2659	. . . . . . . . . . . . . . . . . 18 ⊢ ((#‘𝑝) = 𝑁 → (1 < 𝑁 ↔ 1 < (#‘𝑝)))
112	111	biimpcd 239	. . . . . . . . . . . . . . . . 17 ⊢ (1 < 𝑁 → ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝)))
113	109, 112	simplbiim 659	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝)))
114	14, 108, 113	syl2imc 41	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑁 ∈ (ℤ_≥‘3) → 1 < (#‘𝑝)))
115	114	ad3antrrr 766	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑁 ∈ (ℤ_≥‘3) → 1 < (#‘𝑝)))
116	115	impcom 445	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))) → 1 < (#‘𝑝))
117	116	3adant3 1101	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 1 < (#‘𝑝))
118	103, 107, 117	3jca 1261	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 ∈ Word 𝑉 ∧ 𝑎 ∈ Word 𝑉 ∧ 1 < (#‘𝑝)))
119		2swrd2eqwrdeq 13742	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ Word 𝑉 ∧ 𝑎 ∈ Word 𝑉 ∧ 1 < (#‘𝑝)) → (𝑝 = 𝑎 ↔ ((#‘𝑝) = (#‘𝑎) ∧ ((𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)))))
120	118, 119	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 = 𝑎 ↔ ((#‘𝑝) = (#‘𝑎) ∧ ((𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)))))
121	53, 100, 120	mpbir2and 977	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑝 = 𝑎)
122	121	3exp 1283	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)))
123	122	3ad2ant3 1104	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)))
124	25, 123	sylbid 230	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)))
125	124	imp 444	. . . . 5 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎))
126	13, 125	syl5bi 232	. . . 4 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩ = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩ → 𝑝 = 𝑎))
127	10, 126	sylbid 230	. . 3 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎))
128	127	ralrimivva 3000	. 2 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ∀𝑝 ∈ (𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎))
129		dff13 6552	. 2 ⊢ (𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)) ↔ (𝑇:(𝑋𝐶𝑁)⟶(𝐹 × (𝐺 NeighbVtx 𝑋)) ∧ ∀𝑝 ∈ (𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎)))
130	5, 128, 129	sylanbrc 699	1 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → 𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∧ w3a 1054 = wceq 1523 ∈ wcel 2030 ∀wral 2941 {crab 2945 ⟨cop 4216 class class class wbr 4685 ↦ cmpt 4762 × cxp 5141 ⟶wf 5922 –1-1→wf1 5923 ‘cfv 5926 (class class class)co 6690 ↦ cmpt2 6692 0cc0 9974 1c1 9975 < clt 10112 − cmin 10304 2c2 11108 3c3 11109 ℤcz 11415 ℤ_≥cuz 11725 #chash 13157 Word cword 13323 lastS clsw 13324 substr csubstr 13327 Vtxcvtx 25919 USGraphcusgr 26089 NeighbVtx cnbgr 26269 ClWWalksN cclwwlkn 26981 ClWWalksNOncclwwlknon 27060

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-rep 4804 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-cnex 10030 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-mulcom 10038 ax-addass 10039 ax-mulass 10040 ax-distr 10041 ax-i2m1 10042 ax-1ne0 10043 ax-1rid 10044 ax-rnegex 10045 ax-rrecex 10046 ax-cnre 10047 ax-pre-lttri 10048 ax-pre-lttrn 10049 ax-pre-ltadd 10050 ax-pre-mulgt0 10051

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-fal 1529 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-nel 2927 df-ral 2946 df-rex 2947 df-reu 2948 df-rmo 2949 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-pss 3623 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-tp 4215 df-op 4217 df-uni 4469 df-int 4508 df-iun 4554 df-br 4686 df-opab 4746 df-mpt 4763 df-tr 4786 df-id 5053 df-eprel 5058 df-po 5064 df-so 5065 df-fr 5102 df-we 5104 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-pred 5718 df-ord 5764 df-on 5765 df-lim 5766 df-suc 5767 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-riota 6651 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-om 7108 df-1st 7210 df-2nd 7211 df-wrecs 7452 df-recs 7513 df-rdg 7551 df-1o 7605 df-2o 7606 df-oadd 7609 df-er 7787 df-map 7901 df-pm 7902 df-en 7998 df-dom 7999 df-sdom 8000 df-fin 8001 df-card 8803 df-cda 9028 df-pnf 10114 df-mnf 10115 df-xr 10116 df-ltxr 10117 df-le 10118 df-sub 10306 df-neg 10307 df-nn 11059 df-2 11117 df-3 11118 df-n0 11331 df-xnn0 11402 df-z 11416 df-uz 11726 df-fz 12365 df-fzo 12505 df-hash 13158 df-word 13331 df-lsw 13332 df-concat 13333 df-s1 13334 df-substr 13335 df-s2 13639 df-edg 25985 df-upgr 26022 df-umgr 26023 df-usgr 26091 df-nbgr 26270 df-wwlks 26778 df-wwlksn 26779 df-clwwlk 26950 df-clwwlkn 26983 df-clwwlknon 27061

This theorem is referenced by: numclwlk1lem2f1o 27349

W3C validator