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 𝑋 ) = ∅ )