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 e. _V /\ N e. _V ) -> ( G NeighbVtx N ) = (/) )

Proof

Step Hyp Ref Expression
1 df-nbgr 
 |-  NeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { v } ) | E. e e. ( Edg ` g ) { v , n } C_ e } )
2 1 reldmmpo 
 |-  Rel dom NeighbVtx
3 2 ovprc 
 |-  ( -. ( G e. _V /\ N e. _V ) -> ( G NeighbVtx N ) = (/) )