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 ⊢ X ∈ G ClNeighbVtx N ∧ X ≠ N → X ∈ G NeighbVtx N

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 clnbgrcl ⊢ X ∈ G ClNeighbVtx N → N ∈ Vtx ⁡ G
3 1 dfclnbgr4 ⊢ N ∈ Vtx ⁡ G → G ClNeighbVtx N = N ∪ G NeighbVtx N
4 2 3 syl ⊢ X ∈ G ClNeighbVtx N → G ClNeighbVtx N = N ∪ G NeighbVtx N
5 4 eleq2d ⊢ X ∈ G ClNeighbVtx N → X ∈ G ClNeighbVtx N ↔ X ∈ N ∪ G NeighbVtx N
6 elun ⊢ X ∈ N ∪ G NeighbVtx N ↔ X ∈ N ∨ X ∈ G NeighbVtx N
7 elsng ⊢ X ∈ G ClNeighbVtx N → X ∈ N ↔ X = N
8 eqneqall ⊢ X = N → X ≠ N → X ∈ G NeighbVtx N
9 8 a1i ⊢ X ∈ G ClNeighbVtx N → X = N → X ≠ N → X ∈ G NeighbVtx N
10 7 9 sylbid ⊢ X ∈ G ClNeighbVtx N → X ∈ N → X ≠ N → X ∈ G NeighbVtx N
11 ax-1 ⊢ X ∈ G NeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
12 11 a1i ⊢ X ∈ G ClNeighbVtx N → X ∈ G NeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
13 10 12 jaod ⊢ X ∈ G ClNeighbVtx N → X ∈ N ∨ X ∈ G NeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
14 6 13 biimtrid ⊢ X ∈ G ClNeighbVtx N → X ∈ N ∪ G NeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
15 5 14 sylbid ⊢ X ∈ G ClNeighbVtx N → X ∈ G ClNeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
16 15 pm2.43i ⊢ X ∈ G ClNeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
17 16 imp ⊢ X ∈ G ClNeighbVtx N ∧ X ≠ N → X ∈ G NeighbVtx N