This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → F Trails ⁡ G P
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 ⊢ φ → F Trails ⁡ G P
7 trliswlk ⊢ F Trails ⁡ G P → F Walks ⁡ G P
8 1 wlkpvtx ⊢ F Walks ⁡ G P → N ∈ 0 … F → P ⁡ N ∈ V
9 elfzofz ⊢ N ∈ 0 ..^ F → N ∈ 0 … F
10 8 9 impel ⊢ F Walks ⁡ G P ∧ N ∈ 0 ..^ F → P ⁡ N ∈ V
11 1 wlkpvtx ⊢ F Walks ⁡ G P → N + 1 ∈ 0 … F → P ⁡ N + 1 ∈ V
12 fzofzp1 ⊢ N ∈ 0 ..^ F → N + 1 ∈ 0 … F
13 11 12 impel ⊢ F Walks ⁡ G P ∧ N ∈ 0 ..^ F → P ⁡ N + 1 ∈ V
14 10 13 jca ⊢ F Walks ⁡ G P ∧ N ∈ 0 ..^ F → P ⁡ N ∈ V ∧ P ⁡ N + 1 ∈ V
15 14 ex ⊢ F Walks ⁡ G P → 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