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