Theorem eupth2lemb

Description: Lemma for eupth2 (induction basis): There are no vertices of odd degree in an Eulerian path of length 0, having no edge and identical endpoints (the single vertex of the Eulerian path). Formerly part of proof for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

	Ref	Expression
Hypotheses	eupth2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	eupth2.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	eupth2.g	$$⊢\phi \to G\in \mathrm{UPGraph}$$
	eupth2.f	$$⊢\phi \to \mathrm{Fun}I$$
	eupth2.p	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
Assertion	eupth2lemb	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		eupth2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		eupth2.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		eupth2.g	$$⊢\phi \to G\in \mathrm{UPGraph}$$
4		eupth2.f	$$⊢\phi \to \mathrm{Fun}I$$
5		eupth2.p	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
6		z0even	$$⊢2\parallel 0$$
7	1	fvexi	$$⊢V\in \mathrm{V}$$
8	2	fvexi	$$⊢I\in \mathrm{V}$$
9	8	resex	$$⊢{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}\in \mathrm{V}$$
10	7 9	pm3.2i	$$⊢\left(V\in \mathrm{V}\wedge {I\upharpoonright }_{F\left[\left(0..^0\right)\right]}\in \mathrm{V}\right)$$
11		opvtxfv	$$⊢\left(V\in \mathrm{V}\wedge {I\upharpoonright }_{F\left[\left(0..^0\right)\right]}\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)=V$$
12	10 11	mp1i	$$⊢\phi \to \mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)=V$$
13	12	eqcomd	$$⊢\phi \to V=\mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)$$
14	13	eleq2d	$$⊢\phi \to \left(x\in V\leftrightarrow x\in \mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\right)$$
15	14	biimpa	$$⊢\left(\phi \wedge x\in V\right)\to x\in \mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)$$
16		opiedgfv	$$⊢\left(V\in \mathrm{V}\wedge {I\upharpoonright }_{F\left[\left(0..^0\right)\right]}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)={I\upharpoonright }_{F\left[\left(0..^0\right)\right]}$$
17	10 16	mp1i	$$⊢\phi \to \mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)={I\upharpoonright }_{F\left[\left(0..^0\right)\right]}$$
18		fzo0	$$⊢\left(0..^0\right)=\varnothing$$
19	18	imaeq2i	$$⊢F\left[\left(0..^0\right)\right]=F\left[\varnothing \right]$$
20		ima0	$$⊢F\left[\varnothing \right]=\varnothing$$
21	19 20	eqtri	$$⊢F\left[\left(0..^0\right)\right]=\varnothing$$
22	21	reseq2i	$$⊢{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}={I\upharpoonright }_{\varnothing }$$
23		res0	$$⊢{I\upharpoonright }_{\varnothing }=\varnothing$$
24	22 23	eqtri	$$⊢{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}=\varnothing$$
25	17 24	eqtrdi	$$⊢\phi \to \mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)=\varnothing$$
26	25	adantr	$$⊢\left(\phi \wedge x\in V\right)\to \mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)=\varnothing$$
27		eqid	$$⊢\mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)=\mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)$$
28		eqid	$$⊢\mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)=\mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)$$
29	27 28	vtxdg0e	$$⊢\left(x\in \mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\wedge \mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)=\varnothing \right)\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)=0$$
30	15 26 29	syl2anc	$$⊢\left(\phi \wedge x\in V\right)\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)=0$$
31	6 30	breqtrrid	$$⊢\left(\phi \wedge x\in V\right)\to 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)$$
32	31	notnotd	$$⊢\left(\phi \wedge x\in V\right)\to \neg \neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)$$
33	32	ralrimiva	$$⊢\phi \to \forall x\in V\neg \neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)$$
34		rabeq0	$$⊢\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)\right\}=\varnothing \leftrightarrow \forall x\in V\neg \neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)$$
35	33 34	sylibr	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)\right\}=\varnothing$$