This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )