Theorem cusgr1v

Description: A graph with one vertex and no edges is a complete simple graph. (Contributed by AV, 1-Nov-2020) (Revised by AV, 23-Mar-2021)

	Ref	Expression
Hypothesis	cplgr0v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	cusgr1v	⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ComplUSGraph )

Proof

Step	Hyp	Ref	Expression
1		cplgr0v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	cplgr1vlem	⊢ ( ( ♯ ‘ 𝑉 ) = 1 → 𝐺 ∈ V )
3	2	adantr	⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ V )
4		simpr	⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ( iEdg ‘ 𝐺 ) = ∅ )
5	3 4	usgr0e	⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )
6	1	cplgr1v	⊢ ( ( ♯ ‘ 𝑉 ) = 1 → 𝐺 ∈ ComplGraph )
7	6	adantr	⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ComplGraph )
8		iscusgr	⊢ ( 𝐺 ∈ ComplUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) )
9	5 7 8	sylanbrc	⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ComplUSGraph )