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

Metamath Proof Explorer

Theorem clnbgrnvtx0

Description: If a class X is not a vertex of a graph G , then it has an empty closed neighborhood in G . (Contributed by AV, 8-May-2025)

Ref Expression
Hypothesis clnbgrel.v ⊢ V = Vtx ⁡ G
Assertion clnbgrnvtx0 ⊢ X ∉ V → G ClNeighbVtx X = ∅

Proof

Step Hyp Ref Expression
1 clnbgrel.v ⊢ V = Vtx ⁡ G
2 csbfv ⊢ ⦋ G / g⦌ Vtx ⁡ g = Vtx ⁡ G
3 1 2 eqtr4i ⊢ V = ⦋ G / g⦌ Vtx ⁡ g
4 neleq2 ⊢ V = ⦋ G / g⦌ Vtx ⁡ g → X ∉ V ↔ X ∉ ⦋ G / g⦌ Vtx ⁡ g
5 3 4 ax-mp ⊢ X ∉ V ↔ X ∉ ⦋ G / g⦌ Vtx ⁡ g
6 5 biimpi ⊢ X ∉ V → X ∉ ⦋ G / g⦌ Vtx ⁡ g
7 6 olcd ⊢ X ∉ V → G ∉ V ∨ X ∉ ⦋ G / g⦌ Vtx ⁡ g
8 df-clnbgr ⊢ ClNeighbVtx = g ∈ V , v ∈ Vtx ⁡ g ⟼ v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e
9 8 mpoxneldm ⊢ G ∉ V ∨ X ∉ ⦋ G / g⦌ Vtx ⁡ g → G ClNeighbVtx X = ∅
10 7 9 syl ⊢ X ∉ V → G ClNeighbVtx X = ∅