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 30011

Description: Lemma 3 for clwwlkf1o 30013: 𝐹 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 30009	. 2 ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))
4	1, 2	clwwlkfv 30010	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = (𝑥 prefix 𝑁))
5	1, 2	clwwlkfv 30010	. . . . . 6 ⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) = (𝑦 prefix 𝑁))
6	4, 5	eqeqan12d 2743	. . . . 5 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)))
7	6	adantl 481	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)))
8		fveq2 6826	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (lastS‘𝑤) = (lastS‘𝑥))
9		fveq1 6825	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0))
10	8, 9	eqeq12d 2745	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑥) = (𝑥‘0)))
11	10, 1	elrab2 3653	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)))
12		fveq2 6826	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (lastS‘𝑤) = (lastS‘𝑦))
13		fveq1 6825	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0))
14	12, 13	eqeq12d 2745	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑦) = (𝑦‘0)))
15	14, 1	elrab2 3653	. . . . . . 7 ⊢ (𝑦 ∈ 𝐷 ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)))
16	11, 15	anbi12i 628	. . . . . 6 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ↔ ((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))))
17		eqid 2729	. . . . . . . . . 10 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
18		eqid 2729	. . . . . . . . . 10 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
19	17, 18	wwlknp 29806	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥‘𝑖), (𝑥‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
20	17, 18	wwlknp 29806	. . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . . . . . . . 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 12154	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
26		ax-1cn 11086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1 ∈ ℂ
27		pncan 11387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
28	27	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → 𝑁 = ((𝑁 + 1) − 1))
29	25, 26, 28	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ → 𝑁 = ((𝑁 + 1) − 1))
30		oveq1 7360	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑥) = (𝑁 + 1) → ((♯‘𝑥) − 1) = ((𝑁 + 1) − 1))
31	30	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑥) = (𝑁 + 1) → ((𝑁 + 1) − 1) = ((♯‘𝑥) − 1))
32	29, 31	sylan9eqr 2786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → 𝑁 = ((♯‘𝑥) − 1))
33	32	oveq2d 7369	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑥 prefix 𝑁) = (𝑥 prefix ((♯‘𝑥) − 1)))
34	32	oveq2d 7369	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑦 prefix 𝑁) = (𝑦 prefix ((♯‘𝑥) − 1)))
35	33, 34	eqeq12d 2745	. . . . . . . . . . . . . . . . . . . . . . . 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 12409	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
46		0nn0 12417	. . . . . . . . . . . . . . . . . . . . . . . . 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 12153	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
50	49	lep1d 12074	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1))
51		breq2 5099	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5099	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 14598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ₀) → (𝑥 prefix 𝑁) = (𝑥 substr ⟨0, 𝑁⟩))
62	61	ad2ant2rl 749	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (𝑥 prefix 𝑁) = (𝑥 substr ⟨0, 𝑁⟩))
63		pfxval 14598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ₀) → (𝑦 prefix 𝑁) = (𝑦 substr ⟨0, 𝑁⟩))
64	63	ad2ant2l 746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (𝑦 prefix 𝑁) = (𝑦 substr ⟨0, 𝑁⟩))
65	62, 64	eqeq12d 2745	. . . . . . . . . . . . . . . . . . . . . . . . 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 14590	. . . . . . . . . . . . . . . . . . . . . . . 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 13620	. . . . . . . . . . . . . . . . . . . . . . . . 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 6826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 0 → (𝑥‘𝑖) = (𝑥‘0))
74		fveq2 6826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 0 → (𝑦‘𝑖) = (𝑦‘0))
75	73, 74	eqeq12d 2745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 0 → ((𝑥‘𝑖) = (𝑦‘𝑖) ↔ (𝑥‘0) = (𝑦‘0)))
76	75	rspcv 3575	. . . . . . . . . . . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . . . . . . . . . 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 11135	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℝ)
91		nngt0 12177	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
92		0lt1 11660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 < 1
93	92	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 0 < 1)
94	49, 90, 91, 93	addgt0d 11713	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → 0 < (𝑁 + 1))
95		breq2 5099	. . . . . . . . . . . . . . . . . . . . . . . . 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 14623	. . . . . . . . . . . . . . . . . . 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 3172	. 2 ⊢ (𝑁 ∈ ℕ → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
120		dff13 7195	. 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 2109 ∀wral 3044 {crab 3396 {cpr 4581 ⟨cop 4585 class class class wbr 5095 ↦ cmpt 5176 ⟶wf 6482 –1-1→wf1 6483 ‘cfv 6486 (class class class)co 7353 ℂcc 11026 0cc0 11028 1c1 11029 + caddc 11031 < clt 11168 ≤ cle 11169 − cmin 11365 ℕcn 12146 ℕ₀cn0 12402 ..^cfzo 13575 ♯chash 14255 Word cword 14438 lastSclsw 14487 substr csubstr 14565 prefix cpfx 14595 Vtxcvtx 28959 Edgcedg 29010 WWalksN cwwlksn 29789 ClWWalksN cclwwlkn 29986

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105

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 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8632 df-map 8762 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-nn 12147 df-n0 12403 df-xnn0 12476 df-z 12490 df-uz 12754 df-fz 13429 df-fzo 13576 df-hash 14256 df-word 14439 df-lsw 14488 df-s1 14521 df-substr 14566 df-pfx 14596 df-wwlks 29793 df-wwlksn 29794 df-clwwlk 29944 df-clwwlkn 29987

This theorem is referenced by: clwwlkf1o 30013

W3C validator