Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | 1 | wlkonprop 26554 |
. . 3
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
3 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
4 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
5 | | 0p1e1 11132 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
6 | 4, 5 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
7 | 6 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
8 | 3, 7 | preq12d 4276 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
9 | 8 | sseq1d 3632 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒 ↔ {(𝑃‘0), (𝑃‘1)} ⊆ 𝑒)) |
10 | 9 | rexbidv 3052 |
. . . . . . . 8
⊢ (𝑘 = 0 → (∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒)) |
11 | | wlkonl1iedg.i |
. . . . . . . . . . 11
⊢ 𝐼 = (iEdg‘𝐺) |
12 | 11 | wlkvtxiedg 26520 |
. . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(#‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) |
13 | 12 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ∀𝑘 ∈ (0..^(#‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) |
14 | 13 | adantr 481 |
. . . . . . . 8
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (#‘𝐹) ≠ 0) → ∀𝑘 ∈ (0..^(#‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) |
15 | | wlkcl 26511 |
. . . . . . . . . . 11
⊢ (𝐹(Walks‘𝐺)𝑃 → (#‘𝐹) ∈
ℕ0) |
16 | | elnnne0 11306 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) ∈
ℕ ↔ ((#‘𝐹)
∈ ℕ0 ∧ (#‘𝐹) ≠ 0)) |
17 | 16 | simplbi2 655 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) ≠ 0 → (#‘𝐹) ∈ ℕ)) |
18 | | lbfzo0 12507 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^(#‘𝐹)) ↔
(#‘𝐹) ∈
ℕ) |
19 | 17, 18 | syl6ibr 242 |
. . . . . . . . . . 11
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) ≠ 0 → 0 ∈ (0..^(#‘𝐹)))) |
20 | 15, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → ((#‘𝐹) ≠ 0 → 0 ∈ (0..^(#‘𝐹)))) |
21 | 20 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((#‘𝐹) ≠ 0 → 0 ∈ (0..^(#‘𝐹)))) |
22 | 21 | imp 445 |
. . . . . . . 8
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (#‘𝐹) ≠ 0) → 0 ∈
(0..^(#‘𝐹))) |
23 | 10, 14, 22 | rspcdva 3316 |
. . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (#‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒) |
24 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝑃‘0) ∈
V |
25 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝑃‘1) ∈
V |
26 | 24, 25 | prss 4351 |
. . . . . . . . . 10
⊢ (((𝑃‘0) ∈ 𝑒 ∧ (𝑃‘1) ∈ 𝑒) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ 𝑒) |
27 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘0) = 𝐴 → ((𝑃‘0) ∈ 𝑒 ↔ 𝐴 ∈ 𝑒)) |
28 | | ax-1 6 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒)) |
29 | 27, 28 | syl6bi 243 |
. . . . . . . . . . . 12
⊢ ((𝑃‘0) = 𝐴 → ((𝑃‘0) ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒))) |
30 | 29 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((𝑃‘0) ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒))) |
31 | 30 | impd 447 |
. . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → (((𝑃‘0) ∈ 𝑒 ∧ (𝑃‘1) ∈ 𝑒) → 𝐴 ∈ 𝑒)) |
32 | 26, 31 | syl5bir 233 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ({(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → 𝐴 ∈ 𝑒)) |
33 | 32 | reximdv 3016 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → (∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
34 | 33 | adantr 481 |
. . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (#‘𝐹) ≠ 0) → (∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
35 | 23, 34 | mpd 15 |
. . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (#‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒) |
36 | 35 | ex 450 |
. . . . 5
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((#‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
37 | 36 | 3adant3 1081 |
. . . 4
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((#‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
38 | 37 | 3ad2ant3 1084 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → ((#‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
39 | 2, 38 | syl 17 |
. 2
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((#‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
40 | 39 | imp 445 |
1
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ (#‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒) |