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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	dfvopnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	dfvopnbgr2.u	⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
Assertion	vopnbgrelself	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ 𝑈 ↔ ∃ 𝑒 ∈ 𝐸 𝑒 = { 𝑁 } ) )

Proof

Step	Hyp	Ref	Expression
1		dfvopnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfvopnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		dfvopnbgr2.u	⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
4		ibar	⊢ ( 𝑁 ∈ 𝑉 → ( ∃ 𝑒 ∈ 𝐸 ( ( 𝑁 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) ∨ ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) ) ↔ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑁 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) ∨ ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) ) ) ) )
5		eqid	⊢ 𝑁 = 𝑁
6	5	jctl	⊢ ( 𝑒 = { 𝑁 } → ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) )
7	6	olcd	⊢ ( 𝑒 = { 𝑁 } → ( ( 𝑁 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) ∨ ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) ) )
8		eqneqall	⊢ ( 𝑁 = 𝑁 → ( 𝑁 ≠ 𝑁 → ( ( 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) → 𝑒 = { 𝑁 } ) ) )
9	5 8	ax-mp	⊢ ( 𝑁 ≠ 𝑁 → ( ( 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) → 𝑒 = { 𝑁 } ) )
10	9	3impib	⊢ ( ( 𝑁 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) → 𝑒 = { 𝑁 } )
11		simpr	⊢ ( ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) → 𝑒 = { 𝑁 } )
12	10 11	jaoi	⊢ ( ( ( 𝑁 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) ∨ ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) ) → 𝑒 = { 𝑁 } )
13	7 12	impbii	⊢ ( 𝑒 = { 𝑁 } ↔ ( ( 𝑁 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) ∨ ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) ) )
14	13	a1i	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑒 = { 𝑁 } ↔ ( ( 𝑁 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) ∨ ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) ) ) )
15	14	rexbidv	⊢ ( 𝑁 ∈ 𝑉 → ( ∃ 𝑒 ∈ 𝐸 𝑒 = { 𝑁 } ↔ ∃ 𝑒 ∈ 𝐸 ( ( 𝑁 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) ∨ ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) ) ) )
16	1 2 3	vopnbgrel	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ 𝑈 ↔ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑁 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑁 ∈ 𝑒 ) ∨ ( 𝑁 = 𝑁 ∧ 𝑒 = { 𝑁 } ) ) ) ) )
17	4 15 16	3bitr4rd	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ 𝑈 ↔ ∃ 𝑒 ∈ 𝐸 𝑒 = { 𝑁 } ) )