Theorem trlsegvdeglem3

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	trlsegvdeglem3	⊢ ( 𝜑 → 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		fvex	⊢ ( 𝐹 ‘ 𝑁 ) ∈ V
14		fvex	⊢ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ V
15	13 14	pm3.2i	⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ V ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ V )
16		funsng	⊢ ( ( ( 𝐹 ‘ 𝑁 ) ∈ V ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ V ) → Fun { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
17	15 16	mp1i	⊢ ( 𝜑 → Fun { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
18	11	funeqd	⊢ ( 𝜑 → ( Fun ( iEdg ‘ 𝑌 ) ↔ Fun { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ) )
19	17 18	mpbird	⊢ ( 𝜑 → Fun ( iEdg ‘ 𝑌 ) )