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