| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 2 | 1 | wlkonprop 29676 | . . 3
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) | 
| 3 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) | 
| 4 |  | fv0p1e1 12389 | . . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) | 
| 5 | 3, 4 | preq12d 4741 | . . . . . . . . . 10
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) | 
| 6 | 5 | sseq1d 4015 | . . . . . . . . 9
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒 ↔ {(𝑃‘0), (𝑃‘1)} ⊆ 𝑒)) | 
| 7 | 6 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑘 = 0 → (∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒)) | 
| 8 |  | wlkonl1iedg.i | . . . . . . . . . . 11
⊢ 𝐼 = (iEdg‘𝐺) | 
| 9 | 8 | wlkvtxiedg 29643 | . . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) | 
| 10 | 9 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) | 
| 11 | 10 | adantr 480 | . . . . . . . 8
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) | 
| 12 |  | wlkcl 29633 | . . . . . . . . . . 11
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) | 
| 13 |  | elnnne0 12540 | . . . . . . . . . . . . 13
⊢
((♯‘𝐹)
∈ ℕ ↔ ((♯‘𝐹) ∈ ℕ0 ∧
(♯‘𝐹) ≠
0)) | 
| 14 | 13 | simplbi2 500 | . . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ≠ 0 → (♯‘𝐹) ∈
ℕ)) | 
| 15 |  | lbfzo0 13739 | . . . . . . . . . . . 12
⊢ (0 ∈
(0..^(♯‘𝐹))
↔ (♯‘𝐹)
∈ ℕ) | 
| 16 | 14, 15 | imbitrrdi 252 | . . . . . . . . . . 11
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ≠ 0 → 0 ∈
(0..^(♯‘𝐹)))) | 
| 17 | 12, 16 | syl 17 | . . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → ((♯‘𝐹) ≠ 0 → 0 ∈
(0..^(♯‘𝐹)))) | 
| 18 | 17 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((♯‘𝐹) ≠ 0 → 0 ∈
(0..^(♯‘𝐹)))) | 
| 19 | 18 | imp 406 | . . . . . . . 8
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → 0 ∈
(0..^(♯‘𝐹))) | 
| 20 | 7, 11, 19 | rspcdva 3623 | . . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒) | 
| 21 |  | fvex 6919 | . . . . . . . . . . 11
⊢ (𝑃‘0) ∈
V | 
| 22 |  | fvex 6919 | . . . . . . . . . . 11
⊢ (𝑃‘1) ∈
V | 
| 23 | 21, 22 | prss 4820 | . . . . . . . . . 10
⊢ (((𝑃‘0) ∈ 𝑒 ∧ (𝑃‘1) ∈ 𝑒) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ 𝑒) | 
| 24 |  | eleq1 2829 | . . . . . . . . . . . . 13
⊢ ((𝑃‘0) = 𝐴 → ((𝑃‘0) ∈ 𝑒 ↔ 𝐴 ∈ 𝑒)) | 
| 25 |  | ax-1 6 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒)) | 
| 26 | 24, 25 | biimtrdi 253 | . . . . . . . . . . . 12
⊢ ((𝑃‘0) = 𝐴 → ((𝑃‘0) ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒))) | 
| 27 | 26 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ((𝑃‘0) ∈ 𝑒 → ((𝑃‘1) ∈ 𝑒 → 𝐴 ∈ 𝑒))) | 
| 28 | 27 | impd 410 | . . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → (((𝑃‘0) ∈ 𝑒 ∧ (𝑃‘1) ∈ 𝑒) → 𝐴 ∈ 𝑒)) | 
| 29 | 23, 28 | biimtrrid 243 | . . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → ({(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → 𝐴 ∈ 𝑒)) | 
| 30 | 29 | reximdv 3170 | . . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) → (∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) | 
| 31 | 30 | adantr 480 | . . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → (∃𝑒 ∈ ran 𝐼{(𝑃‘0), (𝑃‘1)} ⊆ 𝑒 → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)) | 
| 32 | 20, 31 | mpd 15 | . . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴) ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒) | 
| 33 | 32 | ex 412 | . . . . 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 406 | 1
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒) |