Metamath Proof Explorer

Theorem dfclnbgr2

Description: Alternate definition of the closed neighborhood of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 7-May-2025)

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

Proof

Step Hyp Ref Expression
1 clnbgrval.v ⊢ V = Vtx ⁡ G
2 clnbgrval.e ⊢ E = Edg ⁡ G
3 1 2 clnbgrval ⊢ N ∈ V → G ClNeighbVtx N = N ∪ n ∈ V | ∃ e ∈ E N n ⊆ e
4 prssg ⊢ N ∈ V ∧ n ∈ V → N ∈ e ∧ n ∈ e ↔ N n ⊆ e
5 4 elvd ⊢ N ∈ V → N ∈ e ∧ n ∈ e ↔ N n ⊆ e
6 5 bicomd ⊢ N ∈ V → N n ⊆ e ↔ N ∈ e ∧ n ∈ e
7 6 rexbidv ⊢ N ∈ V → ∃ e ∈ E N n ⊆ e ↔ ∃ e ∈ E N ∈ e ∧ n ∈ e
8 7 rabbidv ⊢ N ∈ V → n ∈ V | ∃ e ∈ E N n ⊆ e = n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e
9 8 uneq2d ⊢ N ∈ V → N ∪ n ∈ V | ∃ e ∈ E N n ⊆ e = N ∪ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e
10 3 9 eqtrd ⊢ N ∈ V → G ClNeighbVtx N = N ∪ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e