Theorem eupth2lem3lem2

Description: Lemma for eupth2lem3 . (Contributed by AV, 21-Feb-2021)

	Ref	Expression
Hypotheses	trlsegvdeg.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	trlsegvdeg.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	trlsegvdeg.f	$$⊢\phi \to \mathrm{Fun}I$$
	trlsegvdeg.n	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
	trlsegvdeg.u	$$⊢\phi \to U\in V$$
	trlsegvdeg.w	$$⊢\phi \to F\mathrm{Trails}\left(G\right)P$$
	trlsegvdeg.vx	$$⊢\phi \to \mathrm{Vtx}\left(X\right)=V$$
	trlsegvdeg.vy	$$⊢\phi \to \mathrm{Vtx}\left(Y\right)=V$$
	trlsegvdeg.vz	$$⊢\phi \to \mathrm{Vtx}\left(Z\right)=V$$
	trlsegvdeg.ix	$$⊢\phi \to \mathrm{iEdg}\left(X\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
	trlsegvdeg.iy	$$⊢\phi \to \mathrm{iEdg}\left(Y\right)=\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$
	trlsegvdeg.iz	$$⊢\phi \to \mathrm{iEdg}\left(Z\right)={I\upharpoonright }_{F\left[\left(0\dots N\right)\right]}$$
Assertion	eupth2lem3lem2	$$⊢\phi \to \mathrm{VtxDeg}\left(Y\right)\left(U\right)\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		trlsegvdeg.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		trlsegvdeg.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		trlsegvdeg.f	$$⊢\phi \to \mathrm{Fun}I$$
4		trlsegvdeg.n	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
5		trlsegvdeg.u	$$⊢\phi \to U\in V$$
6		trlsegvdeg.w	$$⊢\phi \to F\mathrm{Trails}\left(G\right)P$$
7		trlsegvdeg.vx	$$⊢\phi \to \mathrm{Vtx}\left(X\right)=V$$
8		trlsegvdeg.vy	$$⊢\phi \to \mathrm{Vtx}\left(Y\right)=V$$
9		trlsegvdeg.vz	$$⊢\phi \to \mathrm{Vtx}\left(Z\right)=V$$
10		trlsegvdeg.ix	$$⊢\phi \to \mathrm{iEdg}\left(X\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
11		trlsegvdeg.iy	$$⊢\phi \to \mathrm{iEdg}\left(Y\right)=\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$
12		trlsegvdeg.iz	$$⊢\phi \to \mathrm{iEdg}\left(Z\right)={I\upharpoonright }_{F\left[\left(0\dots N\right)\right]}$$
13	5 8	eleqtrrd	$$⊢\phi \to U\in \mathrm{Vtx}\left(Y\right)$$
14	13	elfvexd	$$⊢\phi \to Y\in \mathrm{V}$$
15	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem7	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(Y\right)\in \mathrm{Fin}$$
16		eqid	$$⊢\mathrm{Vtx}\left(Y\right)=\mathrm{Vtx}\left(Y\right)$$
17		eqid	$$⊢\mathrm{iEdg}\left(Y\right)=\mathrm{iEdg}\left(Y\right)$$
18		eqid	$$⊢\mathrm{dom}\mathrm{iEdg}\left(Y\right)=\mathrm{dom}\mathrm{iEdg}\left(Y\right)$$
19	16 17 18	vtxdgfisf	$$⊢\left(Y\in \mathrm{V}\wedge \mathrm{dom}\mathrm{iEdg}\left(Y\right)\in \mathrm{Fin}\right)\to \mathrm{VtxDeg}\left(Y\right):\mathrm{Vtx}\left(Y\right)⟶{\mathbb{N}}_0$$
20	14 15 19	syl2anc	$$⊢\phi \to \mathrm{VtxDeg}\left(Y\right):\mathrm{Vtx}\left(Y\right)⟶{\mathbb{N}}_0$$
21	20 13	ffvelrnd	$$⊢\phi \to \mathrm{VtxDeg}\left(Y\right)\left(U\right)\in {\mathbb{N}}_0$$