Theorem eupth2lem3lem2

Description: Lemma for eupth2lem3 . (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	eupth2lem3lem2	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝑌 ) ‘ 𝑈 ) ∈ ℕ0 )

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	5 8	eleqtrrd	⊢ ( 𝜑 → 𝑈 ∈ ( Vtx ‘ 𝑌 ) )
14	13	elfvexd	⊢ ( 𝜑 → 𝑌 ∈ V )
15	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem7	⊢ ( 𝜑 → dom ( iEdg ‘ 𝑌 ) ∈ Fin )
16		eqid	⊢ ( Vtx ‘ 𝑌 ) = ( Vtx ‘ 𝑌 )
17		eqid	⊢ ( iEdg ‘ 𝑌 ) = ( iEdg ‘ 𝑌 )
18		eqid	⊢ dom ( iEdg ‘ 𝑌 ) = dom ( iEdg ‘ 𝑌 )
19	16 17 18	vtxdgfisf	⊢ ( ( 𝑌 ∈ V ∧ dom ( iEdg ‘ 𝑌 ) ∈ Fin ) → ( VtxDeg ‘ 𝑌 ) : ( Vtx ‘ 𝑌 ) ⟶ ℕ0 )
20	14 15 19	syl2anc	⊢ ( 𝜑 → ( VtxDeg ‘ 𝑌 ) : ( Vtx ‘ 𝑌 ) ⟶ ℕ0 )
21	20 13	ffvelcdmd	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝑌 ) ‘ 𝑈 ) ∈ ℕ0 )