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

Theorem clwwlkf1 27178
 Description: Lemma 3 for clwwlkf1o 27180: F is a 1-1 function. (Contributed by AV, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.)
Hypotheses
Ref Expression
clwwlkf1o.d 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)}
clwwlkf1o.f 𝐹 = (𝑡𝐷 ↦ (𝑡 substr ⟨0, 𝑁⟩))
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.
StepHypRef Expression
1 clwwlkf1o.d . . 3 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)}
2 clwwlkf1o.f . . 3 𝐹 = (𝑡𝐷 ↦ (𝑡 substr ⟨0, 𝑁⟩))
31, 2clwwlkf 27176 . 2 (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))
41, 2clwwlkfv 27177 . . . . . 6 (𝑥𝐷 → (𝐹𝑥) = (𝑥 substr ⟨0, 𝑁⟩))
51, 2clwwlkfv 27177 . . . . . 6 (𝑦𝐷 → (𝐹𝑦) = (𝑦 substr ⟨0, 𝑁⟩))
64, 5eqeqan12d 2776 . . . . 5 ((𝑥𝐷𝑦𝐷) → ((𝐹𝑥) = (𝐹𝑦) ↔ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)))
76adantl 473 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑥𝐷𝑦𝐷)) → ((𝐹𝑥) = (𝐹𝑦) ↔ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)))
8 fveq2 6352 . . . . . . . . 9 (𝑤 = 𝑥 → (lastS‘𝑤) = (lastS‘𝑥))
9 fveq1 6351 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0))
108, 9eqeq12d 2775 . . . . . . . 8 (𝑤 = 𝑥 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑥) = (𝑥‘0)))
1110, 1elrab2 3507 . . . . . . 7 (𝑥𝐷 ↔ (𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)))
12 fveq2 6352 . . . . . . . . 9 (𝑤 = 𝑦 → (lastS‘𝑤) = (lastS‘𝑦))
13 fveq1 6351 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0))
1412, 13eqeq12d 2775 . . . . . . . 8 (𝑤 = 𝑦 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑦) = (𝑦‘0)))
1514, 1elrab2 3507 . . . . . . 7 (𝑦𝐷 ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)))
1611, 15anbi12i 735 . . . . . 6 ((𝑥𝐷𝑦𝐷) ↔ ((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))))
17 eqid 2760 . . . . . . . . . 10 (Vtx‘𝐺) = (Vtx‘𝐺)
18 eqid 2760 . . . . . . . . . 10 (Edg‘𝐺) = (Edg‘𝐺)
1917, 18wwlknp 26946 . . . . . . . . 9 (𝑥 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥𝑖), (𝑥‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
2017, 18wwlknp 26946 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑁 WWalksN 𝐺) → (𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
21 simprlr 822 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑥) = (𝑁 + 1))
22 simpllr 817 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑦) = (𝑁 + 1))
2321, 22eqtr4d 2797 . . . . . . . . . . . . . . . . . . . 20 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑥) = (♯‘𝑦))
2423ad2antlr 765 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)) → (♯‘𝑥) = (♯‘𝑦))
25 nncn 11220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
26 ax-1cn 10186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
27 pncan 10479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
2827eqcomd 2766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → 𝑁 = ((𝑁 + 1) − 1))
2925, 26, 28sylancl 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℕ → 𝑁 = ((𝑁 + 1) − 1))
30 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝑥) = (𝑁 + 1) → ((♯‘𝑥) − 1) = ((𝑁 + 1) − 1))
3130eqcomd 2766 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((♯‘𝑥) = (𝑁 + 1) → ((𝑁 + 1) − 1) = ((♯‘𝑥) − 1))
3229, 31sylan9eqr 2816 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → 𝑁 = ((♯‘𝑥) − 1))
3332opeq2d 4560 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ⟨0, 𝑁⟩ = ⟨0, ((♯‘𝑥) − 1)⟩)
3433oveq2d 6829 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑥 substr ⟨0, 𝑁⟩) = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩))
3533oveq2d 6829 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑦 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩))
3634, 35eqeq12d 2775 . . . . . . . . . . . . . . . . . . . . . . . 24 (((♯‘𝑥) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) ↔ (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩)))
3736ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) ↔ (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩))))
3837ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) ↔ (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩))))
3938adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) ↔ (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩))))
4039impcom 445 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) ↔ (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩)))
4140biimpa 502 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)) → (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩))
42 simpll 807 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → 𝑦 ∈ Word (Vtx‘𝐺))
43 simpll 807 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → 𝑥 ∈ Word (Vtx‘𝐺))
4442, 43anim12ci 592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)))
4544adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)))
46 nnnn0 11491 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
47 0nn0 11499 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ ℕ0
4846, 47jctil 561 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → (0 ∈ ℕ0𝑁 ∈ ℕ0))
4948adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (0 ∈ ℕ0𝑁 ∈ ℕ0))
50 nnre 11219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
5150lep1d 11147 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1))
52 breq2 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝑥) ↔ 𝑁 ≤ (𝑁 + 1)))
5351, 52syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥)))
5453ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥)))
5554adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥)))
5655impcom 445 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (♯‘𝑥))
57 breq2 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((♯‘𝑦) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝑦) ↔ 𝑁 ≤ (𝑁 + 1)))
5851, 57syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((♯‘𝑦) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦)))
5958ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦)))
6059adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦)))
6160impcom 445 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (♯‘𝑦))
62 swrdspsleq 13649 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥𝑖) = (𝑦𝑖)))
6345, 49, 56, 61, 62syl112anc 1481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥𝑖) = (𝑦𝑖)))
64 lbfzo0 12702 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
6564biimpri 218 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 0 ∈ (0..^𝑁))
6665adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 0 ∈ (0..^𝑁))
67 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 0 → (𝑥𝑖) = (𝑥‘0))
68 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 0 → (𝑦𝑖) = (𝑦‘0))
6967, 68eqeq12d 2775 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 0 → ((𝑥𝑖) = (𝑦𝑖) ↔ (𝑥‘0) = (𝑦‘0)))
7069rspcv 3445 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ (0..^𝑁) → (∀𝑖 ∈ (0..^𝑁)(𝑥𝑖) = (𝑦𝑖) → (𝑥‘0) = (𝑦‘0)))
7166, 70syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (∀𝑖 ∈ (0..^𝑁)(𝑥𝑖) = (𝑦𝑖) → (𝑥‘0) = (𝑦‘0)))
7263, 71sylbid 230 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → (𝑥‘0) = (𝑦‘0)))
7372imp 444 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)) → (𝑥‘0) = (𝑦‘0))
74 simpr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (lastS‘𝑥) = (𝑥‘0))
75 simpr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (lastS‘𝑦) = (𝑦‘0))
7674, 75eqeqan12rd 2778 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → ((lastS‘𝑥) = (lastS‘𝑦) ↔ (𝑥‘0) = (𝑦‘0)))
7776ad2antlr 765 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)) → ((lastS‘𝑥) = (lastS‘𝑦) ↔ (𝑥‘0) = (𝑦‘0)))
7873, 77mpbird 247 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)) → (lastS‘𝑥) = (lastS‘𝑦))
7924, 41, 78jca32 559 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)) → ((♯‘𝑥) = (♯‘𝑦) ∧ ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∧ (lastS‘𝑥) = (lastS‘𝑦))))
8043adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → 𝑥 ∈ Word (Vtx‘𝐺))
8180adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑥 ∈ Word (Vtx‘𝐺))
8242adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → 𝑦 ∈ Word (Vtx‘𝐺))
8382adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑦 ∈ Word (Vtx‘𝐺))
84 1red 10247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → 1 ∈ ℝ)
85 nngt0 11241 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → 0 < 𝑁)
86 0lt1 10742 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 < 1
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → 0 < 1)
8850, 84, 85, 87addgt0d 10794 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 0 < (𝑁 + 1))
89 breq2 4808 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((♯‘𝑥) = (𝑁 + 1) → (0 < (♯‘𝑥) ↔ 0 < (𝑁 + 1)))
9088, 89syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . 24 ((♯‘𝑥) = (𝑁 + 1) → (𝑁 ∈ ℕ → 0 < (♯‘𝑥)))
9190ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 0 < (♯‘𝑥)))
9291adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 0 < (♯‘𝑥)))
9392impcom 445 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 0 < (♯‘𝑥))
9481, 83, 933jca 1123 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥)))
9594adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥)))
96 2swrd1eqwrdeq 13654 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥)) → (𝑥 = 𝑦 ↔ ((♯‘𝑥) = (♯‘𝑦) ∧ ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∧ (lastS‘𝑥) = (lastS‘𝑦)))))
9795, 96syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)) → (𝑥 = 𝑦 ↔ ((♯‘𝑥) = (♯‘𝑦) ∧ ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) = (𝑦 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∧ (lastS‘𝑥) = (lastS‘𝑦)))))
9879, 97mpbird 247 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩)) → 𝑥 = 𝑦)
9998exp31 631 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))
10099expdcom 454 . . . . . . . . . . . . . . 15 (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦))))
101100ex 449 . . . . . . . . . . . . . 14 ((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) → ((lastS‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))))
1021013adant3 1127 . . . . . . . . . . . . 13 ((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((lastS‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))))
10320, 102syl 17 . . . . . . . . . . . 12 (𝑦 ∈ (𝑁 WWalksN 𝐺) → ((lastS‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))))
104103imp 444 . . . . . . . . . . 11 ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦))))
105104expdcom 454 . . . . . . . . . 10 ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) → ((lastS‘𝑥) = (𝑥‘0) → ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))))
1061053adant3 1127 . . . . . . . . 9 ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥𝑖), (𝑥‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((lastS‘𝑥) = (𝑥‘0) → ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))))
10719, 106syl 17 . . . . . . . 8 (𝑥 ∈ (𝑁 WWalksN 𝐺) → ((lastS‘𝑥) = (𝑥‘0) → ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))))
108107imp31 447 . . . . . . 7 (((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))) → (𝑁 ∈ ℕ → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))
109108com12 32 . . . . . 6 (𝑁 ∈ ℕ → (((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))
11016, 109syl5bi 232 . . . . 5 (𝑁 ∈ ℕ → ((𝑥𝐷𝑦𝐷) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦)))
111110imp 444 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑥𝐷𝑦𝐷)) → ((𝑥 substr ⟨0, 𝑁⟩) = (𝑦 substr ⟨0, 𝑁⟩) → 𝑥 = 𝑦))
1127, 111sylbid 230 . . 3 ((𝑁 ∈ ℕ ∧ (𝑥𝐷𝑦𝐷)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
113112ralrimivva 3109 . 2 (𝑁 ∈ ℕ → ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
114 dff13 6675 . 2 (𝐹:𝐷1-1→(𝑁 ClWWalksN 𝐺) ↔ (𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺) ∧ ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
1153, 113, 114sylanbrc 701 1 (𝑁 ∈ ℕ → 𝐹:𝐷1-1→(𝑁 ClWWalksN 𝐺))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139  ∀wral 3050  {crab 3054  {cpr 4323  ⟨cop 4327   class class class wbr 4804   ↦ cmpt 4881  ⟶wf 6045  –1-1→wf1 6046  ‘cfv 6049  (class class class)co 6813  ℂcc 10126  0cc0 10128  1c1 10129   + caddc 10131   < clt 10266   ≤ cle 10267   − cmin 10458  ℕcn 11212  ℕ0cn0 11484  ..^cfzo 12659  ♯chash 13311  Word cword 13477  lastSclsw 13478   substr csubstr 13481  Vtxcvtx 26073  Edgcedg 26138   WWalksN cwwlksn 26929   ClWWalksN cclwwlkn 27147 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-n0 11485  df-xnn0 11556  df-z 11570  df-uz 11880  df-fz 12520  df-fzo 12660  df-hash 13312  df-word 13485  df-lsw 13486  df-s1 13488  df-substr 13489  df-wwlks 26933  df-wwlksn 26934  df-clwwlk 27105  df-clwwlkn 27149 This theorem is referenced by:  clwwlkf1o  27180
 Copyright terms: Public domain W3C validator