Metamath Proof Explorer

Theorem dfnbgr5

Description: Alternate definition of the (open) neighborhood of a vertex as a semiclosed neighborhood without itself. (Contributed by AV, 16-May-2025)

Ref Expression
Hypotheses dfsclnbgr2.v ⊢ V = Vtx ⁡ G
dfsclnbgr2.s ⊢ S = n ∈ V | ∃ e ∈ E N n ⊆ e
dfsclnbgr2.e ⊢ E = Edg ⁡ G
Assertion dfnbgr5 ⊢ N ∈ V → G NeighbVtx N = S ∖ N

Proof

Step Hyp Ref Expression
1 dfsclnbgr2.v ⊢ V = Vtx ⁡ G
2 dfsclnbgr2.s ⊢ S = n ∈ V | ∃ e ∈ E N n ⊆ e
3 dfsclnbgr2.e ⊢ E = Edg ⁡ G
4 rabdif ⊢ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∖ N = n ∈ V ∖ N | ∃ e ∈ E N ∈ e ∧ n ∈ e
5 4 eqcomi ⊢ n ∈ V ∖ N | ∃ e ∈ E N ∈ e ∧ n ∈ e = n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∖ N
6 1 3 dfnbgr2 ⊢ N ∈ V → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N ∈ e ∧ n ∈ e
7 1 2 3 dfsclnbgr2 ⊢ N ∈ V → S = n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e
8 7 difeq1d ⊢ N ∈ V → S ∖ N = n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∖ N
9 5 6 8 3eqtr4a ⊢ N ∈ V → G NeighbVtx N = S ∖ N