| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2741 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 2 | 1 | wlkonprop 29747 |
. . 3
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) |
| 3 | | fveq2 6831 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
| 4 | | fv0p1e1 12294 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
| 5 | 3, 4 | preq12d 4676 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
| 6 | 5 | sseq1d 3948 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒 ↔ {(𝑃‘0), (𝑃‘1)} ⊆ 𝑒)) |
| 7 | 6 | rexbidv 3165 |
. . . . . . . 8
⊢ (𝑘 = 0 → (∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒)) |
| 8 | | wlkonl1iedg.i |
. . . . . . . . . . 11
⊢ 𝐼 = (iEdg‘𝐺) |
| 9 | 8 | wlkvtxiedg 29715 |
. . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) |
| 10 | 9 | adantr 482 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) |
| 11 | 10 | adantr 482 |
. . . . . . . 8
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) |
| 12 | | wlkcl 29706 |
. . . . . . . . . . 11
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
| 13 | | elnnne0 12446 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹)
∈ ℕ ↔ ((♯‘𝐹) ∈ ℕ0 ∧
(♯‘𝐹) ≠
0)) |
| 14 | 13 | simplbi2 502 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ≠ 0 → (♯‘𝐹) ∈
ℕ)) |
| 15 | | lbfzo0 13649 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^(♯‘𝐹))
↔ (♯‘𝐹)
∈ ℕ) |
| 16 | 14, 15 | imbitrrdi 254 |
. . . . . . . . . . 11
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ≠ 0 → 0 ∈
(0..^(♯‘𝐹)))) |
| 17 | 12, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → ((♯‘𝐹) ≠ 0 → 0 ∈
(0..^(♯‘𝐹)))) |
| 18 | 17 | adantr 482 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((♯‘𝐹) ≠ 0 → 0 ∈
(0..^(♯‘𝐹)))) |
| 19 | 18 | imp 408 |
. . . . . . . 8
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → 0 ∈
(0..^(♯‘𝐹))) |
| 20 | 7, 11, 19 | rspcdva 3563 |
. . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒) |
| 21 | | fvex 6844 |
. . . . . . . . . . 11
⊢ (𝑃‘0) ∈
V |
| 22 | | fvex 6844 |
. . . . . . . . . . 11
⊢ (𝑃‘1) ∈
V |
| 23 | 21, 22 | prss 4754 |
. . . . . . . . . 10
⊢ (((𝑃‘0) ∈ 𝑒 ∧ (𝑃‘1) ∈ 𝑒) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ 𝑒) |
| 24 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘0) = 𝐴 → ((𝑃‘0) ∈ 𝑒 ↔ 𝐴 ∈ 𝑒)) |
| 25 | | ax-1 6 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒)) |
| 26 | 24, 25 | biimtrdi 255 |
. . . . . . . . . . . 12
⊢ ((𝑃‘0) = 𝐴 → ((𝑃‘0) ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒))) |
| 27 | 26 | adantl 483 |
. . . . . . . . . . 11
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((𝑃‘0) ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒))) |
| 28 | 27 | impd 412 |
. . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → (((𝑃‘0) ∈ 𝑒 ∧ (𝑃‘1) ∈ 𝑒) → 𝐴 ∈ 𝑒)) |
| 29 | 23, 28 | biimtrrid 245 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ({(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → 𝐴 ∈ 𝑒)) |
| 30 | 29 | reximdv 3156 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → (∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
| 31 | 30 | adantr 482 |
. . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → (∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
| 32 | 20, 31 | mpd 15 |
. . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒) |
| 33 | 32 | ex 414 |
. . . . 5
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((♯‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
| 34 | 33 | 3adant3 1139 |
. . . 4
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵) → ((♯‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
| 35 | 34 | 3ad2ant3 1142 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)) → ((♯‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
| 36 | 2, 35 | syl 17 |
. 2
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((♯‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
| 37 | 36 | imp 408 |
1
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒) |