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

Proof

Step	Hyp	Ref	Expression
1		dfvopnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfvopnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		dfvopnbgr2.u	⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
4	1 2 3	dfvopnbgr2	⊢ ( 𝑁 ∈ 𝑉 → 𝑈 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } )
5	4	eleq2d	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑋 ∈ 𝑈 ↔ 𝑋 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ) )
6		neeq1	⊢ ( 𝑛 = 𝑋 → ( 𝑛 ≠ 𝑁 ↔ 𝑋 ≠ 𝑁 ) )
7		eleq1	⊢ ( 𝑛 = 𝑋 → ( 𝑛 ∈ 𝑒 ↔ 𝑋 ∈ 𝑒 ) )
8	6 7	3anbi13d	⊢ ( 𝑛 = 𝑋 → ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ ( 𝑋 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑋 ∈ 𝑒 ) ) )
9		eqeq1	⊢ ( 𝑛 = 𝑋 → ( 𝑛 = 𝑁 ↔ 𝑋 = 𝑁 ) )
10		sneq	⊢ ( 𝑛 = 𝑋 → { 𝑛 } = { 𝑋 } )
11	10	eqeq2d	⊢ ( 𝑛 = 𝑋 → ( 𝑒 = { 𝑛 } ↔ 𝑒 = { 𝑋 } ) )
12	9 11	anbi12d	⊢ ( 𝑛 = 𝑋 → ( ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ↔ ( 𝑋 = 𝑁 ∧ 𝑒 = { 𝑋 } ) ) )
13	8 12	orbi12d	⊢ ( 𝑛 = 𝑋 → ( ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) ↔ ( ( 𝑋 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑋 ∈ 𝑒 ) ∨ ( 𝑋 = 𝑁 ∧ 𝑒 = { 𝑋 } ) ) ) )
14	13	rexbidv	⊢ ( 𝑛 = 𝑋 → ( ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( 𝑋 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑋 ∈ 𝑒 ) ∨ ( 𝑋 = 𝑁 ∧ 𝑒 = { 𝑋 } ) ) ) )
15	14	elrab	⊢ ( 𝑋 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑋 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑋 ∈ 𝑒 ) ∨ ( 𝑋 = 𝑁 ∧ 𝑒 = { 𝑋 } ) ) ) )
16	5 15	bitrdi	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑋 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑋 ∈ 𝑒 ) ∨ ( 𝑋 = 𝑁 ∧ 𝑒 = { 𝑋 } ) ) ) ) )