Metamath Proof Explorer

Theorem sclnbgrelself

Description: A vertex N is a member of its semiclosed neighborhood iff there is an edge joining the vertex with a vertex. (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 sclnbgrelself ⊢ N ∈ S ↔ N ∈ V ∧ ∃ e ∈ 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 1 2 3 sclnbgrel ⊢ N ∈ S ↔ N ∈ V ∧ ∃ e ∈ E N N ⊆ e
5 dfsn2 ⊢ N = N N
6 5 eqcomi ⊢ N N = N
7 6 sseq1i ⊢ N N ⊆ e ↔ N ⊆ e
8 snssg ⊢ N ∈ V → N ∈ e ↔ N ⊆ e
9 7 8 bitr4id ⊢ N ∈ V → N N ⊆ e ↔ N ∈ e
10 9 rexbidv ⊢ N ∈ V → ∃ e ∈ E N N ⊆ e ↔ ∃ e ∈ E N ∈ e
11 10 pm5.32i ⊢ N ∈ V ∧ ∃ e ∈ E N N ⊆ e ↔ N ∈ V ∧ ∃ e ∈ E N ∈ e
12 4 11 bitri ⊢ N ∈ S ↔ N ∈ V ∧ ∃ e ∈ E N ∈ e