Metamath Proof Explorer

Theorem wlkvtxedg

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

Ref Expression
Hypothesis wlkvtxedg.e ⊢ E = Edg ⁡ G
Assertion wlkvtxedg ⊢ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F ∃ e ∈ E P ⁡ k P ⁡ k + 1 ⊆ e

Proof

Step Hyp Ref Expression
1 wlkvtxedg.e ⊢ E = Edg ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 2 wlkvtxiedg ⊢ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F ∃ e ∈ ran ⁡ iEdg ⁡ G P ⁡ k P ⁡ k + 1 ⊆ e
4 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
5 1 4 eqtr2i ⊢ ran ⁡ iEdg ⁡ G = E
6 5 rexeqi ⊢ ∃ e ∈ ran ⁡ iEdg ⁡ G P ⁡ k P ⁡ k + 1 ⊆ e ↔ ∃ e ∈ E P ⁡ k P ⁡ k + 1 ⊆ e
7 6 ralbii ⊢ ∀ k ∈ 0 ..^ F ∃ e ∈ ran ⁡ iEdg ⁡ G P ⁡ k P ⁡ k + 1 ⊆ e ↔ ∀ k ∈ 0 ..^ F ∃ e ∈ E P ⁡ k P ⁡ k + 1 ⊆ e
8 3 7 sylib ⊢ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F ∃ e ∈ E P ⁡ k P ⁡ k + 1 ⊆ e