Metamath Proof Explorer


Theorem 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 → 𝐸 = ∅ ) )