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

Metamath Proof Explorer

Theorem eupth2lem3lem2

Description: Lemma for eupth2lem3 . (Contributed by AV, 21-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
trlsegvdeg.vx ⊢ φ → Vtx ⁡ X = V
trlsegvdeg.vy ⊢ φ → Vtx ⁡ Y = V
trlsegvdeg.vz ⊢ φ → Vtx ⁡ Z = V
trlsegvdeg.ix ⊢ φ → iEdg ⁡ X = I ↾ F 0 ..^ N
trlsegvdeg.iy ⊢ φ → iEdg ⁡ Y = F ⁡ N I ⁡ F ⁡ N
trlsegvdeg.iz ⊢ φ → iEdg ⁡ Z = I ↾ F 0 … N
Assertion eupth2lem3lem2 ⊢ φ → VtxDeg ⁡ Y ⁡ U ∈ ℕ 0

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 trlsegvdeg.vx ⊢ φ → Vtx ⁡ X = V
8 trlsegvdeg.vy ⊢ φ → Vtx ⁡ Y = V
9 trlsegvdeg.vz ⊢ φ → Vtx ⁡ Z = V
10 trlsegvdeg.ix ⊢ φ → iEdg ⁡ X = I ↾ F 0 ..^ N
11 trlsegvdeg.iy ⊢ φ → iEdg ⁡ Y = F ⁡ N I ⁡ F ⁡ N
12 trlsegvdeg.iz ⊢ φ → iEdg ⁡ Z = I ↾ F 0 … N
13 5 8 eleqtrrd ⊢ φ → U ∈ Vtx ⁡ Y
14 13 elfvexd ⊢ φ → Y ∈ V
15 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem7 ⊢ φ → dom ⁡ iEdg ⁡ Y ∈ Fin
16 eqid ⊢ Vtx ⁡ Y = Vtx ⁡ Y
17 eqid ⊢ iEdg ⁡ Y = iEdg ⁡ Y
18 eqid ⊢ dom ⁡ iEdg ⁡ Y = dom ⁡ iEdg ⁡ Y
19 16 17 18 vtxdgfisf ⊢ Y ∈ V ∧ dom ⁡ iEdg ⁡ Y ∈ Fin → VtxDeg ⁡ Y : Vtx ⁡ Y ⟶ ℕ 0
20 14 15 19 syl2anc ⊢ φ → VtxDeg ⁡ Y : Vtx ⁡ Y ⟶ ℕ 0
21 20 13 ffvelcdmd ⊢ φ → VtxDeg ⁡ Y ⁡ U ∈ ℕ 0