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

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

Step

Hyp

Ref

Expression

 |-  ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) )

 |-  Rel dom ClNeighbVtx

 |-  ( -. ( G e. _V /\ N e. _V ) -> ( G ClNeighbVtx N ) = (/) )