Metamath Proof Explorer


Theorem trlsegvdeglem7

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
|- ( ph -> Fun I )
trlsegvdeg.n
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
trlsegvdeg.u
|- ( ph -> U e. V )
trlsegvdeg.w
|- ( ph -> F ( Trails ` G ) P )
trlsegvdeg.vx
|- ( ph -> ( Vtx ` X ) = V )
trlsegvdeg.vy
|- ( ph -> ( Vtx ` Y ) = V )
trlsegvdeg.vz
|- ( ph -> ( Vtx ` Z ) = V )
trlsegvdeg.ix
|- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
trlsegvdeg.iy
|- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
trlsegvdeg.iz
|- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )
Assertion trlsegvdeglem7
|- ( ph -> dom ( iEdg ` Y ) e. Fin )

Proof

Step Hyp Ref Expression
1 trlsegvdeg.v
 |-  V = ( Vtx ` G )
2 trlsegvdeg.i
 |-  I = ( iEdg ` G )
3 trlsegvdeg.f
 |-  ( ph -> Fun I )
4 trlsegvdeg.n
 |-  ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5 trlsegvdeg.u
 |-  ( ph -> U e. V )
6 trlsegvdeg.w
 |-  ( ph -> F ( Trails ` G ) P )
7 trlsegvdeg.vx
 |-  ( ph -> ( Vtx ` X ) = V )
8 trlsegvdeg.vy
 |-  ( ph -> ( Vtx ` Y ) = V )
9 trlsegvdeg.vz
 |-  ( ph -> ( Vtx ` Z ) = V )
10 trlsegvdeg.ix
 |-  ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
11 trlsegvdeg.iy
 |-  ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
12 trlsegvdeg.iz
 |-  ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem5
 |-  ( ph -> dom ( iEdg ` Y ) = { ( F ` N ) } )
14 snfi
 |-  { ( F ` N ) } e. Fin
15 13 14 eqeltrdi
 |-  ( ph -> dom ( iEdg ` Y ) e. Fin )