Theorem trlsegvdeglem2

Description: Lemma for trlsegvdeg . (Contributed by AV, 20-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	trlsegvdeglem2	|- ( ph -> Fun ( iEdg ` X ) )

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	3	funresd	|- ( ph -> Fun ( I |` ( F " ( 0 ..^ N ) ) ) )
14	10	funeqd	|- ( ph -> ( Fun ( iEdg ` X ) <-> Fun ( I |` ( F " ( 0 ..^ N ) ) ) ) )
15	13 14	mpbird	|- ( ph -> Fun ( iEdg ` X ) )