Theorem vopnbgrelself

Description: A vertex N is a member of its semiopen neighborhood iff there is a loop joining the vertex with itself. (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	vopnbgrelself	|- ( N e. V -> ( N e. U <-> E. e e. E e = { N } ) )

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		ibar	|- ( N e. V -> ( E. e e. E ( ( N =/= N /\ N e. e /\ N e. e ) \/ ( N = N /\ e = { N } ) ) <-> ( N e. V /\ E. e e. E ( ( N =/= N /\ N e. e /\ N e. e ) \/ ( N = N /\ e = { N } ) ) ) ) )
5		eqid	|- N = N
6	5	jctl	|- ( e = { N } -> ( N = N /\ e = { N } ) )
7	6	olcd	|- ( e = { N } -> ( ( N =/= N /\ N e. e /\ N e. e ) \/ ( N = N /\ e = { N } ) ) )
8		eqneqall	|- ( N = N -> ( N =/= N -> ( ( N e. e /\ N e. e ) -> e = { N } ) ) )
9	5 8	ax-mp	|- ( N =/= N -> ( ( N e. e /\ N e. e ) -> e = { N } ) )
10	9	3impib	|- ( ( N =/= N /\ N e. e /\ N e. e ) -> e = { N } )
11		simpr	|- ( ( N = N /\ e = { N } ) -> e = { N } )
12	10 11	jaoi	|- ( ( ( N =/= N /\ N e. e /\ N e. e ) \/ ( N = N /\ e = { N } ) ) -> e = { N } )
13	7 12	impbii	|- ( e = { N } <-> ( ( N =/= N /\ N e. e /\ N e. e ) \/ ( N = N /\ e = { N } ) ) )
14	13	a1i	|- ( N e. V -> ( e = { N } <-> ( ( N =/= N /\ N e. e /\ N e. e ) \/ ( N = N /\ e = { N } ) ) ) )
15	14	rexbidv	|- ( N e. V -> ( E. e e. E e = { N } <-> E. e e. E ( ( N =/= N /\ N e. e /\ N e. e ) \/ ( N = N /\ e = { N } ) ) ) )
16	1 2 3	vopnbgrel	|- ( N e. V -> ( N e. U <-> ( N e. V /\ E. e e. E ( ( N =/= N /\ N e. e /\ N e. e ) \/ ( N = N /\ e = { N } ) ) ) ) )
17	4 15 16	3bitr4rd	|- ( N e. V -> ( N e. U <-> E. e e. E e = { N } ) )