Theorem trlsegvdeglem6

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	trlsegvdeglem6	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(X\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	trlsegvdeglem4	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(X\right)=F\left[\left(0..^N\right)\right]\cap \mathrm{dom}I$$
14	2	trlf1	$$⊢F\mathrm{Trails}\left(G\right)P\to F:\left(0..^\left|F\right|\right)\underset{1-1}{⟶}\mathrm{dom}I$$
15		f1fun	$$⊢F:\left(0..^\left|F\right|\right)\underset{1-1}{⟶}\mathrm{dom}I\to \mathrm{Fun}F$$
16	6 14 15	3syl	$$⊢\phi \to \mathrm{Fun}F$$
17		fzofi	$$⊢\left(0..^N\right)\in \mathrm{Fin}$$
18		imafi	$$⊢\left(\mathrm{Fun}F\wedge \left(0..^N\right)\in \mathrm{Fin}\right)\to F\left[\left(0..^N\right)\right]\in \mathrm{Fin}$$
19	16 17 18	sylancl	$$⊢\phi \to F\left[\left(0..^N\right)\right]\in \mathrm{Fin}$$
20		infi	$$⊢F\left[\left(0..^N\right)\right]\in \mathrm{Fin}\to F\left[\left(0..^N\right)\right]\cap \mathrm{dom}I\in \mathrm{Fin}$$
21	19 20	syl	$$⊢\phi \to F\left[\left(0..^N\right)\right]\cap \mathrm{dom}I\in \mathrm{Fin}$$
22	13 21	eqeltrd	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(X\right)\in \mathrm{Fin}$$