Metamath Proof Explorer

Theorem clnbgrval

Description: The closed neighborhood of a vertex V in a graph G . (Contributed by AV, 7-May-2025)

Ref Expression
Hypotheses clnbgrval.v ⊢ V = Vtx ⁡ G
clnbgrval.e ⊢ E = Edg ⁡ G
Assertion clnbgrval ⊢ N ∈ V → G ClNeighbVtx N = N ∪ n ∈ V | ∃ e ∈ E N n ⊆ e

Proof

Step Hyp Ref Expression
1 clnbgrval.v ⊢ V = Vtx ⁡ G
2 clnbgrval.e ⊢ E = Edg ⁡ G
3 df-clnbgr ⊢ ClNeighbVtx = g ∈ V , v ∈ Vtx ⁡ g ⟼ v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e
4 1 1vgrex ⊢ N ∈ V → G ∈ V
5 fveq2 ⊢ G = g → Vtx ⁡ G = Vtx ⁡ g
6 5 eqcoms ⊢ g = G → Vtx ⁡ G = Vtx ⁡ g
7 1 6 eqtrid ⊢ g = G → V = Vtx ⁡ g
8 7 eleq2d ⊢ g = G → N ∈ V ↔ N ∈ Vtx ⁡ g
9 8 biimpac ⊢ N ∈ V ∧ g = G → N ∈ Vtx ⁡ g
10 vsnex ⊢ v ∈ V
11 10 a1i ⊢ N ∈ V ∧ g = G ∧ v = N → v ∈ V
12 fvex ⊢ Vtx ⁡ g ∈ V
13 rabexg ⊢ Vtx ⁡ g ∈ V → n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e ∈ V
14 12 13 mp1i ⊢ N ∈ V ∧ g = G ∧ v = N → n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e ∈ V
15 11 14 unexd ⊢ N ∈ V ∧ g = G ∧ v = N → v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e ∈ V
16 sneq ⊢ v = N → v = N
17 16 adantl ⊢ g = G ∧ v = N → v = N
18 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
19 18 1 eqtr4di ⊢ g = G → Vtx ⁡ g = V
20 19 adantr ⊢ g = G ∧ v = N → Vtx ⁡ g = V
21 fveq2 ⊢ g = G → Edg ⁡ g = Edg ⁡ G
22 21 2 eqtr4di ⊢ g = G → Edg ⁡ g = E
23 22 adantr ⊢ g = G ∧ v = N → Edg ⁡ g = E
24 preq1 ⊢ v = N → v n = N n
25 24 sseq1d ⊢ v = N → v n ⊆ e ↔ N n ⊆ e
26 25 adantl ⊢ g = G ∧ v = N → v n ⊆ e ↔ N n ⊆ e
27 23 26 rexeqbidv ⊢ g = G ∧ v = N → ∃ e ∈ Edg ⁡ g v n ⊆ e ↔ ∃ e ∈ E N n ⊆ e
28 20 27 rabeqbidv ⊢ g = G ∧ v = N → n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e = n ∈ V | ∃ e ∈ E N n ⊆ e
29 17 28 uneq12d ⊢ g = G ∧ v = N → v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e = N ∪ n ∈ V | ∃ e ∈ E N n ⊆ e
30 29 adantl ⊢ N ∈ V ∧ g = G ∧ v = N → v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e = N ∪ n ∈ V | ∃ e ∈ E N n ⊆ e
31 4 9 15 30 ovmpodv2 ⊢ N ∈ V → ClNeighbVtx = g ∈ V , v ∈ Vtx ⁡ g ⟼ v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e → G ClNeighbVtx N = N ∪ n ∈ V | ∃ e ∈ E N n ⊆ e
32 3 31 mpi ⊢ N ∈ V → G ClNeighbVtx N = N ∪ n ∈ V | ∃ e ∈ E N n ⊆ e