Step | Hyp | Ref
| Expression |
1 | | clwwlkf1o.d |
. . 3
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)} |
2 | | clwwlkf1o.f |
. . 3
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁)) |
3 | 1, 2 | clwwlkf 28157 |
. 2
⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺)) |
4 | 1, 2 | clwwlkfv 28158 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = (𝑥 prefix 𝑁)) |
5 | 1, 2 | clwwlkfv 28158 |
. . . . . 6
⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) = (𝑦 prefix 𝑁)) |
6 | 4, 5 | eqeqan12d 2752 |
. . . . 5
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁))) |
7 | 6 | adantl 485 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁))) |
8 | | fveq2 6736 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (lastS‘𝑤) = (lastS‘𝑥)) |
9 | | fveq1 6735 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0)) |
10 | 8, 9 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑥) = (𝑥‘0))) |
11 | 10, 1 | elrab2 3618 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0))) |
12 | | fveq2 6736 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (lastS‘𝑤) = (lastS‘𝑦)) |
13 | | fveq1 6735 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0)) |
14 | 12, 13 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑦) = (𝑦‘0))) |
15 | 14, 1 | elrab2 3618 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐷 ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))) |
16 | 11, 15 | anbi12i 630 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ↔ ((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)))) |
17 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
18 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
19 | 17, 18 | wwlknp 27954 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥‘𝑖), (𝑥‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
20 | 17, 18 | wwlknp 27954 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝑁 WWalksN 𝐺) → (𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
21 | | simprlr 780 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑥) = (𝑁 + 1)) |
22 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (♯‘𝑦) = (𝑁 + 1)) |
23 | 21, 22 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . . . . 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 11863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
26 | | ax-1cn 10812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
ℂ |
27 | | pncan 11109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
28 | 27 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → 𝑁 = ((𝑁 + 1) −
1)) |
29 | 25, 26, 28 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝑁 = ((𝑁 + 1) − 1)) |
30 | | oveq1 7239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑥) =
(𝑁 + 1) →
((♯‘𝑥) −
1) = ((𝑁 + 1) −
1)) |
31 | 30 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝑥) =
(𝑁 + 1) → ((𝑁 + 1) − 1) =
((♯‘𝑥) −
1)) |
32 | 29, 31 | sylan9eqr 2801 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝑥)
= (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → 𝑁 = ((♯‘𝑥) − 1)) |
33 | 32 | oveq2d 7248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝑥)
= (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑥 prefix 𝑁) = (𝑥 prefix ((♯‘𝑥) − 1))) |
34 | 32 | oveq2d 7248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝑥)
= (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑦 prefix 𝑁) = (𝑦 prefix ((♯‘𝑥) − 1))) |
35 | 33, 34 | eqeq12d 2754 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝑥)
= (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))) |
36 | 35 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . 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 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1))))) |
39 | 38 | impcom 411 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)))) |
40 | 39 | biimpa 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1))) |
41 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → 𝑦 ∈ Word (Vtx‘𝐺)) |
42 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → 𝑥 ∈ Word (Vtx‘𝐺)) |
43 | 41, 42 | anim12ci 617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺))) |
44 | 43 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺))) |
45 | | nnnn0 12122 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
46 | | 0nn0 12130 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
ℕ0 |
47 | 45, 46 | jctil 523 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → (0 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) |
48 | 47 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (0 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) |
49 | | nnre 11862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
50 | 49 | lep1d 11788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1)) |
51 | | breq2 5072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝑥) =
(𝑁 + 1) → (𝑁 ≤ (♯‘𝑥) ↔ 𝑁 ≤ (𝑁 + 1))) |
52 | 50, 51 | syl5ibr 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝑥) =
(𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥))) |
53 | 52 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥))) |
54 | 53 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑥))) |
55 | 54 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (♯‘𝑥)) |
56 | | breq2 5072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝑦) =
(𝑁 + 1) → (𝑁 ≤ (♯‘𝑦) ↔ 𝑁 ≤ (𝑁 + 1))) |
57 | 50, 56 | syl5ibr 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝑦) =
(𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦))) |
58 | 57 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦))) |
59 | 58 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (♯‘𝑦))) |
60 | 59 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (♯‘𝑦)) |
61 | | pfxval 14266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ0) → (𝑥 prefix 𝑁) = (𝑥 substr 〈0, 𝑁〉)) |
62 | 61 | ad2ant2rl 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0)) → (𝑥 prefix 𝑁) = (𝑥 substr 〈0, 𝑁〉)) |
63 | | pfxval 14266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ0) → (𝑦 prefix 𝑁) = (𝑦 substr 〈0, 𝑁〉)) |
64 | 63 | ad2ant2l 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0)) → (𝑦 prefix 𝑁) = (𝑦 substr 〈0, 𝑁〉)) |
65 | 62, 64 | eqeq12d 2754 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0)) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉))) |
66 | 65 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉))) |
67 | | swrdspsleq 14258 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))) |
68 | 66, 67 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ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 13307 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
71 | 70 | biimpri 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 0 ∈
(0..^𝑁)) |
72 | 71 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 0 ∈ (0..^𝑁)) |
73 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 0 → (𝑥‘𝑖) = (𝑥‘0)) |
74 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 0 → (𝑦‘𝑖) = (𝑦‘0)) |
75 | 73, 74 | eqeq12d 2754 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = 0 → ((𝑥‘𝑖) = (𝑦‘𝑖) ↔ (𝑥‘0) = (𝑦‘0))) |
76 | 75 | rspcv 3545 |
. . . . . . . . . . . . . . . . . . . . . . 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 243 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → (𝑥‘0) = (𝑦‘0))) |
79 | 78 | imp 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥‘0) = (𝑦‘0)) |
80 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (lastS‘𝑥) = (𝑥‘0)) |
81 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (lastS‘𝑦) = (𝑦‘0)) |
82 | 80, 81 | eqeqan12rd 2753 |
. . . . . . . . . . . . . . . . . . . . 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 260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (lastS‘𝑥) = (lastS‘𝑦)) |
85 | 24, 40, 84 | jca32 519 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → ((♯‘𝑥) = (♯‘𝑦) ∧ ((𝑥 prefix ((♯‘𝑥) − 1)) = (𝑦 prefix ((♯‘𝑥) − 1)) ∧ (lastS‘𝑥) = (lastS‘𝑦)))) |
86 | 42 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → 𝑥 ∈ Word (Vtx‘𝐺)) |
87 | 86 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑥 ∈ Word (Vtx‘𝐺)) |
88 | 41 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → 𝑦 ∈ Word (Vtx‘𝐺)) |
89 | 88 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 𝑦 ∈ Word (Vtx‘𝐺)) |
90 | | 1red 10859 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
91 | | nngt0 11886 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
92 | | 0lt1 11379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 <
1 |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 0 <
1) |
94 | 49, 90, 91, 93 | addgt0d 11432 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 0 <
(𝑁 + 1)) |
95 | | breq2 5072 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑥) =
(𝑁 + 1) → (0 <
(♯‘𝑥) ↔ 0
< (𝑁 +
1))) |
96 | 94, 95 | syl5ibr 249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑥) =
(𝑁 + 1) → (𝑁 ∈ ℕ → 0 <
(♯‘𝑥))) |
97 | 96 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 0 <
(♯‘𝑥))) |
98 | 97 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 0 <
(♯‘𝑥))) |
99 | 98 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → 0 <
(♯‘𝑥)) |
100 | 87, 89, 99 | 3jca 1130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥))) |
101 | 100 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺) ∧ 0 < (♯‘𝑥))) |
102 | | pfxsuff1eqwrdeq 14292 |
. . . . . . . . . . . . . . . . . . 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 260 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) ∧ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁)) → 𝑥 = 𝑦) |
105 | 104 | exp31 423 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → ((((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))) |
106 | 105 | expdcom 418 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))) |
107 | 106 | ex 416 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) → ((lastS‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))))) |
108 | 107 | 3adant3 1134 |
. . . . . . . . . . . . 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 410 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)))) |
111 | 110 | expdcom 418 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) → ((lastS‘𝑥) = (𝑥‘0) → ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))))) |
112 | 111 | 3adant3 1134 |
. . . . . . . . 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 421 |
. . . . . . 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 245 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦))) |
117 | 116 | imp 410 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) → 𝑥 = 𝑦)) |
118 | 7, 117 | sylbid 243 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
119 | 118 | ralrimivva 3113 |
. 2
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
120 | | dff13 7086 |
. 2
⊢ (𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺) ↔ (𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
121 | 3, 119, 120 | sylanbrc 586 |
1
⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺)) |