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 30030

Description: Lemma 3 for clwwlkf1o 30032: 𝐹 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 30028	. 2 ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))
4	1, 2	clwwlkfv 30029	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = (𝑥 prefix 𝑁))
5	1, 2	clwwlkfv 30029	. . . . . 6 ⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) = (𝑦 prefix 𝑁))
6	4, 5	eqeqan12d 2749	. . . . 5 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)))
7	6	adantl 481	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)))
8		fveq2 6876	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (lastS‘𝑤) = (lastS‘𝑥))
9		fveq1 6875	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0))
10	8, 9	eqeq12d 2751	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑥) = (𝑥‘0)))
11	10, 1	elrab2 3674	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)))
12		fveq2 6876	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (lastS‘𝑤) = (lastS‘𝑦))
13		fveq1 6875	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0))
14	12, 13	eqeq12d 2751	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑦) = (𝑦‘0)))
15	14, 1	elrab2 3674	. . . . . . 7 ⊢ (𝑦 ∈ 𝐷 ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)))
16	11, 15	anbi12i 628	. . . . . 6 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ↔ ((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))))
17		eqid 2735	. . . . . . . . . 10 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
18		eqid 2735	. . . . . . . . . 10 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
19	17, 18	wwlknp 29825	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥‘𝑖), (𝑥‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
20	17, 18	wwlknp 29825	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝑁 WWalksN 𝐺) → (𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
21		simprlr 779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑥) = (𝑁 + 1))
22		simpllr 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑦) = (𝑁 + 1))
23	21, 22	eqtr4d 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑥) = (♯‘𝑦))
24	23	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (♯‘𝑥) = (♯‘𝑦))
25		nncn 12248	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
26		ax-1cn 11187	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1 ∈ ℂ
27		pncan 11488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
28	27	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → 𝑁 = ((𝑁 + 1) − 1))
29	25, 26, 28	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ → 𝑁 = ((𝑁 + 1) − 1))
30		oveq1 7412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑥) = (𝑁 + 1) → ((♯‘𝑥) − 1) = ((𝑁 + 1) − 1))
31	30	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑥) = (𝑁 + 1) → ((𝑁 + 1) − 1) = ((♯‘𝑥) − 1))
32	29, 31	sylan9eqr 2792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → 𝑁 = ((♯‘𝑥) − 1))
33	32	oveq2d 7421	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑥 prefix 𝑁) = (𝑥 prefix ((♯‘𝑥) − 1)))
34	32	oveq2d 7421	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑦 prefix 𝑁) = (𝑦 prefix ((♯‘𝑥) − 1)))
35	33, 34	eqeq12d 2751	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1))))
36	35	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))))
37	36	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))))
38	37	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))))
39	38	impcom 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1))))
40	39	biimpa 476	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))
41		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → 𝑦 ∈ Word (Vtx‘𝐺))
42		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → 𝑥 ∈ Word (Vtx‘𝐺))
43	41, 42	anim12ci 614	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)))
44	43	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)))
45		nnnn0 12508	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
46		0nn0 12516	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℕ₀
47	45, 46	jctil 519	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀))
48	47	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀))
49		nnre 12247	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
50	49	lep1d 12173	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1))
51		breq2 5123	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝑥) ↔ 𝑁 ≤ (𝑁 + 1)))
52	50, 51	imbitrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥)))
53	52	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥)))
54	53	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥)))
55	54	impcom 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (♯‘𝑥))
56		breq2 5123	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑦) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝑦) ↔ 𝑁 ≤ (𝑁 + 1)))
57	50, 56	imbitrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝑦) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦)))
58	57	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦)))
59	58	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦)))
60	59	impcom 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (♯‘𝑦))
61		pfxval 14691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ₀) → (𝑥 prefix 𝑁) = (𝑥 substr ⟨0, 𝑁⟩))
62	61	ad2ant2rl 749	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (𝑥 prefix 𝑁) = (𝑥 substr ⟨0, 𝑁⟩))
63		pfxval 14691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ₀) → (𝑦 prefix 𝑁) = (𝑦 substr ⟨0, 𝑁⟩))
64	63	ad2ant2l 746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (𝑦 prefix 𝑁) = (𝑦 substr ⟨0, 𝑁⟩))
65	62, 64	eqeq12d 2751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)))
66	65	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)))
67		swrdspsleq 14683	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
68	66, 67	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
69	44, 48, 55, 60, 68	syl112anc 1376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
70		lbfzo0 13716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
71	70	biimpri 228	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 0 ∈ (0..^𝑁))
72	71	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 0 ∈ (0..^𝑁))
73		fveq2 6876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 0 → (𝑥‘𝑖) = (𝑥‘0))
74		fveq2 6876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 0 → (𝑦‘𝑖) = (𝑦‘0))
75	73, 74	eqeq12d 2751	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 0 → ((𝑥‘𝑖) = (𝑦‘𝑖) ↔ (𝑥‘0) = (𝑦‘0)))
76	75	rspcv 3597	. . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → (𝑥‘0) = (𝑦‘0)))
79	78	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥‘0) = (𝑦‘0))
80		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (lastS‘𝑥) = (𝑥‘0))
81		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (lastS‘𝑦) = (𝑦‘0))
82	80, 81	eqeqan12rd 2750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → ((lastS‘𝑥) = (lastS‘𝑦) ↔ (𝑥‘0) = (𝑦‘0)))
83	82	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → ((lastS‘𝑥) = (lastS‘𝑦) ↔ (𝑥‘0) = (𝑦‘0)))
84	79, 83	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (lastS‘𝑥) = (lastS‘𝑦))
85	24, 40, 84	jca32 515	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → ((♯‘𝑥) = (♯‘𝑦) ∧ ((𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)) ∧ (lastS‘𝑥) = (lastS‘𝑦))))
86	42	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → 𝑥 ∈ Word (Vtx‘𝐺))
87	86	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑥 ∈ Word (Vtx‘𝐺))
88	41	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → 𝑦 ∈ Word (Vtx‘𝐺))
89	88	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑦 ∈ Word (Vtx‘𝐺))
90		1red 11236	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℝ)
91		nngt0 12271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
92		0lt1 11759	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 < 1
93	92	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 0 < 1)
94	49, 90, 91, 93	addgt0d 11812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → 0 < (𝑁 + 1))
95		breq2 5123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (0 < (♯‘𝑥) ↔ 0 < (𝑁 + 1)))
96	94, 95	imbitrrid 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ∈ ℕ → 0 < (♯‘𝑥)))
97	96	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 0 < (♯‘𝑥)))
98	97	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 0 < (♯‘𝑥)))
99	98	impcom 407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 0 < (♯‘𝑥))
100	87, 89, 99	3jca 1128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥)))
101	100	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥)))
102		pfxsuff1eqwrdeq 14717	. . . . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → 𝑥 = 𝑦)
105	104	exp31 419	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))
106	105	expdcom 414	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))))
107	106	ex 412	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) → ((lastS‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))))
108	107	3adant3 1132	. . . . . . . . . . . . 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 406	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))))
111	110	expdcom 414	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) → ((lastS‘𝑥) = (𝑥‘0) → ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))))
112	111	3adant3 1132	. . . . . . . . 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 417	. . . . . . 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	biimtrid 242	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))
117	116	imp 406	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))
118	7, 117	sylbid 240	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
119	118	ralrimivva 3187	. 2 ⊢ (𝑁 ∈ ℕ → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
120		dff13 7247	. 2 ⊢ (𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺) ↔ (𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
121	3, 119, 120	sylanbrc 583	1 ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ∀wral 3051 {crab 3415 {cpr 4603 ⟨cop 4607 class class class wbr 5119 ↦ cmpt 5201 ⟶wf 6527 –1-1→wf1 6528 ‘cfv 6531 (class class class)co 7405 ℂcc 11127 0cc0 11129 1c1 11130 + caddc 11132 < clt 11269 ≤ cle 11270 − cmin 11466 ℕcn 12240 ℕ₀cn0 12501 ..^cfzo 13671 ♯chash 14348 Word cword 14531 lastSclsw 14580 substr csubstr 14658 prefix cpfx 14688 Vtxcvtx 28975 Edgcedg 29026 WWalksN cwwlksn 29808 ClWWalksN cclwwlkn 30005

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-er 8719 df-map 8842 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-card 9953 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-nn 12241 df-n0 12502 df-xnn0 12575 df-z 12589 df-uz 12853 df-fz 13525 df-fzo 13672 df-hash 14349 df-word 14532 df-lsw 14581 df-s1 14614 df-substr 14659 df-pfx 14689 df-wwlks 29812 df-wwlksn 29813 df-clwwlk 29963 df-clwwlkn 30006

This theorem is referenced by: clwwlkf1o 30032

W3C validator