Theorem trlsegvdeglem3

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	trlsegvdeglem3	|- ( ph -> Fun ( iEdg ` Y ) )

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		fvex	|- ( F ` N ) e. _V
14		fvex	|- ( I ` ( F ` N ) ) e. _V
15	13 14	pm3.2i	|- ( ( F ` N ) e. _V /\ ( I ` ( F ` N ) ) e. _V )
16		funsng	|- ( ( ( F ` N ) e. _V /\ ( I ` ( F ` N ) ) e. _V ) -> Fun { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
17	15 16	mp1i	|- ( ph -> Fun { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
18	11	funeqd	|- ( ph -> ( Fun ( iEdg ` Y ) <-> Fun { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) )
19	17 18	mpbird	|- ( ph -> Fun ( iEdg ` Y ) )