This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clnbgrcl

Description: If a class X has at least one element in its closed neighborhood, this class must be a vertex. (Contributed by AV, 7-May-2025)

Ref Expression
Hypothesis clnbgrcl.v ⊢ V = Vtx ⁡ G
Assertion clnbgrcl ⊢ N ∈ G ClNeighbVtx X → X ∈ V

Proof

Step Hyp Ref Expression
1 clnbgrcl.v ⊢ V = Vtx ⁡ G
2 df-clnbgr ⊢ ClNeighbVtx = g ∈ V , v ∈ Vtx ⁡ g ⟼ v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e
3 2 mpoxeldm ⊢ N ∈ G ClNeighbVtx X → G ∈ V ∧ X ∈ ⦋ G / g⦌ Vtx ⁡ g
4 csbfv ⊢ ⦋ G / g⦌ Vtx ⁡ g = Vtx ⁡ G
5 4 1 eqtr4i ⊢ ⦋ G / g⦌ Vtx ⁡ g = V
6 5 eleq2i ⊢ X ∈ ⦋ G / g⦌ Vtx ⁡ g ↔ X ∈ V
7 6 biimpi ⊢ X ∈ ⦋ G / g⦌ Vtx ⁡ g → X ∈ V
8 3 7 simpl2im ⊢ N ∈ G ClNeighbVtx X → X ∈ V