Theorem vopnbgrel

Description: Characterization of a member X of the semiopen neighborhood of a vertex N in a graph G . (Contributed by AV, 16-May-2025)

	Ref	Expression
Hypotheses	dfvopnbgr2.v	|- V = ( Vtx ` G )
	dfvopnbgr2.e	|- E = ( Edg ` G )
	dfvopnbgr2.u	|- U = { n e. V | ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) }
Assertion	vopnbgrel	|- ( N e. V -> ( X e. U <-> ( X e. V /\ E. e e. E ( ( X =/= N /\ N e. e /\ X e. e ) \/ ( X = N /\ e = { X } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfvopnbgr2.v	|- V = ( Vtx ` G )
2		dfvopnbgr2.e	|- E = ( Edg ` G )
3		dfvopnbgr2.u	|- U = { n e. V | ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) }
4	1 2 3	dfvopnbgr2	|- ( N e. V -> U = { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } )
5	4	eleq2d	|- ( N e. V -> ( X e. U <-> X e. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } ) )
6		neeq1	|- ( n = X -> ( n =/= N <-> X =/= N ) )
7		eleq1	|- ( n = X -> ( n e. e <-> X e. e ) )
8	6 7	3anbi13d	|- ( n = X -> ( ( n =/= N /\ N e. e /\ n e. e ) <-> ( X =/= N /\ N e. e /\ X e. e ) ) )
9		eqeq1	|- ( n = X -> ( n = N <-> X = N ) )
10		sneq	|- ( n = X -> { n } = { X } )
11	10	eqeq2d	|- ( n = X -> ( e = { n } <-> e = { X } ) )
12	9 11	anbi12d	|- ( n = X -> ( ( n = N /\ e = { n } ) <-> ( X = N /\ e = { X } ) ) )
13	8 12	orbi12d	|- ( n = X -> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) <-> ( ( X =/= N /\ N e. e /\ X e. e ) \/ ( X = N /\ e = { X } ) ) ) )
14	13	rexbidv	|- ( n = X -> ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) <-> E. e e. E ( ( X =/= N /\ N e. e /\ X e. e ) \/ ( X = N /\ e = { X } ) ) ) )
15	14	elrab	|- ( X e. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } <-> ( X e. V /\ E. e e. E ( ( X =/= N /\ N e. e /\ X e. e ) \/ ( X = N /\ e = { X } ) ) ) )
16	5 15	bitrdi	|- ( N e. V -> ( X e. U <-> ( X e. V /\ E. e e. E ( ( X =/= N /\ N e. e /\ X e. e ) \/ ( X = N /\ e = { X } ) ) ) ) )