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

Metamath Proof Explorer

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 𝑋 ) → 𝑋 ∈ 𝑉 )