Theorem cusgr0v

Description: A graph with no vertices and no edges is a complete simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 1-Nov-2020)

	Ref	Expression
Hypothesis	cplgr0v.v	|- V = ( Vtx ` G )
Assertion	cusgr0v	|- ( ( G e. W /\ V = (/) /\ ( iEdg ` G ) = (/) ) -> G e. ComplUSGraph )

Proof

Step	Hyp	Ref	Expression
1		cplgr0v.v	|- V = ( Vtx ` G )
2	1	eqeq1i	|- ( V = (/) <-> ( Vtx ` G ) = (/) )
3		usgr0v	|- ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) -> G e. USGraph )
4	2 3	syl3an2b	|- ( ( G e. W /\ V = (/) /\ ( iEdg ` G ) = (/) ) -> G e. USGraph )
5	1	cplgr0v	|- ( ( G e. W /\ V = (/) ) -> G e. ComplGraph )
6	5	3adant3	|- ( ( G e. W /\ V = (/) /\ ( iEdg ` G ) = (/) ) -> G e. ComplGraph )
7		iscusgr	|- ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
8	4 6 7	sylanbrc	|- ( ( G e. W /\ V = (/) /\ ( iEdg ` G ) = (/) ) -> G e. ComplUSGraph )