Theorem cplgr1vlem

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

	Ref	Expression
Hypothesis	cplgr0v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	cplgr1vlem	⊢ ( ( ♯ ‘ 𝑉 ) = 1 → 𝐺 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		cplgr0v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	fvexi	⊢ 𝑉 ∈ V
3		hash1snb	⊢ ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑛 𝑉 = { 𝑛 } ) )
4	2 3	ax-mp	⊢ ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑛 𝑉 = { 𝑛 } )
5		vsnid	⊢ 𝑛 ∈ { 𝑛 }
6		eleq2	⊢ ( 𝑉 = { 𝑛 } → ( 𝑛 ∈ 𝑉 ↔ 𝑛 ∈ { 𝑛 } ) )
7	5 6	mpbiri	⊢ ( 𝑉 = { 𝑛 } → 𝑛 ∈ 𝑉 )
8	1	1vgrex	⊢ ( 𝑛 ∈ 𝑉 → 𝐺 ∈ V )
9	7 8	syl	⊢ ( 𝑉 = { 𝑛 } → 𝐺 ∈ V )
10	9	exlimiv	⊢ ( ∃ 𝑛 𝑉 = { 𝑛 } → 𝐺 ∈ V )
11	4 10	sylbi	⊢ ( ( ♯ ‘ 𝑉 ) = 1 → 𝐺 ∈ V )