Metamath Proof Explorer


Theorem dfclnbgr4

Description: Alternate definition of the closed neighborhood of a vertex as union of the vertex with its open neighborhood. (Contributed by AV, 8-May-2025)

Ref Expression
Hypothesis dfclnbgr4.v V = Vtx G
Assertion dfclnbgr4 N V G ClNeighbVtx N = N G NeighbVtx N

Proof

Step Hyp Ref Expression
1 dfclnbgr4.v V = Vtx G
2 eqid Edg G = Edg G
3 1 2 dfclnbgr2 N V G ClNeighbVtx N = N n V | e Edg G N e n e
4 undif2 N n V | e Edg G N e n e N = N n V | e Edg G N e n e
5 rabdif n V | e Edg G N e n e N = n V N | e Edg G N e n e
6 5 uneq2i N n V | e Edg G N e n e N = N n V N | e Edg G N e n e
7 4 6 eqtr3i N n V | e Edg G N e n e = N n V N | e Edg G N e n e
8 1 2 dfnbgr2 N V G NeighbVtx N = n V N | e Edg G N e n e
9 8 eqcomd N V n V N | e Edg G N e n e = G NeighbVtx N
10 9 uneq2d N V N n V N | e Edg G N e n e = N G NeighbVtx N
11 7 10 eqtrid N V N n V | e Edg G N e n e = N G NeighbVtx N
12 3 11 eqtrd N V G ClNeighbVtx N = N G NeighbVtx N