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
⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdushgrfvedg.e
⊢ 𝐸 = ( Edg ‘ 𝐺 )
vtxdushgrfvedg.d
⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion
vtxdumgr0nedg
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑈 ) = 0 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )
Proof
Step
Hyp
Ref
Expression
1
vtxdushgrfvedg.v
⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
vtxdushgrfvedg.e
⊢ 𝐸 = ( Edg ‘ 𝐺 )
3
vtxdushgrfvedg.d
⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4
umgruhgr
⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
5
1 2 3
vtxduhgr0nedg
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑈 ) = 0 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )
6
4 5
syl3an1
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑈 ) = 0 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )