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 V G NeighbVtx N = n V N | e E N n e

Proof

Step Hyp Ref Expression
1 nbgrval.v V = Vtx G
2 nbgrval.e E = Edg G
3 df-nbgr NeighbVtx = g V , k Vtx g n Vtx g k | e Edg g k n e
4 1 1vgrex N V G V
5 fveq2 g = G Vtx g = Vtx G
6 1 5 eqtr4id g = G V = Vtx g
7 6 eleq2d g = G N V N Vtx g
8 7 biimpac N V g = G N Vtx g
9 fvex Vtx g V
10 9 difexi Vtx g k V
11 rabexg Vtx g k V n Vtx g k | e Edg g k n e V
12 10 11 mp1i N V g = G k = N n Vtx g k | e Edg g k n 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 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 V g = G k = N Edg g = E
23 preq1 k = N k n = N n
24 23 sseq1d k = N k n e N n e
25 24 adantl g = G k = N k n e N n e
26 25 adantl N V g = G k = N k n e N n e
27 22 26 rexeqbidv N V g = G k = N e Edg g k n e e E N n e
28 18 27 rabeqbidv N V g = G k = N n Vtx g k | e Edg g k n e = n V N | e E N n e
29 4 8 12 28 ovmpodv2 N V NeighbVtx = g V , k Vtx g n Vtx g k | e Edg g k n e G NeighbVtx N = n V N | e E N n e
30 3 29 mpi N V G NeighbVtx N = n V N | e E N n e