This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Vertex degree usgrvd00
Description: If every vertex in a simple graph has degree 0, there is no edge in the
graph. (Contributed by Alexander van der Vekens , 12-Jul-2018)
(Revised by AV , 17-Dec-2020) (Proof shortened by AV , 23-Dec-2020)
Ref
Expression
Hypotheses
vtxdusgradjvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdusgradjvtx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion
usgrvd00 ⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 → 𝐸 = ∅ ) )
Proof
Step
Hyp
Ref
Expression
1
vtxdusgradjvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
vtxdusgradjvtx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3
usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
4
1 2
uhgrvd00 ⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 → 𝐸 = ∅ ) )
5
3 4
syl ⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 → 𝐸 = ∅ ) )