Metamath Proof Explorer

Theorem clnbgrprc0

Description: The closed neighborhood is empty if the graph G or the vertex N are proper classes. (Contributed by AV, 7-May-2025)

Ref Expression
Assertion clnbgrprc0 ⊢ ¬ G ∈ V ∧ N ∈ V → G ClNeighbVtx N = ∅

Proof

Step Hyp Ref Expression
1 df-clnbgr ⊢ ClNeighbVtx = g ∈ V , v ∈ Vtx ⁡ g ⟼ v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ ClNeighbVtx
3 2 ovprc ⊢ ¬ G ∈ V ∧ N ∈ V → G ClNeighbVtx N = ∅