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 ) )