Metamath Proof Explorer

Theorem nbgr0edg

Description: In an empty graph (with no edges), every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020) (Proof shortened by AV, 15-Nov-2020)

Ref Expression
Assertion nbgr0edg ⊢ Edg ⁡ G = ∅ → G NeighbVtx K = ∅

Proof

Step Hyp Ref Expression
1 rzal ⊢ Edg ⁡ G = ∅ → ∀ e ∈ Edg ⁡ G ¬ K n ⊆ e
2 ralnex ⊢ ∀ e ∈ Edg ⁡ G ¬ K n ⊆ e ↔ ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
3 1 2 sylib ⊢ Edg ⁡ G = ∅ → ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
4 3 ralrimivw ⊢ Edg ⁡ G = ∅ → ∀ n ∈ Vtx ⁡ G ∖ K ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
5 4 nbgr0vtxlem ⊢ Edg ⁡ G = ∅ → G NeighbVtx K = ∅