vtxd0nedgb

Description: A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020) (Revised by AV, 22-Mar-2021)

	Ref	Expression
Hypotheses	vtxd0nedgb.v	$⊢ V = Vtx (G)$
	vtxd0nedgb.i	$⊢ I = iEdg (G)$
	vtxd0nedgb.d	$⊢ D = VtxDeg (G)$
Assertion	vtxd0nedgb	$⊢ U \in V \to (D (U) = 0 \leftrightarrow \neg \exists i \in dom I U \in I (i))$

Proof

Step	Hyp	Ref	Expression
1		vtxd0nedgb.v	$⊢ V = Vtx (G)$
2		vtxd0nedgb.i	$⊢ I = iEdg (G)$
3		vtxd0nedgb.d	$⊢ D = VtxDeg (G)$
4	3	fveq1i	$⊢ D (U) = VtxDeg (G) (U)$
5		eqid	$⊢ dom I = dom I$
6	1 2 5	vtxdgval	$⊢ U \in V \to VtxDeg (G) (U) = \|\{i \in dom I \| U \in I (i)\}\| +_{𝑒} \|\{i \in dom I \| I (i) = \{U\}\}\|$
7	4 6	syl5eq	$⊢ U \in V \to D (U) = \|\{i \in dom I \| U \in I (i)\}\| +_{𝑒} \|\{i \in dom I \| I (i) = \{U\}\}\|$
8	7	eqeq1d	$⊢ U \in V \to (D (U) = 0 \leftrightarrow \|\{i \in dom I \| U \in I (i)\}\| +_{𝑒} \|\{i \in dom I \| I (i) = \{U\}\}\| = 0)$
9	2	fvexi	$⊢ I \in V$
10	9	dmex	$⊢ dom I \in V$
11	10	rabex	$⊢ \{i \in dom I \| U \in I (i)\} \in V$
12		hashxnn0	$⊢ \{i \in dom I \| U \in I (i)\} \in V \to \|\{i \in dom I \| U \in I (i)\}\| \in ℕ_{0}^{*}$
13	11 12	ax-mp	$⊢ \|\{i \in dom I \| U \in I (i)\}\| \in ℕ_{0}^{*}$
14	10	rabex	$⊢ \{i \in dom I \| I (i) = \{U\}\} \in V$
15		hashxnn0	$⊢ \{i \in dom I \| I (i) = \{U\}\} \in V \to \|\{i \in dom I \| I (i) = \{U\}\}\| \in ℕ_{0}^{*}$
16	14 15	ax-mp	$⊢ \|\{i \in dom I \| I (i) = \{U\}\}\| \in ℕ_{0}^{*}$
17	13 16	pm3.2i	$⊢ (\|\{i \in dom I \| U \in I (i)\}\| \in ℕ_{0}^{} \land \|\{i \in dom I \| I (i) = \{U\}\}\| \in ℕ_{0}^{})$
18		xnn0xadd0	$⊢ (\|\{i \in dom I \| U \in I (i)\}\| \in ℕ_{0}^{} \land \|\{i \in dom I \| I (i) = \{U\}\}\| \in ℕ_{0}^{}) \to (\|\{i \in dom I \| U \in I (i)\}\| +_{𝑒} \|\{i \in dom I \| I (i) = \{U\}\}\| = 0 \leftrightarrow (\|\{i \in dom I \| U \in I (i)\}\| = 0 \land \|\{i \in dom I \| I (i) = \{U\}\}\| = 0))$
19	17 18	mp1i	$⊢ U \in V \to (\|\{i \in dom I \| U \in I (i)\}\| +_{𝑒} \|\{i \in dom I \| I (i) = \{U\}\}\| = 0 \leftrightarrow (\|\{i \in dom I \| U \in I (i)\}\| = 0 \land \|\{i \in dom I \| I (i) = \{U\}\}\| = 0))$
20		hasheq0	$⊢ \{i \in dom I \| U \in I (i)\} \in V \to (\|\{i \in dom I \| U \in I (i)\}\| = 0 \leftrightarrow \{i \in dom I \| U \in I (i)\} = \emptyset)$
21	11 20	ax-mp	$⊢ \|\{i \in dom I \| U \in I (i)\}\| = 0 \leftrightarrow \{i \in dom I \| U \in I (i)\} = \emptyset$
22		hasheq0	$⊢ \{i \in dom I \| I (i) = \{U\}\} \in V \to (\|\{i \in dom I \| I (i) = \{U\}\}\| = 0 \leftrightarrow \{i \in dom I \| I (i) = \{U\}\} = \emptyset)$
23	14 22	ax-mp	$⊢ \|\{i \in dom I \| I (i) = \{U\}\}\| = 0 \leftrightarrow \{i \in dom I \| I (i) = \{U\}\} = \emptyset$
24	21 23	anbi12i	$⊢ (\|\{i \in dom I \| U \in I (i)\}\| = 0 \land \|\{i \in dom I \| I (i) = \{U\}\}\| = 0) \leftrightarrow (\{i \in dom I \| U \in I (i)\} = \emptyset \land \{i \in dom I \| I (i) = \{U\}\} = \emptyset)$
25		rabeq0	$⊢ \{i \in dom I \| U \in I (i)\} = \emptyset \leftrightarrow \forall i \in dom I \neg U \in I (i)$
26		rabeq0	$⊢ \{i \in dom I \| I (i) = \{U\}\} = \emptyset \leftrightarrow \forall i \in dom I \neg I (i) = \{U\}$
27	25 26	anbi12i	$⊢ (\{i \in dom I \| U \in I (i)\} = \emptyset \land \{i \in dom I \| I (i) = \{U\}\} = \emptyset) \leftrightarrow (\forall i \in dom I \neg U \in I (i) \land \forall i \in dom I \neg I (i) = \{U\})$
28		ralnex	$⊢ \forall i \in dom I \neg (U \in I (i) \lor I (i) = \{U\}) \leftrightarrow \neg \exists i \in dom I (U \in I (i) \lor I (i) = \{U\})$
29	28	bicomi	$⊢ \neg \exists i \in dom I (U \in I (i) \lor I (i) = \{U\}) \leftrightarrow \forall i \in dom I \neg (U \in I (i) \lor I (i) = \{U\})$
30		ioran	$⊢ \neg (U \in I (i) \lor I (i) = \{U\}) \leftrightarrow (\neg U \in I (i) \land \neg I (i) = \{U\})$
31	30	ralbii	$⊢ \forall i \in dom I \neg (U \in I (i) \lor I (i) = \{U\}) \leftrightarrow \forall i \in dom I (\neg U \in I (i) \land \neg I (i) = \{U\})$
32		r19.26	$⊢ \forall i \in dom I (\neg U \in I (i) \land \neg I (i) = \{U\}) \leftrightarrow (\forall i \in dom I \neg U \in I (i) \land \forall i \in dom I \neg I (i) = \{U\})$
33	29 31 32	3bitri	$⊢ \neg \exists i \in dom I (U \in I (i) \lor I (i) = \{U\}) \leftrightarrow (\forall i \in dom I \neg U \in I (i) \land \forall i \in dom I \neg I (i) = \{U\})$
34	33	bicomi	$⊢ (\forall i \in dom I \neg U \in I (i) \land \forall i \in dom I \neg I (i) = \{U\}) \leftrightarrow \neg \exists i \in dom I (U \in I (i) \lor I (i) = \{U\})$
35	24 27 34	3bitri	$⊢ (\|\{i \in dom I \| U \in I (i)\}\| = 0 \land \|\{i \in dom I \| I (i) = \{U\}\}\| = 0) \leftrightarrow \neg \exists i \in dom I (U \in I (i) \lor I (i) = \{U\})$
36		orcom	$⊢ (U \in I (i) \lor I (i) = \{U\}) \leftrightarrow (I (i) = \{U\} \lor U \in I (i))$
37		snidg	$⊢ U \in V \to U \in \{U\}$
38		eleq2	$⊢ I (i) = \{U\} \to (U \in I (i) \leftrightarrow U \in \{U\})$
39	37 38	syl5ibrcom	$⊢ U \in V \to (I (i) = \{U\} \to U \in I (i))$
40		pm4.72	$⊢ (I (i) = \{U\} \to U \in I (i)) \leftrightarrow (U \in I (i) \leftrightarrow (I (i) = \{U\} \lor U \in I (i)))$
41	39 40	sylib	$⊢ U \in V \to (U \in I (i) \leftrightarrow (I (i) = \{U\} \lor U \in I (i)))$
42	36 41	bitr4id	$⊢ U \in V \to ((U \in I (i) \lor I (i) = \{U\}) \leftrightarrow U \in I (i))$
43	42	rexbidv	$⊢ U \in V \to (\exists i \in dom I (U \in I (i) \lor I (i) = \{U\}) \leftrightarrow \exists i \in dom I U \in I (i))$
44	43	notbid	$⊢ U \in V \to (\neg \exists i \in dom I (U \in I (i) \lor I (i) = \{U\}) \leftrightarrow \neg \exists i \in dom I U \in I (i))$
45	35 44	syl5bb	$⊢ U \in V \to ((\|\{i \in dom I \| U \in I (i)\}\| = 0 \land \|\{i \in dom I \| I (i) = \{U\}\}\| = 0) \leftrightarrow \neg \exists i \in dom I U \in I (i))$
46	8 19 45	3bitrd	$⊢ U \in V \to (D (U) = 0 \leftrightarrow \neg \exists i \in dom I U \in I (i))$

Metamath Proof Explorer

Theorem vtxd0nedgb

Proof