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

Metamath Proof Explorer

Theorem usgr0e

Description: The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Proof shortened by AV, 25-Nov-2020)

Ref Expression
Hypotheses usgr0e.g 
|- ( ph -> G e. W )
usgr0e.e 
|- ( ph -> ( iEdg ` G ) = (/) )
Assertion usgr0e 
|- ( ph -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 usgr0e.g 
 |-  ( ph -> G e. W )
2 usgr0e.e 
 |-  ( ph -> ( iEdg ` G ) = (/) )
3 2 f10d 
 |-  ( ph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
6 4 5 isusgr 
 |-  ( G e. W -> ( G e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } ) )
7 1 6 syl 
 |-  ( ph -> ( G e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } ) )
8 3 7 mpbird 
 |-  ( ph -> G e. USGraph )