Theorem trlsegvdeglem7

Description: Lemma for trlsegvdeg . (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	trlsegvdeglem7	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(Y\right)\in \mathrm{Fin}$$

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	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem5	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(Y\right)=\left\{F\left(N\right)\right\}$$
14		snfi	$$⊢\left\{F\left(N\right)\right\}\in \mathrm{Fin}$$
15	13 14	eqeltrdi	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(Y\right)\in \mathrm{Fin}$$