Theorem eupth2lem3lem5

Description: Lemma for eupth2 . (Contributed by AV, 25-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]}$$
	eupth2lem3.o	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(X\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(N\right),\varnothing ,\left\{P\left(0\right),P\left(N\right)\right\}\right)$$
	eupth2lem3.e	$$⊢\phi \to I\left(F\left(N\right)\right)=\left\{P\left(N\right),P\left(N+1\right)\right\}$$
Assertion	eupth2lem3lem5	$$⊢\phi \to I\left(F\left(N\right)\right)\in 𝒫V$$

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		eupth2lem3.o	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(X\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(N\right),\varnothing ,\left\{P\left(0\right),P\left(N\right)\right\}\right)$$
14		eupth2lem3.e	$$⊢\phi \to I\left(F\left(N\right)\right)=\left\{P\left(N\right),P\left(N+1\right)\right\}$$
15	1 2 3 4 5 6	trlsegvdeglem1	$$⊢\phi \to \left(P\left(N\right)\in V\wedge P\left(N+1\right)\in V\right)$$
16		prelpwi	$$⊢\left(P\left(N\right)\in V\wedge P\left(N+1\right)\in V\right)\to \left\{P\left(N\right),P\left(N+1\right)\right\}\in 𝒫V$$
17	15 16	syl	$$⊢\phi \to \left\{P\left(N\right),P\left(N+1\right)\right\}\in 𝒫V$$
18	14 17	eqeltrd	$$⊢\phi \to I\left(F\left(N\right)\right)\in 𝒫V$$