Metamath Proof Explorer

Theorem nbgrprc0

Description: The set of neighbors is empty if the graph G or the vertex N are proper classes. (Contributed by AV, 26-Oct-2020)

Ref Expression
Assertion nbgrprc0 ⊢ ¬ G ∈ V ∧ N ∈ V → G NeighbVtx N = ∅

Proof

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