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→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆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⁡gkn⊆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⁡gkn⊆e∈V
12 10 11 mp1i ⊢N∈V∧g=G∧k=N→n∈Vtx⁡g∖k|∃e∈Edg⁡gkn⊆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→kn=Nn
24 23 sseq1d ⊢k=N→kn⊆e↔Nn⊆e
25 24 adantl ⊢g=G∧k=N→kn⊆e↔Nn⊆e
26 25 adantl ⊢N∈V∧g=G∧k=N→kn⊆e↔Nn⊆e
27 22 26 rexeqbidv ⊢N∈V∧g=G∧k=N→∃e∈Edg⁡gkn⊆e↔∃e∈ENn⊆e
28 18 27 rabeqbidv ⊢N∈V∧g=G∧k=N→n∈Vtx⁡g∖k|∃e∈Edg⁡gkn⊆e=n∈V∖N|∃e∈ENn⊆e
29 4 8 12 28 ovmpodv2 ⊢N∈V→NeighbVtx=g∈V,k∈Vtx⁡g⟼n∈Vtx⁡g∖k|∃e∈Edg⁡gkn⊆e→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆e
30 3 29 mpi ⊢N∈V→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆e