Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | 1 | wlkonprop 27600 |
. . 3
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) |
3 | | fveq2 6674 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
4 | | fv0p1e1 11839 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
5 | 3, 4 | preq12d 4632 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
6 | 5 | sseq1d 3908 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒 ↔ {(𝑃‘0), (𝑃‘1)} ⊆ 𝑒)) |
7 | 6 | rexbidv 3207 |
. . . . . . . 8
⊢ (𝑘 = 0 → (∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒)) |
8 | | wlkonl1iedg.i |
. . . . . . . . . . 11
⊢ 𝐼 = (iEdg‘𝐺) |
9 | 8 | wlkvtxiedg 27566 |
. . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) |
10 | 9 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) |
11 | 10 | adantr 484 |
. . . . . . . 8
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) |
12 | | wlkcl 27557 |
. . . . . . . . . . 11
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
13 | | elnnne0 11990 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹)
∈ ℕ ↔ ((♯‘𝐹) ∈ ℕ0 ∧
(♯‘𝐹) ≠
0)) |
14 | 13 | simplbi2 504 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ≠ 0 → (♯‘𝐹) ∈
ℕ)) |
15 | | lbfzo0 13168 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^(♯‘𝐹))
↔ (♯‘𝐹)
∈ ℕ) |
16 | 14, 15 | syl6ibr 255 |
. . . . . . . . . . 11
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ≠ 0 → 0 ∈
(0..^(♯‘𝐹)))) |
17 | 12, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → ((♯‘𝐹) ≠ 0 → 0 ∈
(0..^(♯‘𝐹)))) |
18 | 17 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((♯‘𝐹) ≠ 0 → 0 ∈
(0..^(♯‘𝐹)))) |
19 | 18 | imp 410 |
. . . . . . . 8
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → 0 ∈
(0..^(♯‘𝐹))) |
20 | 7, 11, 19 | rspcdva 3528 |
. . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒) |
21 | | fvex 6687 |
. . . . . . . . . . 11
⊢ (𝑃‘0) ∈
V |
22 | | fvex 6687 |
. . . . . . . . . . 11
⊢ (𝑃‘1) ∈
V |
23 | 21, 22 | prss 4708 |
. . . . . . . . . 10
⊢ (((𝑃‘0) ∈ 𝑒 ∧ (𝑃‘1) ∈ 𝑒) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ 𝑒) |
24 | | eleq1 2820 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘0) = 𝐴 → ((𝑃‘0) ∈ 𝑒 ↔ 𝐴 ∈ 𝑒)) |
25 | | ax-1 6 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒)) |
26 | 24, 25 | syl6bi 256 |
. . . . . . . . . . . 12
⊢ ((𝑃‘0) = 𝐴 → ((𝑃‘0) ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒))) |
27 | 26 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((𝑃‘0) ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒))) |
28 | 27 | impd 414 |
. . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → (((𝑃‘0) ∈ 𝑒 ∧ (𝑃‘1) ∈ 𝑒) → 𝐴 ∈ 𝑒)) |
29 | 23, 28 | syl5bir 246 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ({(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → 𝐴 ∈ 𝑒)) |
30 | 29 | reximdv 3183 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → (∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
31 | 30 | adantr 484 |
. . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → (∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
32 | 20, 31 | mpd 15 |
. . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒) |
33 | 32 | ex 416 |
. . . . 5
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((♯‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
34 | 33 | 3adant3 1133 |
. . . 4
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵) → ((♯‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
35 | 34 | 3ad2ant3 1136 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)) → ((♯‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
36 | 2, 35 | syl 17 |
. 2
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((♯‘𝐹) ≠ 0 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) |
37 | 36 | imp 410 |
1
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒) |