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	|- V = ( Vtx ` G )
Assertion	cusgr1v	|- ( ( ( # ` V ) = 1 /\ ( iEdg ` G ) = (/) ) -> G e. ComplUSGraph )

Proof

Step	Hyp	Ref	Expression
1		cplgr0v.v	|- V = ( Vtx ` G )
2	1	cplgr1vlem	|- ( ( # ` V ) = 1 -> G e. _V )
3	2	adantr	|- ( ( ( # ` V ) = 1 /\ ( iEdg ` G ) = (/) ) -> G e. _V )
4		simpr	|- ( ( ( # ` V ) = 1 /\ ( iEdg ` G ) = (/) ) -> ( iEdg ` G ) = (/) )
5	3 4	usgr0e	|- ( ( ( # ` V ) = 1 /\ ( iEdg ` G ) = (/) ) -> G e. USGraph )
6	1	cplgr1v	|- ( ( # ` V ) = 1 -> G e. ComplGraph )
7	6	adantr	|- ( ( ( # ` V ) = 1 /\ ( iEdg ` G ) = (/) ) -> G e. ComplGraph )
8		iscusgr	|- ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
9	5 7 8	sylanbrc	|- ( ( ( # ` V ) = 1 /\ ( iEdg ` G ) = (/) ) -> G e. ComplUSGraph )