Metamath Proof Explorer

Theorem clnbgrisvtx

Description: Every member N of the closed neighborhood of a vertex K is a vertex. (Contributed by AV, 9-May-2025)

Ref Expression
Hypothesis clnbgrvtxel.v ⊢ V = Vtx ⁡ G
Assertion clnbgrisvtx ⊢ N ∈ G ClNeighbVtx K → N ∈ V

Proof

Step Hyp Ref Expression
1 clnbgrvtxel.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 clnbgrel ⊢ N ∈ G ClNeighbVtx K ↔ N ∈ V ∧ K ∈ V ∧ N = K ∨ ∃ e ∈ Edg ⁡ G K N ⊆ e
4 simpll ⊢ N ∈ V ∧ K ∈ V ∧ N = K ∨ ∃ e ∈ Edg ⁡ G K N ⊆ e → N ∈ V
5 3 4 sylbi ⊢ N ∈ G ClNeighbVtx K → N ∈ V