Theorem trlsegvdeglem2

Description: Lemma for trlsegvdeg . (Contributed by AV, 20-Feb-2021)

	Ref	Expression
Hypotheses	trlsegvdeg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	trlsegvdeg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	trlsegvdeg.f	⊢ ( 𝜑 → Fun 𝐼 )
	trlsegvdeg.n	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
	trlsegvdeg.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	trlsegvdeg.w	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
	trlsegvdeg.vx	⊢ ( 𝜑 → ( Vtx ‘ 𝑋 ) = 𝑉 )
	trlsegvdeg.vy	⊢ ( 𝜑 → ( Vtx ‘ 𝑌 ) = 𝑉 )
	trlsegvdeg.vz	⊢ ( 𝜑 → ( Vtx ‘ 𝑍 ) = 𝑉 )
	trlsegvdeg.ix	⊢ ( 𝜑 → ( iEdg ‘ 𝑋 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
	trlsegvdeg.iy	⊢ ( 𝜑 → ( iEdg ‘ 𝑌 ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
	trlsegvdeg.iz	⊢ ( 𝜑 → ( iEdg ‘ 𝑍 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) )
Assertion	trlsegvdeglem2	⊢ ( 𝜑 → Fun ( iEdg ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		trlsegvdeg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		trlsegvdeg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		trlsegvdeg.f	⊢ ( 𝜑 → Fun 𝐼 )
4		trlsegvdeg.n	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5		trlsegvdeg.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6		trlsegvdeg.w	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
7		trlsegvdeg.vx	⊢ ( 𝜑 → ( Vtx ‘ 𝑋 ) = 𝑉 )
8		trlsegvdeg.vy	⊢ ( 𝜑 → ( Vtx ‘ 𝑌 ) = 𝑉 )
9		trlsegvdeg.vz	⊢ ( 𝜑 → ( Vtx ‘ 𝑍 ) = 𝑉 )
10		trlsegvdeg.ix	⊢ ( 𝜑 → ( iEdg ‘ 𝑋 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
11		trlsegvdeg.iy	⊢ ( 𝜑 → ( iEdg ‘ 𝑌 ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
12		trlsegvdeg.iz	⊢ ( 𝜑 → ( iEdg ‘ 𝑍 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) )
13	3	funresd	⊢ ( 𝜑 → Fun ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
14	10	funeqd	⊢ ( 𝜑 → ( Fun ( iEdg ‘ 𝑋 ) ↔ Fun ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ) )
15	13 14	mpbird	⊢ ( 𝜑 → Fun ( iEdg ‘ 𝑋 ) )