Theorem cplgr0v

Description: A null graph (with no vertices) is a complete 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	cplgr0v	|- ( ( G e. W /\ V = (/) ) -> G e. ComplGraph )

Proof

Step	Hyp	Ref	Expression
1		cplgr0v.v	|- V = ( Vtx ` G )
2		rzal	|- ( V = (/) -> A. v e. V v e. ( UnivVtx ` G ) )
3	2	adantl	|- ( ( G e. W /\ V = (/) ) -> A. v e. V v e. ( UnivVtx ` G ) )
4	1	iscplgr	|- ( G e. W -> ( G e. ComplGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )
5	4	adantr	|- ( ( G e. W /\ V = (/) ) -> ( G e. ComplGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )
6	3 5	mpbird	|- ( ( G e. W /\ V = (/) ) -> G e. ComplGraph )