Theorem trlsegvdeglem3

Description: Lemma for trlsegvdeg . (Contributed by AV, 20-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	trlsegvdeglem3	$$⊢\phi \to \mathrm{Fun}\mathrm{iEdg}\left(Y\right)$$

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		fvex	$$⊢F\left(N\right)\in \mathrm{V}$$
14		fvex	$$⊢I\left(F\left(N\right)\right)\in \mathrm{V}$$
15	13 14	pm3.2i	$$⊢\left(F\left(N\right)\in \mathrm{V}\wedge I\left(F\left(N\right)\right)\in \mathrm{V}\right)$$
16		funsng	$$⊢\left(F\left(N\right)\in \mathrm{V}\wedge I\left(F\left(N\right)\right)\in \mathrm{V}\right)\to \mathrm{Fun}\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$
17	15 16	mp1i	$$⊢\phi \to \mathrm{Fun}\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$
18	11	funeqd	$$⊢\phi \to \left(\mathrm{Fun}\mathrm{iEdg}\left(Y\right)\leftrightarrow \mathrm{Fun}\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}\right)$$
19	17 18	mpbird	$$⊢\phi \to \mathrm{Fun}\mathrm{iEdg}\left(Y\right)$$