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
|- ( 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 eupth2lem3lem2
|- ( ph -> ( ( VtxDeg ` Y ) ` U ) e. NN0 )

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 5 8 eleqtrrd
 |-  ( ph -> U e. ( Vtx ` Y ) )
14 13 elfvexd
 |-  ( ph -> Y e. _V )
15 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem7
 |-  ( ph -> dom ( iEdg ` Y ) e. 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 e. _V /\ dom ( iEdg ` Y ) e. Fin ) -> ( VtxDeg ` Y ) : ( Vtx ` Y ) --> NN0 )
20 14 15 19 syl2anc
 |-  ( ph -> ( VtxDeg ` Y ) : ( Vtx ` Y ) --> NN0 )
21 20 13 ffvelrnd
 |-  ( ph -> ( ( VtxDeg ` Y ) ` U ) e. NN0 )