Proof of Theorem pthhashvtx
| Step | Hyp | Ref
| Expression |
| 1 | | hashfz0 14471 |
. . . 4
⊢
(((♯‘𝐹)
− 1) ∈ ℕ0 →
(♯‘(0...((♯‘𝐹) − 1))) = (((♯‘𝐹) − 1) +
1)) |
| 2 | | pthiswlk 29745 |
. . . . . 6
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
| 3 | | wlkcl 29633 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
| 4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
| 5 | | nn0cn 12536 |
. . . . 5
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℂ) |
| 6 | | npcan1 11688 |
. . . . 5
⊢
((♯‘𝐹)
∈ ℂ → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) |
| 7 | 4, 5, 6 | 3syl 18 |
. . . 4
⊢ (𝐹(Paths‘𝐺)𝑃 → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) |
| 8 | 1, 7 | sylan9eqr 2799 |
. . 3
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ0)
→ (♯‘(0...((♯‘𝐹) − 1))) = (♯‘𝐹)) |
| 9 | | pthhashvtx.1 |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
| 10 | 9 | wlkp 29634 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 11 | 2, 10 | syl 17 |
. . . . . 6
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 12 | 11 | ffnd 6737 |
. . . . 5
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝑃 Fn (0...(♯‘𝐹))) |
| 13 | | fzfi 14013 |
. . . . 5
⊢
(0...((♯‘𝐹) − 1)) ∈ Fin |
| 14 | | resfnfinfin 9377 |
. . . . 5
⊢ ((𝑃 Fn (0...(♯‘𝐹)) ∧
(0...((♯‘𝐹)
− 1)) ∈ Fin) → (𝑃 ↾ (0...((♯‘𝐹) − 1))) ∈
Fin) |
| 15 | 12, 13, 14 | sylancl 586 |
. . . 4
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (0...((♯‘𝐹) − 1))) ∈
Fin) |
| 16 | | simpr 484 |
. . . . 5
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ0)
→ ((♯‘𝐹)
− 1) ∈ ℕ0) |
| 17 | | fzssp1 13607 |
. . . . . . . 8
⊢
(0...((♯‘𝐹) − 1)) ⊆
(0...(((♯‘𝐹)
− 1) + 1)) |
| 18 | 7 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝐹(Paths‘𝐺)𝑃 → (0...(((♯‘𝐹) − 1) + 1)) =
(0...(♯‘𝐹))) |
| 19 | 17, 18 | sseqtrid 4026 |
. . . . . . 7
⊢ (𝐹(Paths‘𝐺)𝑃 → (0...((♯‘𝐹) − 1)) ⊆
(0...(♯‘𝐹))) |
| 20 | 11, 19 | fssresd 6775 |
. . . . . 6
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (0...((♯‘𝐹) −
1))):(0...((♯‘𝐹) − 1))⟶𝑉) |
| 21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ0)
→ (𝑃 ↾
(0...((♯‘𝐹)
− 1))):(0...((♯‘𝐹) − 1))⟶𝑉) |
| 22 | | fz1ssfz0 13663 |
. . . . . . . . 9
⊢
(1...((♯‘𝐹) − 1)) ⊆
(0...((♯‘𝐹)
− 1)) |
| 23 | 22 | a1i 11 |
. . . . . . . 8
⊢ (𝐹(Paths‘𝐺)𝑃 → (1...((♯‘𝐹) − 1)) ⊆
(0...((♯‘𝐹)
− 1))) |
| 24 | 20, 23 | fssresd 6775 |
. . . . . . 7
⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾
(1...((♯‘𝐹)
− 1))):(1...((♯‘𝐹) − 1))⟶𝑉) |
| 25 | | ispth 29741 |
. . . . . . . . 9
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) =
∅)) |
| 26 | 25 | simp2bi 1147 |
. . . . . . . 8
⊢ (𝐹(Paths‘𝐺)𝑃 → Fun ◡(𝑃 ↾ (1..^(♯‘𝐹)))) |
| 27 | | nn0z 12638 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℤ) |
| 28 | | fzoval 13700 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐹)
∈ ℤ → (1..^(♯‘𝐹)) = (1...((♯‘𝐹) − 1))) |
| 29 | 27, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹)
∈ ℕ0 → (1..^(♯‘𝐹)) = (1...((♯‘𝐹) − 1))) |
| 30 | 4, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹(Paths‘𝐺)𝑃 → (1..^(♯‘𝐹)) = (1...((♯‘𝐹) − 1))) |
| 31 | 30 | reseq2d 5997 |
. . . . . . . . . . 11
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (1..^(♯‘𝐹))) = (𝑃 ↾ (1...((♯‘𝐹) − 1)))) |
| 32 | | resabs1 6024 |
. . . . . . . . . . . 12
⊢
((1...((♯‘𝐹) − 1)) ⊆
(0...((♯‘𝐹)
− 1)) → ((𝑃
↾ (0...((♯‘𝐹) − 1))) ↾
(1...((♯‘𝐹)
− 1))) = (𝑃 ↾
(1...((♯‘𝐹)
− 1)))) |
| 33 | 22, 32 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑃 ↾
(0...((♯‘𝐹)
− 1))) ↾ (1...((♯‘𝐹) − 1))) = (𝑃 ↾ (1...((♯‘𝐹) − 1))) |
| 34 | 31, 33 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (1..^(♯‘𝐹))) = ((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾
(1...((♯‘𝐹)
− 1)))) |
| 35 | 34 | cnveqd 5886 |
. . . . . . . . 9
⊢ (𝐹(Paths‘𝐺)𝑃 → ◡(𝑃 ↾ (1..^(♯‘𝐹))) = ◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾
(1...((♯‘𝐹)
− 1)))) |
| 36 | 35 | funeqd 6588 |
. . . . . . . 8
⊢ (𝐹(Paths‘𝐺)𝑃 → (Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ↔ Fun ◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾
(1...((♯‘𝐹)
− 1))))) |
| 37 | 26, 36 | mpbid 232 |
. . . . . . 7
⊢ (𝐹(Paths‘𝐺)𝑃 → Fun ◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾
(1...((♯‘𝐹)
− 1)))) |
| 38 | | df-f1 6566 |
. . . . . . 7
⊢ (((𝑃 ↾
(0...((♯‘𝐹)
− 1))) ↾ (1...((♯‘𝐹) − 1))):(1...((♯‘𝐹) − 1))–1-1→𝑉 ↔ (((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾
(1...((♯‘𝐹)
− 1))):(1...((♯‘𝐹) − 1))⟶𝑉 ∧ Fun ◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾
(1...((♯‘𝐹)
− 1))))) |
| 39 | 24, 37, 38 | sylanbrc 583 |
. . . . . 6
⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾
(1...((♯‘𝐹)
− 1))):(1...((♯‘𝐹) − 1))–1-1→𝑉) |
| 40 | 39 | adantr 480 |
. . . . 5
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ0)
→ ((𝑃 ↾
(0...((♯‘𝐹)
− 1))) ↾ (1...((♯‘𝐹) − 1))):(1...((♯‘𝐹) − 1))–1-1→𝑉) |
| 41 | | snsspr1 4814 |
. . . . . . . 8
⊢ {0}
⊆ {0, (♯‘𝐹)} |
| 42 | | imass2 6120 |
. . . . . . . 8
⊢ ({0}
⊆ {0, (♯‘𝐹)} → (𝑃 “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)})) |
| 43 | 41, 42 | ax-mp 5 |
. . . . . . 7
⊢ (𝑃 “ {0}) ⊆ (𝑃 “ {0,
(♯‘𝐹)}) |
| 44 | | 0elfz 13664 |
. . . . . . . . 9
⊢
(((♯‘𝐹)
− 1) ∈ ℕ0 → 0 ∈
(0...((♯‘𝐹)
− 1))) |
| 45 | 44 | snssd 4809 |
. . . . . . . 8
⊢
(((♯‘𝐹)
− 1) ∈ ℕ0 → {0} ⊆
(0...((♯‘𝐹)
− 1))) |
| 46 | | resima2 6034 |
. . . . . . . 8
⊢ ({0}
⊆ (0...((♯‘𝐹) − 1)) → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0}) =
(𝑃 “
{0})) |
| 47 | | sseq1 4009 |
. . . . . . . 8
⊢ (((𝑃 ↾
(0...((♯‘𝐹)
− 1))) “ {0}) = (𝑃 “ {0}) → (((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0})
⊆ (𝑃 “ {0,
(♯‘𝐹)}) ↔
(𝑃 “ {0}) ⊆
(𝑃 “ {0,
(♯‘𝐹)}))) |
| 48 | 45, 46, 47 | 3syl 18 |
. . . . . . 7
⊢
(((♯‘𝐹)
− 1) ∈ ℕ0 → (((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0})
⊆ (𝑃 “ {0,
(♯‘𝐹)}) ↔
(𝑃 “ {0}) ⊆
(𝑃 “ {0,
(♯‘𝐹)}))) |
| 49 | 43, 48 | mpbiri 258 |
. . . . . 6
⊢
(((♯‘𝐹)
− 1) ∈ ℕ0 → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0})
⊆ (𝑃 “ {0,
(♯‘𝐹)})) |
| 50 | | resima2 6034 |
. . . . . . . . . 10
⊢
((1...((♯‘𝐹) − 1)) ⊆
(0...((♯‘𝐹)
− 1)) → ((𝑃
↾ (0...((♯‘𝐹) − 1))) “
(1...((♯‘𝐹)
− 1))) = (𝑃 “
(1...((♯‘𝐹)
− 1)))) |
| 51 | 22, 50 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑃 ↾
(0...((♯‘𝐹)
− 1))) “ (1...((♯‘𝐹) − 1))) = (𝑃 “ (1...((♯‘𝐹) − 1))) |
| 52 | 30 | imaeq2d 6078 |
. . . . . . . . 9
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 “ (1..^(♯‘𝐹))) = (𝑃 “ (1...((♯‘𝐹) − 1)))) |
| 53 | 51, 52 | eqtr4id 2796 |
. . . . . . . 8
⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “
(1...((♯‘𝐹)
− 1))) = (𝑃 “
(1..^(♯‘𝐹)))) |
| 54 | 53 | ineq2d 4220 |
. . . . . . 7
⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 “ {0, (♯‘𝐹)}) ∩ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “
(1...((♯‘𝐹)
− 1)))) = ((𝑃 “
{0, (♯‘𝐹)})
∩ (𝑃 “
(1..^(♯‘𝐹))))) |
| 55 | 25 | simp3bi 1148 |
. . . . . . 7
⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅) |
| 56 | 54, 55 | eqtrd 2777 |
. . . . . 6
⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 “ {0, (♯‘𝐹)}) ∩ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “
(1...((♯‘𝐹)
− 1)))) = ∅) |
| 57 | | ssdisj 4460 |
. . . . . 6
⊢ ((((𝑃 ↾
(0...((♯‘𝐹)
− 1))) “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)}) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “
(1...((♯‘𝐹)
− 1)))) = ∅) → (((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0})
∩ ((𝑃 ↾
(0...((♯‘𝐹)
− 1))) “ (1...((♯‘𝐹) − 1)))) = ∅) |
| 58 | 49, 56, 57 | syl2anr 597 |
. . . . 5
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ0)
→ (((𝑃 ↾
(0...((♯‘𝐹)
− 1))) “ {0}) ∩ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “
(1...((♯‘𝐹)
− 1)))) = ∅) |
| 59 | 16, 21, 40, 58 | f1resfz0f1d 35119 |
. . . 4
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ0)
→ (𝑃 ↾
(0...((♯‘𝐹)
− 1))):(0...((♯‘𝐹) − 1))–1-1→𝑉) |
| 60 | 9 | fvexi 6920 |
. . . . 5
⊢ 𝑉 ∈ V |
| 61 | | hashf1dmcdm 14483 |
. . . . 5
⊢ (((𝑃 ↾
(0...((♯‘𝐹)
− 1))) ∈ Fin ∧ 𝑉 ∈ V ∧ (𝑃 ↾ (0...((♯‘𝐹) −
1))):(0...((♯‘𝐹) − 1))–1-1→𝑉) →
(♯‘(0...((♯‘𝐹) − 1))) ≤ (♯‘𝑉)) |
| 62 | 60, 61 | mp3an2 1451 |
. . . 4
⊢ (((𝑃 ↾
(0...((♯‘𝐹)
− 1))) ∈ Fin ∧ (𝑃 ↾ (0...((♯‘𝐹) −
1))):(0...((♯‘𝐹) − 1))–1-1→𝑉) →
(♯‘(0...((♯‘𝐹) − 1))) ≤ (♯‘𝑉)) |
| 63 | 15, 59, 62 | syl2an2r 685 |
. . 3
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ0)
→ (♯‘(0...((♯‘𝐹) − 1))) ≤ (♯‘𝑉)) |
| 64 | 8, 63 | eqbrtrrd 5167 |
. 2
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ0)
→ (♯‘𝐹)
≤ (♯‘𝑉)) |
| 65 | | 0nn0m1nnn0 35118 |
. . . . 5
⊢
((♯‘𝐹) =
0 ↔ ((♯‘𝐹)
∈ ℕ0 ∧ ¬ ((♯‘𝐹) − 1) ∈
ℕ0)) |
| 66 | 65 | biimpri 228 |
. . . 4
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ ¬ ((♯‘𝐹) − 1) ∈ ℕ0)
→ (♯‘𝐹) =
0) |
| 67 | 4, 66 | sylan 580 |
. . 3
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ¬ ((♯‘𝐹) − 1) ∈
ℕ0) → (♯‘𝐹) = 0) |
| 68 | | hashge0 14426 |
. . . 4
⊢ (𝑉 ∈ V → 0 ≤
(♯‘𝑉)) |
| 69 | 60, 68 | ax-mp 5 |
. . 3
⊢ 0 ≤
(♯‘𝑉) |
| 70 | 67, 69 | eqbrtrdi 5182 |
. 2
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ¬ ((♯‘𝐹) − 1) ∈
ℕ0) → (♯‘𝐹) ≤ (♯‘𝑉)) |
| 71 | 64, 70 | pm2.61dan 813 |
1
⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ≤ (♯‘𝑉)) |