Metamath Proof Explorer

Theorem clnbgr0edg

Description: In an empty graph (with no edges), all closed neighborhoods consists of a single vertex. (Contributed by AV, 10-May-2025)

Ref Expression
Assertion clnbgr0edg ⊢ Edg ⁡ G = ∅ ∧ K ∈ Vtx ⁡ G → G ClNeighbVtx K = K

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 dfclnbgr4 ⊢ K ∈ Vtx ⁡ G → G ClNeighbVtx K = K ∪ G NeighbVtx K
3 2 adantl ⊢ Edg ⁡ G = ∅ ∧ K ∈ Vtx ⁡ G → G ClNeighbVtx K = K ∪ G NeighbVtx K
4 nbgr0edg ⊢ Edg ⁡ G = ∅ → G NeighbVtx K = ∅
5 4 adantr ⊢ Edg ⁡ G = ∅ ∧ K ∈ Vtx ⁡ G → G NeighbVtx K = ∅
6 5 uneq2d ⊢ Edg ⁡ G = ∅ ∧ K ∈ Vtx ⁡ G → K ∪ G NeighbVtx K = K ∪ ∅
7 un0 ⊢ K ∪ ∅ = K
8 7 a1i ⊢ Edg ⁡ G = ∅ ∧ K ∈ Vtx ⁡ G → K ∪ ∅ = K
9 3 6 8 3eqtrd ⊢ Edg ⁡ G = ∅ ∧ K ∈ Vtx ⁡ G → G ClNeighbVtx K = K