This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfclnbgr4

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

Ref Expression
Hypothesis dfclnbgr4.v 
|- V = ( Vtx ` G )
Assertion dfclnbgr4 
|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) )

Proof

Step Hyp Ref Expression
1 dfclnbgr4.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 dfclnbgr2 
 |-  ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } ) )
4 undif2 
 |-  ( { N } u. ( { n e. V | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } \ { N } ) ) = ( { N } u. { n e. V | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } )
5 rabdif 
 |-  ( { n e. V | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } \ { N } ) = { n e. ( V \ { N } ) | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) }
6 5 uneq2i 
 |-  ( { N } u. ( { n e. V | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } \ { N } ) ) = ( { N } u. { n e. ( V \ { N } ) | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } )
7 4 6 eqtr3i 
 |-  ( { N } u. { n e. V | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } ) = ( { N } u. { n e. ( V \ { N } ) | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } )
8 1 2 dfnbgr2 
 |-  ( N e. V -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } )
9 8 eqcomd 
 |-  ( N e. V -> { n e. ( V \ { N } ) | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } = ( G NeighbVtx N ) )
10 9 uneq2d 
 |-  ( N e. V -> ( { N } u. { n e. ( V \ { N } ) | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } ) = ( { N } u. ( G NeighbVtx N ) ) )
11 7 10 eqtrid 
 |-  ( N e. V -> ( { N } u. { n e. V | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } ) = ( { N } u. ( G NeighbVtx N ) ) )
12 3 11 eqtrd 
 |-  ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) )