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