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

Metamath Proof Explorer

Theorem clnbgrnvtx0

Description: If a class X is not a vertex of a graph G , then it has an empty closed neighborhood in G . (Contributed by AV, 8-May-2025)

Ref Expression
Hypothesis clnbgrel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion clnbgrnvtx0 ( 𝑋 ∉ 𝑉 → ( 𝐺 ClNeighbVtx 𝑋 ) = ∅ )

Proof

Step Hyp Ref Expression
1 clnbgrel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 csbfv ⊢ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 )
3 1 2 eqtr4i ⊢ 𝑉 = ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 )
4 neleq2 ⊢ ( 𝑉 = ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) → ( 𝑋 ∉ 𝑉 ↔ 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) ) )
5 3 4 ax-mp ⊢ ( 𝑋 ∉ 𝑉 ↔ 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) )
6 5 biimpi ⊢ ( 𝑋 ∉ 𝑉 → 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) )
7 6 olcd ⊢ ( 𝑋 ∉ 𝑉 → ( 𝐺 ∉ V ∨ 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) ) )
8 df-clnbgr ⊢ ClNeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) )
9 8 mpoxneldm ⊢ ( ( 𝐺 ∉ V ∨ 𝑋 ∉ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) ) → ( 𝐺 ClNeighbVtx 𝑋 ) = ∅ )
10 7 9 syl ⊢ ( 𝑋 ∉ 𝑉 → ( 𝐺 ClNeighbVtx 𝑋 ) = ∅ )