Metamath Proof Explorer

Theorem dfsclnbgr2

Description: Alternate definition of the semiclosed neighborhood of a vertex breaking up the subset relationship of an unordered pair. Asemiclosed neighborhood S of a vertex N is the set of all vertices incident with edges which join the vertex N with a vertex. Therefore, a vertex is contained in its semiclosed neighborhood if it is connected with any vertex by an edge (see sclnbgrelself ), even only with itself (i.e., by a loop). (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 dfsclnbgr2 ⊢ N ∈ V → S = n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e

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 prssg ⊢ N ∈ V ∧ n ∈ V → N ∈ e ∧ n ∈ e ↔ N n ⊆ e
5 4 bicomd ⊢ N ∈ V ∧ n ∈ V → N n ⊆ e ↔ N ∈ e ∧ n ∈ e
6 5 rexbidv ⊢ N ∈ V ∧ n ∈ V → ∃ e ∈ E N n ⊆ e ↔ ∃ e ∈ E N ∈ e ∧ n ∈ e
7 6 rabbidva ⊢ N ∈ V → n ∈ V | ∃ e ∈ E N n ⊆ e = n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e
8 2 7 eqtrid ⊢ N ∈ V → S = n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e