Metamath Proof Explorer

Theorem nbgrval

Description: The set of neighbors of a vertex V in a graph G . (Contributed by Alexander van der Vekens, 7-Oct-2017) (Revised by AV, 24-Oct-2020) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypotheses nbgrval.v 
|- V = ( Vtx ` G )
nbgrval.e 
|- E = ( Edg ` G )
Assertion nbgrval 
|- ( N e. V -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )

Proof

Step Hyp Ref Expression
1 nbgrval.v 
 |-  V = ( Vtx ` G )
2 nbgrval.e 
 |-  E = ( Edg ` G )
3 df-nbgr 
 |-  NeighbVtx = ( g e. _V , k e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { k } ) | E. e e. ( Edg ` g ) { k , n } C_ e } )
4 1 1vgrex 
 |-  ( N e. V -> G e. _V )
5 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
6 1 5 eqtr4id 
 |-  ( g = G -> V = ( Vtx ` g ) )
7 6 eleq2d 
 |-  ( g = G -> ( N e. V <-> N e. ( Vtx ` g ) ) )
8 7 biimpac 
 |-  ( ( N e. V /\ g = G ) -> N e. ( Vtx ` g ) )
9 fvex 
 |-  ( Vtx ` g ) e. _V
10 9 difexi 
 |-  ( ( Vtx ` g ) \ { k } ) e. _V
11 rabexg 
 |-  ( ( ( Vtx ` g ) \ { k } ) e. _V -> { n e. ( ( Vtx ` g ) \ { k } ) | E. e e. ( Edg ` g ) { k , n } C_ e } e. _V )
12 10 11 mp1i 
 |-  ( ( N e. V /\ ( g = G /\ k = N ) ) -> { n e. ( ( Vtx ` g ) \ { k } ) | E. e e. ( Edg ` g ) { k , n } C_ e } e. _V )
13 5 1 eqtr4di 
 |-  ( g = G -> ( Vtx ` g ) = V )
14 13 adantr 
 |-  ( ( g = G /\ k = N ) -> ( Vtx ` g ) = V )
15 sneq 
 |-  ( k = N -> { k } = { N } )
16 15 adantl 
 |-  ( ( g = G /\ k = N ) -> { k } = { N } )
17 14 16 difeq12d 
 |-  ( ( g = G /\ k = N ) -> ( ( Vtx ` g ) \ { k } ) = ( V \ { N } ) )
18 17 adantl 
 |-  ( ( N e. V /\ ( g = G /\ k = N ) ) -> ( ( Vtx ` g ) \ { k } ) = ( V \ { N } ) )
19 fveq2 
 |-  ( g = G -> ( Edg ` g ) = ( Edg ` G ) )
20 19 2 eqtr4di 
 |-  ( g = G -> ( Edg ` g ) = E )
21 20 adantr 
 |-  ( ( g = G /\ k = N ) -> ( Edg ` g ) = E )
22 21 adantl 
 |-  ( ( N e. V /\ ( g = G /\ k = N ) ) -> ( Edg ` g ) = E )
23 preq1 
 |-  ( k = N -> { k , n } = { N , n } )
24 23 sseq1d 
 |-  ( k = N -> ( { k , n } C_ e <-> { N , n } C_ e ) )
25 24 adantl 
 |-  ( ( g = G /\ k = N ) -> ( { k , n } C_ e <-> { N , n } C_ e ) )
26 25 adantl 
 |-  ( ( N e. V /\ ( g = G /\ k = N ) ) -> ( { k , n } C_ e <-> { N , n } C_ e ) )
27 22 26 rexeqbidv 
 |-  ( ( N e. V /\ ( g = G /\ k = N ) ) -> ( E. e e. ( Edg ` g ) { k , n } C_ e <-> E. e e. E { N , n } C_ e ) )
28 18 27 rabeqbidv 
 |-  ( ( N e. V /\ ( g = G /\ k = N ) ) -> { n e. ( ( Vtx ` g ) \ { k } ) | E. e e. ( Edg ` g ) { k , n } C_ e } = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )
29 4 8 12 28 ovmpodv2 
 |-  ( N e. V -> ( NeighbVtx = ( g e. _V , k e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { k } ) | E. e e. ( Edg ` g ) { k , n } C_ e } ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } ) )
30 3 29 mpi 
 |-  ( N e. V -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )