Theorem eupth2

Description: The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (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	eupth2	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(\left|F\right|\right),\varnothing ,\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}\right)$$

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		eqid	$$⊢⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩=⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩$$
7	1 2 3 4 5 6	eupthvdres	$$⊢\phi \to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)=\mathrm{VtxDeg}\left(G\right)$$
8	7	fveq1d	$$⊢\phi \to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)=\mathrm{VtxDeg}\left(G\right)\left(x\right)$$
9	8	breq2d	$$⊢\phi \to \left(2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\leftrightarrow 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right)$$
10	9	notbid	$$⊢\phi \to \left(\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\leftrightarrow \neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right)$$
11	10	rabbidv	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right\}=\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}$$
12		eupthiswlk	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
13		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
14	5 12 13	3syl	$$⊢\phi \to \left|F\right|\in {\mathbb{N}}_0$$
15		nn0re	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \left|F\right|\in ℝ$$
16	15	leidd	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \left|F\right|\le \left|F\right|$$
17		breq1	$$⊢m=0\to \left(m\le \left|F\right|\leftrightarrow 0\le \left|F\right|\right)$$
18		oveq2	$$⊢m=0\to \left(0..^m\right)=\left(0..^0\right)$$
19	18	imaeq2d	$$⊢m=0\to F\left[\left(0..^m\right)\right]=F\left[\left(0..^0\right)\right]$$
20	19	reseq2d	$$⊢m=0\to {I\upharpoonright }_{F\left[\left(0..^m\right)\right]}={I\upharpoonright }_{F\left[\left(0..^0\right)\right]}$$
21	20	opeq2d	$$⊢m=0\to ⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩=⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩$$
22	21	fveq2d	$$⊢m=0\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)=\mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)$$
23	22	fveq1d	$$⊢m=0\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)=\mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)$$
24	23	breq2d	$$⊢m=0\to \left(2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\leftrightarrow 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)\right)$$
25	24	notbid	$$⊢m=0\to \left(\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\leftrightarrow \neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^0\right)\right]}⟩\right)\left(x\right)\right)$$
26	25	rabbidv	$$⊢m=0\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=\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\}$$
27		fveq2	$$⊢m=0\to P\left(m\right)=P\left(0\right)$$
28	27	eqeq2d	$$⊢m=0\to \left(P\left(0\right)=P\left(m\right)\leftrightarrow P\left(0\right)=P\left(0\right)\right)$$
29	27	preq2d	$$⊢m=0\to \left\{P\left(0\right),P\left(m\right)\right\}=\left\{P\left(0\right),P\left(0\right)\right\}$$
30	28 29	ifbieq2d	$$⊢m=0\to if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)=if\left(P\left(0\right)=P\left(0\right),\varnothing ,\left\{P\left(0\right),P\left(0\right)\right\}\right)$$
31	26 30	eqeq12d	$$⊢m=0\to \left(\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\leftrightarrow \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\}=if\left(P\left(0\right)=P\left(0\right),\varnothing ,\left\{P\left(0\right),P\left(0\right)\right\}\right)\right)$$
32	17 31	imbi12d	$$⊢m=0\to \left(\left(m\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\right)\leftrightarrow \left(0\le \left|F\right|\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\}=if\left(P\left(0\right)=P\left(0\right),\varnothing ,\left\{P\left(0\right),P\left(0\right)\right\}\right)\right)\right)$$
33	32	imbi2d	$$⊢m=0\to \left(\left(\phi \to \left(m\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\right)\right)\leftrightarrow \left(\phi \to \left(0\le \left|F\right|\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\}=if\left(P\left(0\right)=P\left(0\right),\varnothing ,\left\{P\left(0\right),P\left(0\right)\right\}\right)\right)\right)\right)$$
34		breq1	$$⊢m=n\to \left(m\le \left|F\right|\leftrightarrow n\le \left|F\right|\right)$$
35		oveq2	$$⊢m=n\to \left(0..^m\right)=\left(0..^n\right)$$
36	35	imaeq2d	$$⊢m=n\to F\left[\left(0..^m\right)\right]=F\left[\left(0..^n\right)\right]$$
37	36	reseq2d	$$⊢m=n\to {I\upharpoonright }_{F\left[\left(0..^m\right)\right]}={I\upharpoonright }_{F\left[\left(0..^n\right)\right]}$$
38	37	opeq2d	$$⊢m=n\to ⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩=⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩$$
39	38	fveq2d	$$⊢m=n\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)=\mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\right)$$
40	39	fveq1d	$$⊢m=n\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)=\mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\right)\left(x\right)$$
41	40	breq2d	$$⊢m=n\to \left(2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\leftrightarrow 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\right)\left(x\right)\right)$$
42	41	notbid	$$⊢m=n\to \left(\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\leftrightarrow \neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\right)\left(x\right)\right)$$
43	42	rabbidv	$$⊢m=n\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\right)\left(x\right)\right\}$$
44		fveq2	$$⊢m=n\to P\left(m\right)=P\left(n\right)$$
45	44	eqeq2d	$$⊢m=n\to \left(P\left(0\right)=P\left(m\right)\leftrightarrow P\left(0\right)=P\left(n\right)\right)$$
46	44	preq2d	$$⊢m=n\to \left\{P\left(0\right),P\left(m\right)\right\}=\left\{P\left(0\right),P\left(n\right)\right\}$$
47	45 46	ifbieq2d	$$⊢m=n\to if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)=if\left(P\left(0\right)=P\left(n\right),\varnothing ,\left\{P\left(0\right),P\left(n\right)\right\}\right)$$
48	43 47	eqeq12d	$$⊢m=n\to \left(\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\leftrightarrow \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\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)\right)$$
49	34 48	imbi12d	$$⊢m=n\to \left(\left(m\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\right)\leftrightarrow \left(n\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\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)\right)\right)$$
50	49	imbi2d	$$⊢m=n\to \left(\left(\phi \to \left(m\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\right)\right)\leftrightarrow \left(\phi \to \left(n\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\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)\right)\right)\right)$$
51		breq1	$$⊢m=n+1\to \left(m\le \left|F\right|\leftrightarrow n+1\le \left|F\right|\right)$$
52		oveq2	$$⊢m=n+1\to \left(0..^m\right)=\left(0..^n+1\right)$$
53	52	imaeq2d	$$⊢m=n+1\to F\left[\left(0..^m\right)\right]=F\left[\left(0..^n+1\right)\right]$$
54	53	reseq2d	$$⊢m=n+1\to {I\upharpoonright }_{F\left[\left(0..^m\right)\right]}={I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}$$
55	54	opeq2d	$$⊢m=n+1\to ⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩=⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩$$
56	55	fveq2d	$$⊢m=n+1\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)=\mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)$$
57	56	fveq1d	$$⊢m=n+1\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)=\mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)$$
58	57	breq2d	$$⊢m=n+1\to \left(2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\leftrightarrow 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)\right)$$
59	58	notbid	$$⊢m=n+1\to \left(\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\leftrightarrow \neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)\right)$$
60	59	rabbidv	$$⊢m=n+1\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)\right\}$$
61		fveq2	$$⊢m=n+1\to P\left(m\right)=P\left(n+1\right)$$
62	61	eqeq2d	$$⊢m=n+1\to \left(P\left(0\right)=P\left(m\right)\leftrightarrow P\left(0\right)=P\left(n+1\right)\right)$$
63	61	preq2d	$$⊢m=n+1\to \left\{P\left(0\right),P\left(m\right)\right\}=\left\{P\left(0\right),P\left(n+1\right)\right\}$$
64	62 63	ifbieq2d	$$⊢m=n+1\to if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)=if\left(P\left(0\right)=P\left(n+1\right),\varnothing ,\left\{P\left(0\right),P\left(n+1\right)\right\}\right)$$
65	60 64	eqeq12d	$$⊢m=n+1\to \left(\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\leftrightarrow \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(n+1\right),\varnothing ,\left\{P\left(0\right),P\left(n+1\right)\right\}\right)\right)$$
66	51 65	imbi12d	$$⊢m=n+1\to \left(\left(m\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\right)\leftrightarrow \left(n+1\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(n+1\right),\varnothing ,\left\{P\left(0\right),P\left(n+1\right)\right\}\right)\right)\right)$$
67	66	imbi2d	$$⊢m=n+1\to \left(\left(\phi \to \left(m\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\right)\right)\leftrightarrow \left(\phi \to \left(n+1\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(n+1\right),\varnothing ,\left\{P\left(0\right),P\left(n+1\right)\right\}\right)\right)\right)\right)$$
68		breq1	$$⊢m=\left|F\right|\to \left(m\le \left|F\right|\leftrightarrow \left|F\right|\le \left|F\right|\right)$$
69		oveq2	$$⊢m=\left|F\right|\to \left(0..^m\right)=\left(0..^\left|F\right|\right)$$
70	69	imaeq2d	$$⊢m=\left|F\right|\to F\left[\left(0..^m\right)\right]=F\left[\left(0..^\left|F\right|\right)\right]$$
71	70	reseq2d	$$⊢m=\left|F\right|\to {I\upharpoonright }_{F\left[\left(0..^m\right)\right]}={I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}$$
72	71	opeq2d	$$⊢m=\left|F\right|\to ⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩=⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩$$
73	72	fveq2d	$$⊢m=\left|F\right|\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)=\mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)$$
74	73	fveq1d	$$⊢m=\left|F\right|\to \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)=\mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)$$
75	74	breq2d	$$⊢m=\left|F\right|\to \left(2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\leftrightarrow 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right)$$
76	75	notbid	$$⊢m=\left|F\right|\to \left(\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\leftrightarrow \neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right)$$
77	76	rabbidv	$$⊢m=\left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right\}$$
78		fveq2	$$⊢m=\left|F\right|\to P\left(m\right)=P\left(\left|F\right|\right)$$
79	78	eqeq2d	$$⊢m=\left|F\right|\to \left(P\left(0\right)=P\left(m\right)\leftrightarrow P\left(0\right)=P\left(\left|F\right|\right)\right)$$
80	78	preq2d	$$⊢m=\left|F\right|\to \left\{P\left(0\right),P\left(m\right)\right\}=\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}$$
81	79 80	ifbieq2d	$$⊢m=\left|F\right|\to if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)=if\left(P\left(0\right)=P\left(\left|F\right|\right),\varnothing ,\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}\right)$$
82	77 81	eqeq12d	$$⊢m=\left|F\right|\to \left(\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\leftrightarrow \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(\left|F\right|\right),\varnothing ,\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}\right)\right)$$
83	68 82	imbi12d	$$⊢m=\left|F\right|\to \left(\left(m\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\right)\leftrightarrow \left(\left|F\right|\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(\left|F\right|\right),\varnothing ,\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}\right)\right)\right)$$
84	83	imbi2d	$$⊢m=\left|F\right|\to \left(\left(\phi \to \left(m\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^m\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(m\right),\varnothing ,\left\{P\left(0\right),P\left(m\right)\right\}\right)\right)\right)\leftrightarrow \left(\phi \to \left(\left|F\right|\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(\left|F\right|\right),\varnothing ,\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}\right)\right)\right)\right)$$
85	1 2 3 4 5	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$$
86		eqid	$$⊢P\left(0\right)=P\left(0\right)$$
87	86	iftruei	$$⊢if\left(P\left(0\right)=P\left(0\right),\varnothing ,\left\{P\left(0\right),P\left(0\right)\right\}\right)=\varnothing$$
88	85 87	eqtr4di	$$⊢\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\}=if\left(P\left(0\right)=P\left(0\right),\varnothing ,\left\{P\left(0\right),P\left(0\right)\right\}\right)$$
89	88	a1d	$$⊢\phi \to \left(0\le \left|F\right|\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\}=if\left(P\left(0\right)=P\left(0\right),\varnothing ,\left\{P\left(0\right),P\left(0\right)\right\}\right)\right)$$
90	1 2 3 4 5	eupth2lems	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(\left(n\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\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)\right)\to \left(n+1\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(n+1\right),\varnothing ,\left\{P\left(0\right),P\left(n+1\right)\right\}\right)\right)\right)$$
91	90	expcom	$$⊢n\in {\mathbb{N}}_0\to \left(\phi \to \left(\left(n\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\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)\right)\to \left(n+1\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(n+1\right),\varnothing ,\left\{P\left(0\right),P\left(n+1\right)\right\}\right)\right)\right)\right)$$
92	91	a2d	$$⊢n\in {\mathbb{N}}_0\to \left(\left(\phi \to \left(n\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n\right)\right]}⟩\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)\right)\right)\to \left(\phi \to \left(n+1\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^n+1\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(n+1\right),\varnothing ,\left\{P\left(0\right),P\left(n+1\right)\right\}\right)\right)\right)\right)$$
93	33 50 67 84 89 92	nn0ind	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \left(\phi \to \left(\left|F\right|\le \left|F\right|\to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(\left|F\right|\right),\varnothing ,\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}\right)\right)\right)$$
94	16 93	mpid	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \left(\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(\left|F\right|\right),\varnothing ,\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}\right)\right)$$
95	14 94	mpcom	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(\left|F\right|\right),\varnothing ,\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}\right)$$
96	11 95	eqtr3d	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(\left|F\right|\right),\varnothing ,\left\{P\left(0\right),P\left(\left|F\right|\right)\right\}\right)$$