Theorem dfclnbgr5

Description: Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiclosed neighborhood. (Contributed by AV, 16-May-2025)

	Ref	Expression
Hypotheses	dfsclnbgr2.v	|- V = ( Vtx ` G )
	dfsclnbgr2.s	|- S = { n e. V | E. e e. E { N , n } C_ e }
	dfsclnbgr2.e	|- E = ( Edg ` G )
Assertion	dfclnbgr5	|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. S ) )

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	|- V = ( Vtx ` G )
2		dfsclnbgr2.s	|- S = { n e. V | E. e e. E { N , n } C_ e }
3		dfsclnbgr2.e	|- E = ( Edg ` G )
4	1 3	dfclnbgr2	|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )
5	1 2 3	dfsclnbgr2	|- ( N e. V -> S = { n e. V | E. e e. E ( N e. e /\ n e. e ) } )
6	5	uneq2d	|- ( N e. V -> ( { N } u. S ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )
7	4 6	eqtr4d	|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. S ) )