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

Metamath Proof Explorer

Theorem nbgrcl

Description: If a class X has at least one neighbor, this class must be a vertex. (Contributed by AV, 6-Jun-2021) (Revised by AV, 12-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 nbgrcl.v ⊢ V = Vtx ⁡ G
2 df-nbgr ⊢ NeighbVtx = g ∈ V , v ∈ Vtx ⁡ g ⟼ n ∈ Vtx ⁡ g ∖ v | ∃ e ∈ Edg ⁡ g v n ⊆ e
3 2 mpoxeldm ⊢ N ∈ G NeighbVtx 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 NeighbVtx X → X ∈ V