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

Metamath Proof Explorer

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 )