Theorem cplgr1vlem

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

	Ref	Expression
Hypothesis	cplgr0v.v	|- V = ( Vtx ` G )
Assertion	cplgr1vlem	|- ( ( # ` V ) = 1 -> G e. _V )

Proof

Step	Hyp	Ref	Expression
1		cplgr0v.v	|- V = ( Vtx ` G )
2	1	fvexi	|- V e. _V
3		hash1snb	|- ( V e. _V -> ( ( # ` V ) = 1 <-> E. n V = { n } ) )
4	2 3	ax-mp	|- ( ( # ` V ) = 1 <-> E. n V = { n } )
5		vsnid	|- n e. { n }
6		eleq2	|- ( V = { n } -> ( n e. V <-> n e. { n } ) )
7	5 6	mpbiri	|- ( V = { n } -> n e. V )
8	1	1vgrex	|- ( n e. V -> G e. _V )
9	7 8	syl	|- ( V = { n } -> G e. _V )
10	9	exlimiv	|- ( E. n V = { n } -> G e. _V )
11	4 10	sylbi	|- ( ( # ` V ) = 1 -> G e. _V )