This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑁 ) )