Metamath Proof Explorer

Theorem wlkvtxiedg

Description: The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 2-Jan-2021) (Proof shortened by AV, 4-Apr-2021)

Ref Expression
Hypothesis wlkvtxeledg.i ⊢ I = iEdg ⁡ G
Assertion wlkvtxiedg ⊢ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F ∃ e ∈ ran ⁡ I P ⁡ k P ⁡ k + 1 ⊆ e

Proof

Step Hyp Ref Expression
1 wlkvtxeledg.i ⊢ I = iEdg ⁡ G
2 1 wlkvtxeledg ⊢ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
3 fvex ⊢ P ⁡ k ∈ V
4 3 prnz ⊢ P ⁡ k P ⁡ k + 1 ≠ ∅
5 ssn0 ⊢ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ∧ P ⁡ k P ⁡ k + 1 ≠ ∅ → I ⁡ F ⁡ k ≠ ∅
6 4 5 mpan2 ⊢ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → I ⁡ F ⁡ k ≠ ∅
7 6 adantl ⊢ F Walks ⁡ G P ∧ k ∈ 0 ..^ F ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → I ⁡ F ⁡ k ≠ ∅
8 fvn0fvelrn ⊢ I ⁡ F ⁡ k ≠ ∅ → I ⁡ F ⁡ k ∈ ran ⁡ I
9 7 8 syl ⊢ F Walks ⁡ G P ∧ k ∈ 0 ..^ F ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → I ⁡ F ⁡ k ∈ ran ⁡ I
10 sseq2 ⊢ e = I ⁡ F ⁡ k → P ⁡ k P ⁡ k + 1 ⊆ e ↔ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
11 10 adantl ⊢ F Walks ⁡ G P ∧ k ∈ 0 ..^ F ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ∧ e = I ⁡ F ⁡ k → P ⁡ k P ⁡ k + 1 ⊆ e ↔ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
12 simpr ⊢ F Walks ⁡ G P ∧ k ∈ 0 ..^ F ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
13 9 11 12 rspcedvd ⊢ F Walks ⁡ G P ∧ k ∈ 0 ..^ F ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∃ e ∈ ran ⁡ I P ⁡ k P ⁡ k + 1 ⊆ e
14 13 ex ⊢ F Walks ⁡ G P ∧ k ∈ 0 ..^ F → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∃ e ∈ ran ⁡ I P ⁡ k P ⁡ k + 1 ⊆ e
15 14 ralimdva ⊢ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F ∃ e ∈ ran ⁡ I P ⁡ k P ⁡ k + 1 ⊆ e
16 2 15 mpd ⊢ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F ∃ e ∈ ran ⁡ I P ⁡ k P ⁡ k + 1 ⊆ e