numclwwlk1lem2f1OLD - Metamath Proof Explorer

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

Theorem numclwwlk1lem2f1OLD 27723

Description: Obsolete version of numclwwlk1lem2f1 27718 as of 12-Oct-2022. (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.) (New usage is discouraged.) (Proof modification is discouraged.)

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

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

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

Proof of Theorem numclwwlk1lem2f1OLD 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		numclwwlkOLD.t	. . 3 ⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 substr ⟨0, (𝑁 − 2)⟩), (𝑢‘(𝑁 − 1))⟩)
5	1, 2, 3, 4	numclwwlk1lem2fOLD 27721	. 2 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → 𝑇:(𝑋𝐶𝑁)⟶(𝐹 × (𝐺 NeighbVtx 𝑋)))
6	1, 2, 3, 4	numclwwlk1lem2fvOLD 27722	. . . . . 6 ⊢ (𝑝 ∈ (𝑋𝐶𝑁) → (𝑇‘𝑝) = ⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩)
7	6	ad2antrl 720	. . . . 5 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇‘𝑝) = ⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩)
8	1, 2, 3, 4	numclwwlk1lem2fvOLD 27722	. . . . . 6 ⊢ (𝑎 ∈ (𝑋𝐶𝑁) → (𝑇‘𝑎) = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩)
9	8	ad2antll 721	. . . . 5 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇‘𝑎) = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩)
10	7, 9	eqeq12d 2814	. . . 4 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑎) ↔ ⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩ = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩))
11		ovex 6910	. . . . . 6 ⊢ (𝑝 substr ⟨0, (𝑁 − 2)⟩) ∈ V
12		fvex 6424	. . . . . 6 ⊢ (𝑝‘(𝑁 − 1)) ∈ V
13	11, 12	opth 5135	. . . . 5 ⊢ (⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩ = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩ ↔ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))))
14		uzuzle23 11973	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
15	2	2clwwlkel 27703	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑝 ∈ (𝑋𝐶𝑁) ↔ (𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑝‘(𝑁 − 2)) = 𝑋)))
16		isclwwlknon 27428	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋))
17	16	anbi1i 618	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ↔ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋))
18	15, 17	syl6bb 279	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑝 ∈ (𝑋𝐶𝑁) ↔ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋)))
19	2	2clwwlkel 27703	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑎 ∈ (𝑋𝐶𝑁) ↔ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)))
20		isclwwlknon 27428	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋))
21	20	anbi1i 618	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) ↔ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))
22	19, 21	syl6bb 279	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑎 ∈ (𝑋𝐶𝑁) ↔ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)))
23	18, 22	anbi12d 625	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))))
24	14, 23	sylan2 587	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))))
25	24	3adant1 1161	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))))
26	1	clwwlknbp 27342	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 𝑁))
27	26	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 𝑁))
28	27	adantr 473	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 𝑁))
29		simpr 478	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (𝑝‘0) = 𝑋)
30	29	adantr 473	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘0) = 𝑋)
31		simpr 478	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘(𝑁 − 2)) = 𝑋)
32	29	eqcomd 2805	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → 𝑋 = (𝑝‘0))
33	32	adantr 473	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑝‘0))
34	31, 33	eqtrd 2833	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘(𝑁 − 2)) = (𝑝‘0))
35	28, 30, 34	jca32 512	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))))
36	1	clwwlknbp 27342	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁))
37	36	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁))
38	37	adantr 473	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁))
39		simpr 478	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎‘0) = 𝑋)
40	39	adantr 473	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘0) = 𝑋)
41		simpr 478	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘(𝑁 − 2)) = 𝑋)
42	39	eqcomd 2805	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → 𝑋 = (𝑎‘0))
43	42	adantr 473	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑎‘0))
44	41, 43	eqtrd 2833	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘(𝑁 − 2)) = (𝑎‘0))
45	38, 40, 44	jca32 512	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → ((𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))
46		eqtr3 2820	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝑝) = 𝑁 ∧ (♯‘𝑎) = 𝑁) → (♯‘𝑝) = (♯‘𝑎))
47	46	expcom 403	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑎) = 𝑁 → ((♯‘𝑝) = 𝑁 → (♯‘𝑝) = (♯‘𝑎)))
48	47	ad2antlr 719	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → ((♯‘𝑝) = 𝑁 → (♯‘𝑝) = (♯‘𝑎)))
49	48	com12 32	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑝) = 𝑁 → (((𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (♯‘𝑝) = (♯‘𝑎)))
50	49	ad2antlr 719	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → (((𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (♯‘𝑝) = (♯‘𝑎)))
51	50	imp 396	. . . . . . . . . . . 12 ⊢ ((((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (♯‘𝑝) = (♯‘𝑎))
52	35, 45, 51	syl2an 590	. . . . . . . . . . 11 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (♯‘𝑝) = (♯‘𝑎))
53	52	3ad2ant2 1165	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (♯‘𝑝) = (♯‘𝑎))
54	27	simprd 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (♯‘𝑝) = 𝑁)
55	54	adantr 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (♯‘𝑝) = 𝑁)
56	55	eqcomd 2805	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → 𝑁 = (♯‘𝑝))
57	56	adantr 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑁 = (♯‘𝑝))
58	57	oveq1d 6893	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑁 − 2) = ((♯‘𝑝) − 2))
59	58	opeq2d 4600	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ⟨0, (𝑁 − 2)⟩ = ⟨0, ((♯‘𝑝) − 2)⟩)
60	59	oveq2d 6894	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑝 substr ⟨0, ((♯‘𝑝) − 2)⟩))
61	59	oveq2d 6894	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, ((♯‘𝑝) − 2)⟩))
62	60, 61	eqeq12d 2814	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ↔ (𝑝 substr ⟨0, ((♯‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((♯‘𝑝) − 2)⟩)))
63	62	biimpcd 241	. . . . . . . . . . . . . 14 ⊢ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr ⟨0, ((♯‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((♯‘𝑝) − 2)⟩)))
64	63	adantr 473	. . . . . . . . . . . . 13 ⊢ (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr ⟨0, ((♯‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((♯‘𝑝) − 2)⟩)))
65	64	impcom 397	. . . . . . . . . . . 12 ⊢ (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 substr ⟨0, ((♯‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((♯‘𝑝) − 2)⟩))
66	55	oveq1d 6893	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → ((♯‘𝑝) − 2) = (𝑁 − 2))
67	66	fveq2d 6415	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘((♯‘𝑝) − 2)) = (𝑝‘(𝑁 − 2)))
68	67, 31	eqtrd 2833	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘((♯‘𝑝) − 2)) = 𝑋)
69	68	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘((♯‘𝑝) − 2)) = 𝑋)
70	41	eqcomd 2805	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑎‘(𝑁 − 2)))
71	70	adantl 474	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑋 = (𝑎‘(𝑁 − 2)))
72	58	fveq2d 6415	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎‘(𝑁 − 2)) = (𝑎‘((♯‘𝑝) − 2)))
73	71, 72	eqtrd 2833	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑋 = (𝑎‘((♯‘𝑝) − 2)))
74	69, 73	eqtrd 2833	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘((♯‘𝑝) − 2)) = (𝑎‘((♯‘𝑝) − 2)))
75	74	adantr 473	. . . . . . . . . . . 12 ⊢ (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝‘((♯‘𝑝) − 2)) = (𝑎‘((♯‘𝑝) − 2)))
76		lsw 13584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ Word 𝑉 → (lastS‘𝑝) = (𝑝‘((♯‘𝑝) − 1)))
77		fvoveq1 6901	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑝) = 𝑁 → (𝑝‘((♯‘𝑝) − 1)) = (𝑝‘(𝑁 − 1)))
78	76, 77	sylan9eq 2853	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 𝑁) → (lastS‘𝑝) = (𝑝‘(𝑁 − 1)))
79	26, 78	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (lastS‘𝑝) = (𝑝‘(𝑁 − 1)))
80	79	eqcomd 2805	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑝‘(𝑁 − 1)) = (lastS‘𝑝))
81	80	ad3antrrr 722	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘(𝑁 − 1)) = (lastS‘𝑝))
82		lsw 13584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ Word 𝑉 → (lastS‘𝑎) = (𝑎‘((♯‘𝑎) − 1)))
83	82	adantr 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁) → (lastS‘𝑎) = (𝑎‘((♯‘𝑎) − 1)))
84		oveq1 6885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 = (♯‘𝑎) → (𝑁 − 1) = ((♯‘𝑎) − 1))
85	84	eqcoms 2807	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑎) = 𝑁 → (𝑁 − 1) = ((♯‘𝑎) − 1))
86	85	fveq2d 6415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝑎) = 𝑁 → (𝑎‘(𝑁 − 1)) = (𝑎‘((♯‘𝑎) − 1)))
87	86	eqeq2d 2809	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑎) = 𝑁 → ((lastS‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ (lastS‘𝑎) = (𝑎‘((♯‘𝑎) − 1))))
88	87	adantl 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁) → ((lastS‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ (lastS‘𝑎) = (𝑎‘((♯‘𝑎) − 1))))
89	83, 88	mpbird 249	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ Word 𝑉 ∧ (♯‘𝑎) = 𝑁) → (lastS‘𝑎) = (𝑎‘(𝑁 − 1)))
90	36, 89	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (lastS‘𝑎) = (𝑎‘(𝑁 − 1)))
91	90	eqcomd 2805	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (𝑎‘(𝑁 − 1)) = (lastS‘𝑎))
92	91	adantr 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎‘(𝑁 − 1)) = (lastS‘𝑎))
93	92	ad2antrl 720	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎‘(𝑁 − 1)) = (lastS‘𝑎))
94	81, 93	eqeq12d 2814	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)) ↔ (lastS‘𝑝) = (lastS‘𝑎)))
95	94	biimpd 221	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)) → (lastS‘𝑝) = (lastS‘𝑎)))
96	95	adantld 485	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → (lastS‘𝑝) = (lastS‘𝑎)))
97	96	imp 396	. . . . . . . . . . . 12 ⊢ (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (lastS‘𝑝) = (lastS‘𝑎))
98	65, 75, 97	3jca 1159	. . . . . . . . . . 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‘𝑎)))
99	98	3adant1 1161	. . . . . . . . . 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‘𝑎)))
100	1	clwwlknwrd 27341	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → 𝑝 ∈ Word 𝑉)
101	100	ad3antrrr 722	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑝 ∈ Word 𝑉)
102	101	3ad2ant2 1165	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑝 ∈ Word 𝑉)
103	1	clwwlknwrd 27341	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → 𝑎 ∈ Word 𝑉)
104	103	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → 𝑎 ∈ Word 𝑉)
105	104	ad2antrl 720	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑎 ∈ Word 𝑉)
106	105	3ad2ant2 1165	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑎 ∈ Word 𝑉)
107		clwwlknlen 27339	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (♯‘𝑝) = 𝑁)
108		eluz2b1 12004	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁))
109		breq2 4847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 = (♯‘𝑝) → (1 < 𝑁 ↔ 1 < (♯‘𝑝)))
110	109	eqcoms 2807	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑝) = 𝑁 → (1 < 𝑁 ↔ 1 < (♯‘𝑝)))
111	110	biimpcd 241	. . . . . . . . . . . . . . . . 17 ⊢ (1 < 𝑁 → ((♯‘𝑝) = 𝑁 → 1 < (♯‘𝑝)))
112	108, 111	simplbiim 500	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ((♯‘𝑝) = 𝑁 → 1 < (♯‘𝑝)))
113	14, 107, 112	syl2imc 41	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑁 ∈ (ℤ_≥‘3) → 1 < (♯‘𝑝)))
114	113	ad3antrrr 722	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑁 ∈ (ℤ_≥‘3) → 1 < (♯‘𝑝)))
115	114	impcom 397	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))) → 1 < (♯‘𝑝))
116	115	3adant3 1163	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 1 < (♯‘𝑝))
117	102, 106, 116	3jca 1159	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 ∈ Word 𝑉 ∧ 𝑎 ∈ Word 𝑉 ∧ 1 < (♯‘𝑝)))
118		2swrd2eqwrdeqOLD 14039	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ Word 𝑉 ∧ 𝑎 ∈ Word 𝑉 ∧ 1 < (♯‘𝑝)) → (𝑝 = 𝑎 ↔ ((♯‘𝑝) = (♯‘𝑎) ∧ ((𝑝 substr ⟨0, ((♯‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((♯‘𝑝) − 2)⟩) ∧ (𝑝‘((♯‘𝑝) − 2)) = (𝑎‘((♯‘𝑝) − 2)) ∧ (lastS‘𝑝) = (lastS‘𝑎)))))
119	117, 118	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‘𝑎)))))
120	53, 99, 119	mpbir2and 705	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑝 = 𝑎)
121	120	3exp 1149	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)))
122	121	3ad2ant3 1166	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)))
123	25, 122	sylbid 232	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)))
124	123	imp 396	. . . . 5 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎))
125	13, 124	syl5bi 234	. . . 4 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩ = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩ → 𝑝 = 𝑎))
126	10, 125	sylbid 232	. . 3 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎))
127	126	ralrimivva 3152	. 2 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ∀𝑝 ∈ (𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎))
128		dff13 6740	. 2 ⊢ (𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)) ↔ (𝑇:(𝑋𝐶𝑁)⟶(𝐹 × (𝐺 NeighbVtx 𝑋)) ∧ ∀𝑝 ∈ (𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎)))
129	5, 127, 128	sylanbrc 579	1 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → 𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ∀wral 3089 {crab 3093 ⟨cop 4374 class class class wbr 4843 ↦ cmpt 4922 × cxp 5310 ⟶wf 6097 –1-1→wf1 6098 ‘cfv 6101 (class class class)co 6878 ↦ cmpt2 6880 0cc0 10224 1c1 10225 < clt 10363 − cmin 10556 2c2 11368 3c3 11369 ℤcz 11666 ℤ_≥cuz 11930 ♯chash 13370 Word cword 13534 lastSclsw 13582 substr csubstr 13664 Vtxcvtx 26231 USGraphcusgr 26385 NeighbVtx cnbgr 26566 ClWWalksN cclwwlkn 27326 ClWWalksNOncclwwlknon 27423

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 ax-cnex 10280 ax-resscn 10281 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-addrcl 10285 ax-mulcl 10286 ax-mulrcl 10287 ax-mulcom 10288 ax-addass 10289 ax-mulass 10290 ax-distr 10291 ax-i2m1 10292 ax-1ne0 10293 ax-1rid 10294 ax-rnegex 10295 ax-rrecex 10296 ax-cnre 10297 ax-pre-lttri 10298 ax-pre-lttrn 10299 ax-pre-ltadd 10300 ax-pre-mulgt0 10301

This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-fal 1667 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rmo 3097 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-tp 4373 df-op 4375 df-uni 4629 df-int 4668 df-iun 4712 df-br 4844 df-opab 4906 df-mpt 4923 df-tr 4946 df-id 5220 df-eprel 5225 df-po 5233 df-so 5234 df-fr 5271 df-we 5273 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-pred 5898 df-ord 5944 df-on 5945 df-lim 5946 df-suc 5947 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-riota 6839 df-ov 6881 df-oprab 6882 df-mpt2 6883 df-om 7300 df-1st 7401 df-2nd 7402 df-wrecs 7645 df-recs 7707 df-rdg 7745 df-1o 7799 df-2o 7800 df-oadd 7803 df-er 7982 df-map 8097 df-pm 8098 df-en 8196 df-dom 8197 df-sdom 8198 df-fin 8199 df-card 9051 df-cda 9278 df-pnf 10365 df-mnf 10366 df-xr 10367 df-ltxr 10368 df-le 10369 df-sub 10558 df-neg 10559 df-nn 11313 df-2 11376 df-3 11377 df-n0 11581 df-xnn0 11653 df-z 11667 df-uz 11931 df-rp 12075 df-fz 12581 df-fzo 12721 df-hash 13371 df-word 13535 df-lsw 13583 df-concat 13591 df-s1 13616 df-substr 13665 df-pfx 13714 df-s2 13933 df-edg 26283 df-upgr 26317 df-umgr 26318 df-usgr 26387 df-nbgr 26567 df-wwlks 27081 df-wwlksn 27082 df-clwwlk 27275 df-clwwlkn 27328 df-clwwlknon 27424

This theorem is referenced by: numclwwlk1lem2f1oOLD 27725

W3C validator