Metamath Proof Explorer

Theorem nbgrnvtx0

Description: If a class X is not a vertex of a graph G , then it has no neighbors in G . (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Hypothesis nbgrel.v ⊢ V = Vtx ⁡ G
Assertion nbgrnvtx0 ⊢ X ∉ V → G NeighbVtx X = ∅

Proof

Step Hyp Ref Expression
1 nbgrel.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-nbgr ⊢ NeighbVtx = g ∈ V , v ∈ Vtx ⁡ g ⟼ n ∈ Vtx ⁡ g ∖ v | ∃ e ∈ Edg ⁡ g v n ⊆ e
9 8 mpoxneldm ⊢ G ∉ V ∨ X ∉ ⦋ G / g⦌ Vtx ⁡ g → G NeighbVtx X = ∅
10 7 9 syl ⊢ X ∉ V → G NeighbVtx X = ∅