Theorem clnbgrcl

Description: If a class X has at least one element in its closed neighborhood, this class must be a vertex. (Contributed by AV, 7-May-2025)

	Ref	Expression
Hypothesis	clnbgrcl.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	clnbgrcl	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) → 𝑋 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		clnbgrcl.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		df-clnbgr	⊢ ClNeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) )
3	2	mpoxeldm	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) → ( 𝐺 ∈ V ∧ 𝑋 ∈ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) ) )
4		csbfv	⊢ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 )
5	4 1	eqtr4i	⊢ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) = 𝑉
6	5	eleq2i	⊢ ( 𝑋 ∈ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) ↔ 𝑋 ∈ 𝑉 )
7	6	biimpi	⊢ ( 𝑋 ∈ ⦋ 𝐺 / 𝑔 ⦌ ( Vtx ‘ 𝑔 ) → 𝑋 ∈ 𝑉 )
8	3 7	simpl2im	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) → 𝑋 ∈ 𝑉 )