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

Proof

Step	Hyp	Ref	Expression
1		clnbgrel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		csbfv	$$⊢⦋G/g⦌\mathrm{Vtx}\left(g\right)=\mathrm{Vtx}\left(G\right)$$
3	1 2	eqtr4i	$$⊢V=⦋G/g⦌\mathrm{Vtx}\left(g\right)$$
4		neleq2	$$⊢V=⦋G/g⦌\mathrm{Vtx}\left(g\right)\to \left(X\notin V\leftrightarrow X\notin ⦋G/g⦌\mathrm{Vtx}\left(g\right)\right)$$
5	3 4	ax-mp	$$⊢X\notin V\leftrightarrow X\notin ⦋G/g⦌\mathrm{Vtx}\left(g\right)$$
6	5	biimpi	$$⊢X\notin V\to X\notin ⦋G/g⦌\mathrm{Vtx}\left(g\right)$$
7	6	olcd	$$⊢X\notin V\to \left(G\notin \mathrm{V}\vee X\notin ⦋G/g⦌\mathrm{Vtx}\left(g\right)\right)$$
8		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 |-
9	8	mpoxneldm	Could not format ( ( G e/ _V \/ X e/ [_ G / g ]_ ( Vtx ` g ) ) -> ( G ClNeighbVtx X ) = (/) ) : No typesetting found for |- ( ( G e/ _V \/ X e/ [_ G / g ]_ ( Vtx ` g ) ) -> ( G ClNeighbVtx X ) = (/) ) with typecode |-
10	7 9	syl	Could not format ( X e/ V -> ( G ClNeighbVtx X ) = (/) ) : No typesetting found for |- ( X e/ V -> ( G ClNeighbVtx X ) = (/) ) with typecode |-