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

Metamath Proof Explorer

Theorem dfclnbgr2

Description: Alternate definition of the closed neighborhood of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 7-May-2025)

Ref Expression
Hypotheses clnbgrval.v 
|- V = ( Vtx ` G )
clnbgrval.e 
|- E = ( Edg ` G )
Assertion dfclnbgr2 
|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )

Proof

Step Hyp Ref Expression
1 clnbgrval.v 
 |-  V = ( Vtx ` G )
2 clnbgrval.e 
 |-  E = ( Edg ` G )
3 1 2 clnbgrval 
 |-  ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E { N , n } C_ e } ) )
4 prssg 
 |-  ( ( N e. V /\ n e. _V ) -> ( ( N e. e /\ n e. e ) <-> { N , n } C_ e ) )
5 4 elvd 
 |-  ( N e. V -> ( ( N e. e /\ n e. e ) <-> { N , n } C_ e ) )
6 5 bicomd 
 |-  ( N e. V -> ( { N , n } C_ e <-> ( N e. e /\ n e. e ) ) )
7 6 rexbidv 
 |-  ( N e. V -> ( E. e e. E { N , n } C_ e <-> E. e e. E ( N e. e /\ n e. e ) ) )
8 7 rabbidv 
 |-  ( N e. V -> { n e. V | E. e e. E { N , n } C_ e } = { n e. V | E. e e. E ( N e. e /\ n e. e ) } )
9 8 uneq2d 
 |-  ( N e. V -> ( { N } u. { n e. V | E. e e. E { N , n } C_ e } ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )
10 3 9 eqtrd 
 |-  ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )