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 ∈ UMGraph ∧ U ∈ V ∧ D ⁡ U = 0 → ¬ ∃ v ∈ V U v ∈ 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 ∈ UMGraph → G ∈ UHGraph
5 1 2 3 vtxduhgr0nedg ⊢ G ∈ UHGraph ∧ U ∈ V ∧ D ⁡ U = 0 → ¬ ∃ v ∈ V U v ∈ E
6 4 5 syl3an1 ⊢ G ∈ UMGraph ∧ U ∈ V ∧ D ⁡ U = 0 → ¬ ∃ v ∈ V U v ∈ E