clwwlkf1 - Metamath Proof Explorer

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

Theorem clwwlkf1 27830

Description: Lemma 3 for clwwlkf1o 27832: F is a 1-1 function. (Contributed by AV, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.)

**Hypotheses**
Ref	Expression
clwwlkf1o.d	⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)}
clwwlkf1o.f	⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁))

**Assertion**
Ref	Expression
clwwlkf1	⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺))

Distinct variable groups: 𝑤,𝐺 𝑤,𝑁 𝑡,𝐷 𝑡,𝐺,𝑤 𝑡,𝑁 Allowed substitution hints: 𝐷(𝑤) 𝐹(𝑤,𝑡)

Proof of Theorem clwwlkf1 Dummy variables 𝑖 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		clwwlkf1o.d	. . 3 ⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)}
2		clwwlkf1o.f	. . 3 ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁))
3	1, 2	clwwlkf 27828	. 2 ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))
4	1, 2	clwwlkfv 27829	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = (𝑥 prefix 𝑁))
5	1, 2	clwwlkfv 27829	. . . . . 6 ⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) = (𝑦 prefix 𝑁))
6	4, 5	eqeqan12d 2840	. . . . 5 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)))
7	6	adantl 484	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)))
8		fveq2 6672	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (lastS‘𝑤) = (lastS‘𝑥))
9		fveq1 6671	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0))
10	8, 9	eqeq12d 2839	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑥) = (𝑥‘0)))
11	10, 1	elrab2 3685	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)))
12		fveq2 6672	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (lastS‘𝑤) = (lastS‘𝑦))
13		fveq1 6671	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0))
14	12, 13	eqeq12d 2839	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑦) = (𝑦‘0)))
15	14, 1	elrab2 3685	. . . . . . 7 ⊢ (𝑦 ∈ 𝐷 ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)))
16	11, 15	anbi12i 628	. . . . . 6 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ↔ ((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))))
17		eqid 2823	. . . . . . . . . 10 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
18		eqid 2823	. . . . . . . . . 10 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
19	17, 18	wwlknp 27623	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥‘𝑖), (𝑥‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
20	17, 18	wwlknp 27623	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝑁 WWalksN 𝐺) → (𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
21		simprlr 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑥) = (𝑁 + 1))
22		simpllr 774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑦) = (𝑁 + 1))
23	21, 22	eqtr4d 2861	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑥) = (♯‘𝑦))
24	23	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (♯‘𝑥) = (♯‘𝑦))
25		nncn 11648	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
26		ax-1cn 10597	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1 ∈ ℂ
27		pncan 10894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
28	27	eqcomd 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → 𝑁 = ((𝑁 + 1) − 1))
29	25, 26, 28	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ → 𝑁 = ((𝑁 + 1) − 1))
30		oveq1 7165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑥) = (𝑁 + 1) → ((♯‘𝑥) − 1) = ((𝑁 + 1) − 1))
31	30	eqcomd 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑥) = (𝑁 + 1) → ((𝑁 + 1) − 1) = ((♯‘𝑥) − 1))
32	29, 31	sylan9eqr 2880	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → 𝑁 = ((♯‘𝑥) − 1))
33	32	oveq2d 7174	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑥 prefix 𝑁) = (𝑥 prefix ((♯‘𝑥) − 1)))
34	32	oveq2d 7174	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑦 prefix 𝑁) = (𝑦 prefix ((♯‘𝑥) − 1)))
35	33, 34	eqeq12d 2839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1))))
36	35	ex 415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))))
37	36	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))))
38	37	adantl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))))
39	38	impcom 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1))))
40	39	biimpa 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))
41		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → 𝑦 ∈ Word (Vtx‘𝐺))
42		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → 𝑥 ∈ Word (Vtx‘𝐺))
43	41, 42	anim12ci 615	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)))
44	43	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)))
45		nnnn0 11907	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
46		0nn0 11915	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℕ₀
47	45, 46	jctil 522	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀))
48	47	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀))
49		nnre 11647	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
50	49	lep1d 11573	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1))
51		breq2 5072	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝑥) ↔ 𝑁 ≤ (𝑁 + 1)))
52	50, 51	syl5ibr 248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥)))
53	52	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥)))
54	53	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥)))
55	54	impcom 410	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (♯‘𝑥))
56		breq2 5072	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑦) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝑦) ↔ 𝑁 ≤ (𝑁 + 1)))
57	50, 56	syl5ibr 248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝑦) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦)))
58	57	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦)))
59	58	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦)))
60	59	impcom 410	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (♯‘𝑦))
61		pfxval 14037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ₀) → (𝑥 prefix 𝑁) = (𝑥 substr ⟨0, 𝑁⟩))
62	61	ad2ant2rl 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (𝑥 prefix 𝑁) = (𝑥 substr ⟨0, 𝑁⟩))
63		pfxval 14037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ₀) → (𝑦 prefix 𝑁) = (𝑦 substr ⟨0, 𝑁⟩))
64	63	ad2ant2l 744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (𝑦 prefix 𝑁) = (𝑦 substr ⟨0, 𝑁⟩))
65	62, 64	eqeq12d 2839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)))
66	65	3adant3 1128	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)))
67		swrdspsleq 14029	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
68	66, 67	bitrd 281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
69	44, 48, 55, 60, 68	syl112anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
70		lbfzo0 13080	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
71	70	biimpri 230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 0 ∈ (0..^𝑁))
72	71	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 0 ∈ (0..^𝑁))
73		fveq2 6672	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 0 → (𝑥‘𝑖) = (𝑥‘0))
74		fveq2 6672	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 0 → (𝑦‘𝑖) = (𝑦‘0))
75	73, 74	eqeq12d 2839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 0 → ((𝑥‘𝑖) = (𝑦‘𝑖) ↔ (𝑥‘0) = (𝑦‘0)))
76	75	rspcv 3620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ∈ (0..^𝑁) → (∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖) → (𝑥‘0) = (𝑦‘0)))
77	72, 76	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖) → (𝑥‘0) = (𝑦‘0)))
78	69, 77	sylbid 242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → (𝑥‘0) = (𝑦‘0)))
79	78	imp 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥‘0) = (𝑦‘0))
80		simpr 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (lastS‘𝑥) = (𝑥‘0))
81		simpr 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (lastS‘𝑦) = (𝑦‘0))
82	80, 81	eqeqan12rd 2842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → ((lastS‘𝑥) = (lastS‘𝑦) ↔ (𝑥‘0) = (𝑦‘0)))
83	82	ad2antlr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → ((lastS‘𝑥) = (lastS‘𝑦) ↔ (𝑥‘0) = (𝑦‘0)))
84	79, 83	mpbird 259	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (lastS‘𝑥) = (lastS‘𝑦))
85	24, 40, 84	jca32 518	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → ((♯‘𝑥) = (♯‘𝑦) ∧ ((𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)) ∧ (lastS‘𝑥) = (lastS‘𝑦))))
86	42	adantl 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → 𝑥 ∈ Word (Vtx‘𝐺))
87	86	adantl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑥 ∈ Word (Vtx‘𝐺))
88	41	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → 𝑦 ∈ Word (Vtx‘𝐺))
89	88	adantl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑦 ∈ Word (Vtx‘𝐺))
90		1red 10644	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℝ)
91		nngt0 11671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
92		0lt1 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 < 1
93	92	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 0 < 1)
94	49, 90, 91, 93	addgt0d 11217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → 0 < (𝑁 + 1))
95		breq2 5072	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (0 < (♯‘𝑥) ↔ 0 < (𝑁 + 1)))
96	94, 95	syl5ibr 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ∈ ℕ → 0 < (♯‘𝑥)))
97	96	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 0 < (♯‘𝑥)))
98	97	adantl 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 0 < (♯‘𝑥)))
99	98	impcom 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 0 < (♯‘𝑥))
100	87, 89, 99	3jca 1124	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥)))
101	100	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥)))
102		pfxsuff1eqwrdeq 14063	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥)) → (𝑥 = 𝑦 ↔ ((♯‘𝑥) = (♯‘𝑦) ∧ ((𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)) ∧ (lastS‘𝑥) = (lastS‘𝑦)))))
103	101, 102	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥 = 𝑦 ↔ ((♯‘𝑥) = (♯‘𝑦) ∧ ((𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)) ∧ (lastS‘𝑥) = (lastS‘𝑦)))))
104	85, 103	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → 𝑥 = 𝑦)
105	104	exp31 422	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))
106	105	expdcom 417	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))))
107	106	ex 415	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) → ((lastS‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))))
108	107	3adant3 1128	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((lastS‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))))
109	20, 108	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑁 WWalksN 𝐺) → ((lastS‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))))
110	109	imp 409	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))))
111	110	expdcom 417	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) → ((lastS‘𝑥) = (𝑥‘0) → ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))))
112	111	3adant3 1128	. . . . . . . . 9 ⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥‘𝑖), (𝑥‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((lastS‘𝑥) = (𝑥‘0) → ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))))
113	19, 112	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑁 WWalksN 𝐺) → ((lastS‘𝑥) = (𝑥‘0) → ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))))
114	113	imp31 420	. . . . . . 7 ⊢ (((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))
115	114	com12 32	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))
116	16, 115	syl5bi 244	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))
117	116	imp 409	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))
118	7, 117	sylbid 242	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
119	118	ralrimivva 3193	. 2 ⊢ (𝑁 ∈ ℕ → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
120		dff13 7015	. 2 ⊢ (𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺) ↔ (𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
121	3, 119, 120	sylanbrc 585	1 ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ∀wral 3140 {crab 3144 {cpr 4571 ⟨cop 4575 class class class wbr 5068 ↦ cmpt 5148 ⟶wf 6353 –1-1→wf1 6354 ‘cfv 6357 (class class class)co 7158 ℂcc 10537 0cc0 10539 1c1 10540 + caddc 10542 < clt 10677 ≤ cle 10678 − cmin 10872 ℕcn 11640 ℕ₀cn0 11900 ..^cfzo 13036 ♯chash 13693 Word cword 13864 lastSclsw 13916 substr csubstr 14004 prefix cpfx 14034 Vtxcvtx 26783 Edgcedg 26834 WWalksN cwwlksn 27606 ClWWalksN cclwwlkn 27804

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-oadd 8108 df-er 8291 df-map 8410 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-nn 11641 df-n0 11901 df-xnn0 11971 df-z 11985 df-uz 12247 df-fz 12896 df-fzo 13037 df-hash 13694 df-word 13865 df-lsw 13917 df-s1 13952 df-substr 14005 df-pfx 14035 df-wwlks 27610 df-wwlksn 27611 df-clwwlk 27762 df-clwwlkn 27805

This theorem is referenced by: clwwlkf1o 27832

W3C validator