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

Metamath Proof Explorer

Theorem dfclnbgr3

Description: Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval ). (Contributed by AV, 8-May-2025)

Ref Expression
Hypotheses dfclnbgr3.v 
|- V = ( Vtx ` G )
dfclnbgr3.i 
|- I = ( iEdg ` G )
Assertion dfclnbgr3 
|- ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } ) )

Proof

Step Hyp Ref Expression
1 dfclnbgr3.v 
 |-  V = ( Vtx ` G )
2 dfclnbgr3.i 
 |-  I = ( iEdg ` G )
3 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
4 3 eqcomi 
 |-  ran ( iEdg ` G ) = ( Edg ` G )
5 1 4 clnbgrval 
 |-  ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) )
6 5 adantr 
 |-  ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) )
7 2 eqcomi 
 |-  ( iEdg ` G ) = I
8 7 rneqi 
 |-  ran ( iEdg ` G ) = ran I
9 8 rexeqi 
 |-  ( E. e e. ran ( iEdg ` G ) { N , n } C_ e <-> E. e e. ran I { N , n } C_ e )
10 funfn 
 |-  ( Fun I <-> I Fn dom I )
11 10 biimpi 
 |-  ( Fun I -> I Fn dom I )
12 11 adantl 
 |-  ( ( N e. V /\ Fun I ) -> I Fn dom I )
13 sseq2 
 |-  ( e = ( I ` i ) -> ( { N , n } C_ e <-> { N , n } C_ ( I ` i ) ) )
14 13 rexrn 
 |-  ( I Fn dom I -> ( E. e e. ran I { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
15 12 14 syl 
 |-  ( ( N e. V /\ Fun I ) -> ( E. e e. ran I { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
16 9 15 bitrid 
 |-  ( ( N e. V /\ Fun I ) -> ( E. e e. ran ( iEdg ` G ) { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
17 16 rabbidv 
 |-  ( ( N e. V /\ Fun I ) -> { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } = { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } )
18 17 uneq2d 
 |-  ( ( N e. V /\ Fun I ) -> ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) = ( { N } u. { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } ) )
19 6 18 eqtrd 
 |-  ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } ) )