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	8	a1i	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 = 𝑁 → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
10	7 9	sylbid	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ { 𝑁 } → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
11		ax-1	⊢ ( 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) )
12	11	a1i	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
13	10 12	jaod	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( ( 𝑋 ∈ { 𝑁 } ∨ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
14	6 13	biimtrid	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
15	5 14	sylbid	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ) )
16	15	pm2.43i	⊢ ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) → ( 𝑋 ≠ 𝑁 → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) )
17	16	imp	⊢ ( ( 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) ∧ 𝑋 ≠ 𝑁 ) → 𝑋 ∈ ( 𝐺 NeighbVtx 𝑁 ) )