Theorem trlsegvdeglem5

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	trlsegvdeglem5	|- ( ph -> dom ( iEdg ` Y ) = { ( F ` N ) } )

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	11	dmeqd	|- ( ph -> dom ( iEdg ` Y ) = dom { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
14		fvex	|- ( I ` ( F ` N ) ) e. _V
15		dmsnopg	|- ( ( I ` ( F ` N ) ) e. _V -> dom { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } = { ( F ` N ) } )
16	14 15	mp1i	|- ( ph -> dom { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } = { ( F ` N ) } )
17	13 16	eqtrd	|- ( ph -> dom ( iEdg ` Y ) = { ( F ` N ) } )