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