Theorem cplgr1vlem

Description: Lemma for cplgr1v and cusgr1v . (Contributed by AV, 23-Mar-2021)

	Ref	Expression
Hypothesis	cplgr0v.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	cplgr1vlem	$$⊢\left|V\right|=1\to G\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		cplgr0v.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	fvexi	$$⊢V\in \mathrm{V}$$
3		hash1snb	$$⊢V\in \mathrm{V}\to \left(\left|V\right|=1\leftrightarrow \exists nV=\left\{n\right\}\right)$$
4	2 3	ax-mp	$$⊢\left|V\right|=1\leftrightarrow \exists nV=\left\{n\right\}$$
5		vsnid	$$⊢n\in \left\{n\right\}$$
6		eleq2	$$⊢V=\left\{n\right\}\to \left(n\in V\leftrightarrow n\in \left\{n\right\}\right)$$
7	5 6	mpbiri	$$⊢V=\left\{n\right\}\to n\in V$$
8	1	1vgrex	$$⊢n\in V\to G\in \mathrm{V}$$
9	7 8	syl	$$⊢V=\left\{n\right\}\to G\in \mathrm{V}$$
10	9	exlimiv	$$⊢\exists nV=\left\{n\right\}\to G\in \mathrm{V}$$
11	4 10	sylbi	$$⊢\left|V\right|=1\to G\in \mathrm{V}$$