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 7 8 biimtrdi ⊢ X ∈ G ClNeighbVtx N → X ∈ N → X ≠ N → X ∈ G NeighbVtx N
10 ax1w ⊢ X ∈ G ClNeighbVtx N → X ∈ G NeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
11 9 10 jaod ⊢ X ∈ G ClNeighbVtx N → X ∈ N ∨ X ∈ G NeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
12 6 11 biimtrid ⊢ X ∈ G ClNeighbVtx N → X ∈ N ∪ G NeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
13 5 12 sylbid ⊢ X ∈ G ClNeighbVtx N → X ∈ G ClNeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
14 13 pm2.43i ⊢ X ∈ G ClNeighbVtx N → X ≠ N → X ∈ G NeighbVtx N
15 14 imp ⊢ X ∈ G ClNeighbVtx N ∧ X ≠ N → X ∈ G NeighbVtx N