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

Metamath Proof Explorer

Theorem trlsegvdeglem6

Description: Lemma for trlsegvdeg . (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 trlsegvdeglem6 ⊢ φ → dom ⁡ iEdg ⁡ X ∈ Fin

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 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem4 ⊢ φ → dom ⁡ iEdg ⁡ X = F 0 ..^ N ∩ dom ⁡ I
14 2 trlf1 ⊢ F Trails ⁡ G P → F : 0 ..^ F ⟶ 1-1 dom ⁡ I
15 f1fun ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ I → Fun ⁡ F
16 6 14 15 3syl ⊢ φ → Fun ⁡ F
17 fzofi ⊢ 0 ..^ N ∈ Fin
18 imafi ⊢ Fun ⁡ F ∧ 0 ..^ N ∈ Fin → F 0 ..^ N ∈ Fin
19 16 17 18 sylancl ⊢ φ → F 0 ..^ N ∈ Fin
20 infi ⊢ F 0 ..^ N ∈ Fin → F 0 ..^ N ∩ dom ⁡ I ∈ Fin
21 19 20 syl ⊢ φ → F 0 ..^ N ∩ dom ⁡ I ∈ Fin
22 13 21 eqeltrd ⊢ φ → dom ⁡ iEdg ⁡ X ∈ Fin