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	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	clnbgrcl	Could not format assertion : No typesetting found for |- ( N e. ( G ClNeighbVtx X ) -> X e. V ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		clnbgrcl.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		df-clnbgr	Could not format ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) : No typesetting found for |- ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) with typecode |-
3	2	mpoxeldm	Could not format ( N e. ( G ClNeighbVtx X ) -> ( G e. _V /\ X e. [_ G / g ]_ ( Vtx ` g ) ) ) : No typesetting found for |- ( N e. ( G ClNeighbVtx X ) -> ( G e. _V /\ X e. [_ G / g ]_ ( Vtx ` g ) ) ) with typecode |-
4		csbfv	$$⊢⦋G/g⦌\mathrm{Vtx}\left(g\right)=\mathrm{Vtx}\left(G\right)$$
5	4 1	eqtr4i	$$⊢⦋G/g⦌\mathrm{Vtx}\left(g\right)=V$$
6	5	eleq2i	$$⊢X\in ⦋G/g⦌\mathrm{Vtx}\left(g\right)\leftrightarrow X\in V$$
7	6	biimpi	$$⊢X\in ⦋G/g⦌\mathrm{Vtx}\left(g\right)\to X\in V$$
8	3 7	simpl2im	Could not format ( N e. ( G ClNeighbVtx X ) -> X e. V ) : No typesetting found for |- ( N e. ( G ClNeighbVtx X ) -> X e. V ) with typecode |-