Theorem nbgrcl

Description: If a class X has at least one neighbor, this class must be a vertex. (Contributed by AV, 6-Jun-2021) (Revised by AV, 12-Feb-2022)

	Ref	Expression
Hypothesis	nbgrcl.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	nbgrcl	$$⊢N\in \left(G\mathrm{NeighbVtx}X\right)\to X\in V$$

Proof

Step	Hyp	Ref	Expression
1		nbgrcl.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		df-nbgr	$$⊢\mathrm{NeighbVtx}=\left(g\in \mathrm{V},v\in \mathrm{Vtx}\left(g\right)⟼\left\{n\in \left(\mathrm{Vtx}\left(g\right)\setminus \left\{v\right\}\right)|\exists e\in \mathrm{Edg}\left(g\right)\left\{v,n\right\}\subseteq e\right\}\right)$$
3	2	mpoxeldm	$$⊢N\in \left(G\mathrm{NeighbVtx}X\right)\to \left(G\in \mathrm{V}\wedge X\in ⦋G/g⦌\mathrm{Vtx}\left(g\right)\right)$$
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	$$⊢N\in \left(G\mathrm{NeighbVtx}X\right)\to X\in V$$