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

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 ‘ 𝐺 ) = ∅ ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ClNeighbVtx 𝐾 ) = { 𝐾 } )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 dfclnbgr4 ⊢ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( 𝐺 ClNeighbVtx 𝐾 ) = ( { 𝐾 } ∪ ( 𝐺 NeighbVtx 𝐾 ) ) )
3 2 adantl ⊢ ( ( ( Edg ‘ 𝐺 ) = ∅ ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ClNeighbVtx 𝐾 ) = ( { 𝐾 } ∪ ( 𝐺 NeighbVtx 𝐾 ) ) )
4 nbgr0edg ⊢ ( ( Edg ‘ 𝐺 ) = ∅ → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )
5 4 adantr ⊢ ( ( ( Edg ‘ 𝐺 ) = ∅ ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )
6 5 uneq2d ⊢ ( ( ( Edg ‘ 𝐺 ) = ∅ ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) → ( { 𝐾 } ∪ ( 𝐺 NeighbVtx 𝐾 ) ) = ( { 𝐾 } ∪ ∅ ) )
7 un0 ⊢ ( { 𝐾 } ∪ ∅ ) = { 𝐾 }
8 7 a1i ⊢ ( ( ( Edg ‘ 𝐺 ) = ∅ ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) → ( { 𝐾 } ∪ ∅ ) = { 𝐾 } )
9 3 6 8 3eqtrd ⊢ ( ( ( Edg ‘ 𝐺 ) = ∅ ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ClNeighbVtx 𝐾 ) = { 𝐾 } )