Metamath Proof Explorer

Theorem trlsegvdeglem1

Description: Lemma for trlsegvdeg . (Contributed by AV, 20-Feb-2021)

Ref Expression
Hypotheses trlsegvdeg.v ⊢V=Vtx⁡G
trlsegvdeg.i ⊢I=iEdg⁡G
trlsegvdeg.f ⊢φ→Fun⁡I
trlsegvdeg.n ⊢φ→N∈0..^F
trlsegvdeg.u ⊢φ→U∈V
trlsegvdeg.w ⊢φ→FTrails⁡GP
Assertion trlsegvdeglem1 ⊢φ→P⁡N∈V∧P⁡N+1∈V

Proof

Step Hyp Ref Expression
1 trlsegvdeg.v ⊢V=Vtx⁡G
2 trlsegvdeg.i ⊢I=iEdg⁡G
3 trlsegvdeg.f ⊢φ→Fun⁡I
4 trlsegvdeg.n ⊢φ→N∈0..^F
5 trlsegvdeg.u ⊢φ→U∈V
6 trlsegvdeg.w ⊢φ→FTrails⁡GP
7 trliswlk ⊢FTrails⁡GP→FWalks⁡GP
8 1 wlkpvtx ⊢FWalks⁡GP→N∈0…F→P⁡N∈V
9 elfzofz ⊢N∈0..^F→N∈0…F
10 8 9 impel ⊢FWalks⁡GP∧N∈0..^F→P⁡N∈V
11 1 wlkpvtx ⊢FWalks⁡GP→N+1∈0…F→P⁡N+1∈V
12 fzofzp1 ⊢N∈0..^F→N+1∈0…F
13 11 12 impel ⊢FWalks⁡GP∧N∈0..^F→P⁡N+1∈V
14 10 13 jca ⊢FWalks⁡GP∧N∈0..^F→P⁡N∈V∧P⁡N+1∈V
15 14 ex ⊢FWalks⁡GP→N∈0..^F→P⁡N∈V∧P⁡N+1∈V
16 6 7 15 3syl ⊢φ→N∈0..^F→P⁡N∈V∧P⁡N+1∈V
17 4 16 mpd ⊢φ→P⁡N∈V∧P⁡N+1∈V