This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtxdumgr0nedg

Description: If a vertex in a multigraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017) (Revised by AV, 12-Dec-2020) (Proof shortened by AV, 15-Dec-2020)

	Ref	Expression
Hypotheses	vtxdushgrfvedg.v	$⊢ V = Vtx (G)$
	vtxdushgrfvedg.e	$⊢ E = Edg (G)$
	vtxdushgrfvedg.d	$⊢ D = VtxDeg (G)$
Assertion	vtxdumgr0nedg	$⊢ (G \in UMGraph \land U \in V \land D (U) = 0) \to \neg \exists v \in V \{U, v\} \in E$

Proof

Step	Hyp	Ref	Expression
1		vtxdushgrfvedg.v	$⊢ V = Vtx (G)$
2		vtxdushgrfvedg.e	$⊢ E = Edg (G)$
3		vtxdushgrfvedg.d	$⊢ D = VtxDeg (G)$
4		umgruhgr	$⊢ G \in UMGraph \to G \in UHGraph$
5	1 2 3	vtxduhgr0nedg	$⊢ (G \in UHGraph \land U \in V \land D (U) = 0) \to \neg \exists v \in V \{U, v\} \in E$
6	4 5	syl3an1	$⊢ (G \in UMGraph \land U \in V \land D (U) = 0) \to \neg \exists v \in V \{U, v\} \in E$