Theorem elclnbgrelnbgr

Description: An element of the closed neighborhood of a vertex which is not the vertex itself is an element of the open neighborhood of the vertex. (Contributed by AV, 24-Sep-2025)

	Ref	Expression
Assertion	elclnbgrelnbgr	⊢ ( ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) ∧ 𝑋 ≠ 𝑁 ) → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2	1	clnbgrcl	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
3	1	dfclnbgr4	⊢ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
4	2 3	syl	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
5	4	eleq2d	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) ↔ 𝑋 ∈ ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
6		elun	⊢ ( 𝑋 ∈ ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) ↔ ( 𝑋 ∈ { 𝑁 } ∨ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) )
7		elsng	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ { 𝑁 } ↔ 𝑋 = 𝑁 ) )
8		eqneqall	⊢ ( 𝑋 = 𝑁 → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) )
9	7 8	biimtrdi	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ { 𝑁 } → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
10		ax1w	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
11	9 10	jaod	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( ( 𝑋 ∈ { 𝑁 } ∨ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
12	6 11	biimtrid	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
13	5 12	sylbid	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
14	13	pm2.43i	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) )
15	14	imp	⊢ ( ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) ∧ 𝑋 ≠ 𝑁 ) → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) )