Theorem eupth2lem3lem1

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