Database
GRAPH THEORY
Undirected graphs
Vertex degree
vtxdumgr0nedg
Metamath Proof Explorer
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