| Step | Hyp | Ref
| Expression |
| 1 | | clwwlkf1o.d |
. . 3
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)} |
| 2 | | clwwlkf1o.f |
. . 3
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁)) |
| 3 | 1, 2 | clwwlkf 30066 |
. 2
⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺)) |
| 4 | 1, 2 | clwwlkfv 30067 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = (𝑥 prefix 𝑁)) |
| 5 | 1, 2 | clwwlkfv 30067 |
. . . . . 6
⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) = (𝑦 prefix 𝑁)) |
| 6 | 4, 5 | eqeqan12d 2751 |
. . . . 5
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁))) |
| 7 | 6 | adantl 481 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 prefix 𝑁) = (𝑦 prefix 𝑁))) |
| 8 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (lastS‘𝑤) = (lastS‘𝑥)) |
| 9 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0)) |
| 10 | 8, 9 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑥) = (𝑥‘0))) |
| 11 | 10, 1 | elrab2 3695 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0))) |
| 12 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (lastS‘𝑤) = (lastS‘𝑦)) |
| 13 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0)) |
| 14 | 12, 13 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑦) = (𝑦‘0))) |
| 15 | 14, 1 | elrab2 3695 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐷 ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0))) |
| 16 | 11, 15 | anbi12i 628 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ↔ ((𝑥 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑦) = (𝑦‘0)))) |
| 17 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 18 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 19 | 17, 18 | wwlknp 29863 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥‘𝑖), (𝑥‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 20 | 17, 18 | wwlknp 29863 |
. . . . . . . . . . . . 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 2780 |
. . . . . . . . . . . . . . . . . . . 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 12274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 26 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
ℂ |
| 27 | | pncan 11514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
| 28 | 27 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → 𝑁 = ((𝑁 + 1) −
1)) |
| 29 | 25, 26, 28 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝑁 = ((𝑁 + 1) − 1)) |
| 30 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑥) =
(𝑁 + 1) →
((♯‘𝑥) −
1) = ((𝑁 + 1) −
1)) |
| 31 | 30 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝑥) =
(𝑁 + 1) → ((𝑁 + 1) − 1) =
((♯‘𝑥) −
1)) |
| 32 | 29, 31 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝑥)
= (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → 𝑁 = ((♯‘𝑥) − 1)) |
| 33 | 32 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝑥)
= (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑥 prefix 𝑁) = (𝑥 prefix ((♯‘𝑥) − 1))) |
| 34 | 32 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝑥)
= (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑦 prefix 𝑁) = (𝑦 prefix ((♯‘𝑥) − 1))) |
| 35 | 33, 34 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . . 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 767 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) → 𝑦 ∈ Word (Vtx‘𝐺)) |
| 42 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 12533 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 46 | | 0nn0 12541 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
ℕ0 |
| 47 | 45, 46 | jctil 519 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → (0 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (lastS‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = (𝑁 + 1)) ∧ (lastS‘𝑥) = (𝑥‘0)))) → (0 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) |
| 49 | | nnre 12273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 50 | 49 | lep1d 12199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1)) |
| 51 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 14711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ0) → (𝑥 prefix 𝑁) = (𝑥 substr 〈0, 𝑁〉)) |
| 62 | 61 | ad2ant2rl 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0)) → (𝑥 prefix 𝑁) = (𝑥 substr 〈0, 𝑁〉)) |
| 63 | | pfxval 14711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0)) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉))) |
| 66 | 65 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 prefix 𝑁) = (𝑦 prefix 𝑁) ↔ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉))) |
| 67 | | swrdspsleq 14703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑦 ∈ Word (Vtx‘𝐺)) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0) ∧ (𝑁 ≤ (♯‘𝑥) ∧ 𝑁 ≤ (♯‘𝑦))) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))) |
| 68 | 66, 67 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . 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 13739 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 0 → (𝑥‘𝑖) = (𝑥‘0)) |
| 74 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 0 → (𝑦‘𝑖) = (𝑦‘0)) |
| 75 | 73, 74 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = 0 → ((𝑥‘𝑖) = (𝑦‘𝑖) ↔ (𝑥‘0) = (𝑦‘0))) |
| 76 | 75 | rspcv 3618 |
. . . . . . . . . . . . . . . . . . . . . . 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 2752 |
. . . . . . . . . . . . . . . . . . . . 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 11262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
| 91 | | nngt0 12297 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 92 | | 0lt1 11785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 <
1 |
| 93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 0 <
1) |
| 94 | 49, 90, 91, 93 | addgt0d 11838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 0 <
(𝑁 + 1)) |
| 95 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 1129 |
. . . . . . . . . . . . . . . . . . . 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 14737 |
. . . . . . . . . . . . . . . . . . 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 1133 |
. . . . . . . . . . . . 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 1133 |
. . . . . . . . 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 3202 |
. 2
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
| 120 | | dff13 7275 |
. 2
⊢ (𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺) ↔ (𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 121 | 3, 119, 120 | sylanbrc 583 |
1
⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺)) |