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 e. V /\ X e. V /\ { X , N } e. E ) -> N e. ( G ClNeighbVtx X ) )

Proof

Step Hyp Ref Expression
1 predgclnbgrel.v 
 |-  V = ( Vtx ` G )
2 predgclnbgrel.e 
 |-  E = ( Edg ` G )
3 3simpa 
 |-  ( ( N e. V /\ X e. V /\ { X , N } e. E ) -> ( N e. V /\ X e. V ) )
4 simp3 
 |-  ( ( N e. V /\ X e. V /\ { X , N } e. E ) -> { X , N } e. E )
5 sseq2 
 |-  ( e = { X , N } -> ( { X , N } C_ e <-> { X , N } C_ { X , N } ) )
6 5 adantl 
 |-  ( ( ( N e. V /\ X e. V /\ { X , N } e. E ) /\ e = { X , N } ) -> ( { X , N } C_ e <-> { X , N } C_ { X , N } ) )
7 ssidd 
 |-  ( ( N e. V /\ X e. V /\ { X , N } e. E ) -> { X , N } C_ { X , N } )
8 4 6 7 rspcedvd 
 |-  ( ( N e. V /\ X e. V /\ { X , N } e. E ) -> E. e e. E { X , N } C_ e )
9 8 olcd 
 |-  ( ( N e. V /\ X e. V /\ { X , N } e. E ) -> ( N = X \/ E. e e. E { X , N } C_ e ) )
10 1 2 clnbgrel 
 |-  ( N e. ( G ClNeighbVtx X ) <-> ( ( N e. V /\ X e. V ) /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) )
11 3 9 10 sylanbrc 
 |-  ( ( N e. V /\ X e. V /\ { X , N } e. E ) -> N e. ( G ClNeighbVtx X ) )