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

Metamath Proof Explorer

Theorem clnbupgr

Description: The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025)

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

Proof

Step Hyp Ref Expression
1 clnbuhgr.v 
 |-  V = ( Vtx ` G )
2 clnbuhgr.e 
 |-  E = ( Edg ` G )
3 1 dfclnbgr4 
 |-  ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) )
4 3 adantl 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) )
5 1 2 nbupgr 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | { N , n } e. E } )
6 5 uneq2d 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( { N } u. ( G NeighbVtx N ) ) = ( { N } u. { n e. ( V \ { N } ) | { N , n } e. E } ) )
7 rabdif 
 |-  ( { n e. V | { N , n } e. E } \ { N } ) = { n e. ( V \ { N } ) | { N , n } e. E }
8 7 eqcomi 
 |-  { n e. ( V \ { N } ) | { N , n } e. E } = ( { n e. V | { N , n } e. E } \ { N } )
9 8 uneq2i 
 |-  ( { N } u. { n e. ( V \ { N } ) | { N , n } e. E } ) = ( { N } u. ( { n e. V | { N , n } e. E } \ { N } ) )
10 undif2 
 |-  ( { N } u. ( { n e. V | { N , n } e. E } \ { N } ) ) = ( { N } u. { n e. V | { N , n } e. E } )
11 9 10 eqtri 
 |-  ( { N } u. { n e. ( V \ { N } ) | { N , n } e. E } ) = ( { N } u. { n e. V | { N , n } e. E } )
12 11 a1i 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( { N } u. { n e. ( V \ { N } ) | { N , n } e. E } ) = ( { N } u. { n e. V | { N , n } e. E } ) )
13 4 6 12 3eqtrd 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | { N , n } e. E } ) )