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

Metamath Proof Explorer

Theorem usgr0vb

Description: The null graph, with no vertices, is a simple graph iff the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017) (Revised by AV, 16-Oct-2020)

Ref Expression
Assertion usgr0vb 
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )

Proof

Step Hyp Ref Expression
1 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
2 uhgr0vb 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> ( iEdg ` G ) = (/) ) )
3 1 2 imbitrid 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. USGraph -> ( iEdg ` G ) = (/) ) )
4 simpl 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G e. W )
5 simpr 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> ( iEdg ` G ) = (/) )
6 4 5 usgr0e 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G e. USGraph )
7 6 ex 
 |-  ( G e. W -> ( ( iEdg ` G ) = (/) -> G e. USGraph ) )
8 7 adantr 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( iEdg ` G ) = (/) -> G e. USGraph ) )
9 3 8 impbid 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )