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

Metamath Proof Explorer

Theorem dfnbgr3

Description: Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval ). (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 25-Oct-2020) (Revised by AV, 21-Mar-2021)

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

Proof

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