Metamath Proof Explorer

Theorem vtxdusgr0edgnel

Description: A vertex in a simple graph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020) (Proof shortened by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢ V = Vtx ⁡ G
vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
Assertion vtxdusgr0edgnel ⊢ G ∈ USGraph ∧ U ∈ V → D ⁡ U = 0 ↔ ¬ ∃ e ∈ E U ∈ e

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢ V = Vtx ⁡ G
2 vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
3 vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
4 usgruhgr ⊢ G ∈ USGraph → G ∈ UHGraph
5 1 2 3 vtxduhgr0edgnel ⊢ G ∈ UHGraph ∧ U ∈ V → D ⁡ U = 0 ↔ ¬ ∃ e ∈ E U ∈ e
6 4 5 sylan ⊢ G ∈ USGraph ∧ U ∈ V → D ⁡ U = 0 ↔ ¬ ∃ e ∈ E U ∈ e