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 = Vtx (G)$
	eupth2.i	$⊢ I = iEdg (G)$
	eupth2.g	$⊢ φ \to G \in UPGraph$
	eupth2.f	$⊢ φ \to Fun I$
	eupth2.p	$⊢ φ \to F EulerPaths (G) P$
Assertion	eupth2	$⊢ φ \to \{x \in V \| \neg 2 ∥ VtxDeg (G) (x)\} = if (P (0) = P (\|F\|), \emptyset, \{P (0), P (\|F\|)\})$

Proof

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

Metamath Proof Explorer

Theorem eupth2

Proof