Theorem trlsegvdeglem7

Description: Lemma for trlsegvdeg . (Contributed by AV, 21-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	trlsegvdeglem7	⊢ ( 𝜑 → dom ( iEdg ‘ 𝑌 ) ∈ Fin )

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	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem5	⊢ ( 𝜑 → dom ( iEdg ‘ 𝑌 ) = { ( 𝐹 ‘ 𝑁 ) } )
14		snfi	⊢ { ( 𝐹 ‘ 𝑁 ) } ∈ Fin
15	13 14	eqeltrdi	⊢ ( 𝜑 → dom ( iEdg ‘ 𝑌 ) ∈ Fin )