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

Proof

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