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 𝑉 = ( 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 ) → ¬ ∃ 𝑣𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )