This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem predgclnbgrel

Description: If a (not necessarily proper) unordered pair containing a vertex is an edge, the other vertex is in the closed neighborhood of the first vertex. (Contributed by AV, 23-Aug-2025)

Ref Expression
Hypotheses predgclnbgrel.v ⊢ V = Vtx ⁡ G
predgclnbgrel.e ⊢ E = Edg ⁡ G
Assertion predgclnbgrel ⊢ N ∈ V ∧ X ∈ V ∧ X N ∈ E → N ∈ G ClNeighbVtx X

Proof

Step Hyp Ref Expression
1 predgclnbgrel.v ⊢ V = Vtx ⁡ G
2 predgclnbgrel.e ⊢ E = Edg ⁡ G
3 3simpa ⊢ N ∈ V ∧ X ∈ V ∧ X N ∈ E → N ∈ V ∧ X ∈ V
4 simp3 ⊢ N ∈ V ∧ X ∈ V ∧ X N ∈ E → X N ∈ E
5 sseq2 ⊢ e = X N → X N ⊆ e ↔ X N ⊆ X N
6 5 adantl ⊢ N ∈ V ∧ X ∈ V ∧ X N ∈ E ∧ e = X N → X N ⊆ e ↔ X N ⊆ X N
7 ssidd ⊢ N ∈ V ∧ X ∈ V ∧ X N ∈ E → X N ⊆ X N
8 4 6 7 rspcedvd ⊢ N ∈ V ∧ X ∈ V ∧ X N ∈ E → ∃ e ∈ E X N ⊆ e
9 8 olcd ⊢ N ∈ V ∧ X ∈ V ∧ X N ∈ E → N = X ∨ ∃ e ∈ E X N ⊆ e
10 1 2 clnbgrel ⊢ N ∈ G ClNeighbVtx X ↔ N ∈ V ∧ X ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
11 3 9 10 sylanbrc ⊢ N ∈ V ∧ X ∈ V ∧ X N ∈ E → N ∈ G ClNeighbVtx X