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 ⊢FWalks⁡GP→∀k∈0..^F∃e∈ran⁡IP⁡kP⁡k+1⊆e

Proof

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