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	⊢ ( ¬ ( 𝐺 ∈ V ∧ 𝑁 ∈ V ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-nbgr	⊢ NeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )
2	1	reldmmpo	⊢ Rel dom NeighbVtx
3	2	ovprc	⊢ ( ¬ ( 𝐺 ∈ V ∧ 𝑁 ∈ V ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )