1hevtxdg0

Description: The vertex degree of vertex D in a graph G with only one hyperedge E is 0 if D is not incident with the edge E . (Contributed by AV, 2-Mar-2021)

	Ref	Expression
Hypotheses	1hevtxdg0.i	$⊢ φ \to iEdg (G) = \{⟨A, E⟩\}$
	1hevtxdg0.v	$⊢ φ \to Vtx (G) = V$
	1hevtxdg0.a	$⊢ φ \to A \in X$
	1hevtxdg0.d	$⊢ φ \to D \in V$
	1hevtxdg0.e	$⊢ φ \to E \in Y$
	1hevtxdg0.n	$⊢ φ \to D \notin E$
Assertion	1hevtxdg0	$⊢ φ \to VtxDeg (G) (D) = 0$

Proof

Step	Hyp	Ref	Expression
1		1hevtxdg0.i	$⊢ φ \to iEdg (G) = \{⟨A, E⟩\}$
2		1hevtxdg0.v	$⊢ φ \to Vtx (G) = V$
3		1hevtxdg0.a	$⊢ φ \to A \in X$
4		1hevtxdg0.d	$⊢ φ \to D \in V$
5		1hevtxdg0.e	$⊢ φ \to E \in Y$
6		1hevtxdg0.n	$⊢ φ \to D \notin E$
7		df-nel	$⊢ D \notin E \leftrightarrow \neg D \in E$
8	6 7	sylib	$⊢ φ \to \neg D \in E$
9	1	fveq1d	$⊢ φ \to iEdg (G) (A) = \{⟨A, E⟩\} (A)$
10		fvsng	$⊢ (A \in X \land E \in Y) \to \{⟨A, E⟩\} (A) = E$
11	3 5 10	syl2anc	$⊢ φ \to \{⟨A, E⟩\} (A) = E$
12	9 11	eqtrd	$⊢ φ \to iEdg (G) (A) = E$
13	8 12	neleqtrrd	$⊢ φ \to \neg D \in iEdg (G) (A)$
14		fveq2	$⊢ x = A \to iEdg (G) (x) = iEdg (G) (A)$
15	14	eleq2d	$⊢ x = A \to (D \in iEdg (G) (x) \leftrightarrow D \in iEdg (G) (A))$
16	15	notbid	$⊢ x = A \to (\neg D \in iEdg (G) (x) \leftrightarrow \neg D \in iEdg (G) (A))$
17	16	ralsng	$⊢ A \in X \to (\forall x \in \{A\} \neg D \in iEdg (G) (x) \leftrightarrow \neg D \in iEdg (G) (A))$
18	3 17	syl	$⊢ φ \to (\forall x \in \{A\} \neg D \in iEdg (G) (x) \leftrightarrow \neg D \in iEdg (G) (A))$
19	13 18	mpbird	$⊢ φ \to \forall x \in \{A\} \neg D \in iEdg (G) (x)$
20	1	dmeqd	$⊢ φ \to dom iEdg (G) = dom \{⟨A, E⟩\}$
21		dmsnopg	$⊢ E \in Y \to dom \{⟨A, E⟩\} = \{A\}$
22	5 21	syl	$⊢ φ \to dom \{⟨A, E⟩\} = \{A\}$
23	20 22	eqtrd	$⊢ φ \to dom iEdg (G) = \{A\}$
24	23	raleqdv	$⊢ φ \to (\forall x \in dom iEdg (G) \neg D \in iEdg (G) (x) \leftrightarrow \forall x \in \{A\} \neg D \in iEdg (G) (x))$
25	19 24	mpbird	$⊢ φ \to \forall x \in dom iEdg (G) \neg D \in iEdg (G) (x)$
26		ralnex	$⊢ \forall x \in dom iEdg (G) \neg D \in iEdg (G) (x) \leftrightarrow \neg \exists x \in dom iEdg (G) D \in iEdg (G) (x)$
27	25 26	sylib	$⊢ φ \to \neg \exists x \in dom iEdg (G) D \in iEdg (G) (x)$
28	2	eleq2d	$⊢ φ \to (D \in Vtx (G) \leftrightarrow D \in V)$
29	4 28	mpbird	$⊢ φ \to D \in Vtx (G)$
30		eqid	$⊢ Vtx (G) = Vtx (G)$
31		eqid	$⊢ iEdg (G) = iEdg (G)$
32		eqid	$⊢ VtxDeg (G) = VtxDeg (G)$
33	30 31 32	vtxd0nedgb	$⊢ D \in Vtx (G) \to (VtxDeg (G) (D) = 0 \leftrightarrow \neg \exists x \in dom iEdg (G) D \in iEdg (G) (x))$
34	29 33	syl	$⊢ φ \to (VtxDeg (G) (D) = 0 \leftrightarrow \neg \exists x \in dom iEdg (G) D \in iEdg (G) (x))$
35	27 34	mpbird	$⊢ φ \to VtxDeg (G) (D) = 0$

Metamath Proof Explorer

Theorem 1hevtxdg0

Proof