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

Metamath Proof Explorer

Theorem usgr1v0edg

Description: A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 18-Oct-2020)

Ref Expression
Assertion usgr1v0edg 
|- ( ( G e. W /\ ( Vtx ` G ) = { A } /\ Fun ( iEdg ` G ) ) -> ( G e. USGraph <-> ( Edg ` G ) = (/) ) )

Proof

Step Hyp Ref Expression
1 usgr1v 
 |-  ( ( G e. W /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )
2 1 3adant3 
 |-  ( ( G e. W /\ ( Vtx ` G ) = { A } /\ Fun ( iEdg ` G ) ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )
3 funrel 
 |-  ( Fun ( iEdg ` G ) -> Rel ( iEdg ` G ) )
4 relrn0 
 |-  ( Rel ( iEdg ` G ) -> ( ( iEdg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) )
5 3 4 syl 
 |-  ( Fun ( iEdg ` G ) -> ( ( iEdg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) )
6 5 3ad2ant3 
 |-  ( ( G e. W /\ ( Vtx ` G ) = { A } /\ Fun ( iEdg ` G ) ) -> ( ( iEdg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) )
7 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
8 7 eqcomi 
 |-  ran ( iEdg ` G ) = ( Edg ` G )
9 8 eqeq1i 
 |-  ( ran ( iEdg ` G ) = (/) <-> ( Edg ` G ) = (/) )
10 9 a1i 
 |-  ( ( G e. W /\ ( Vtx ` G ) = { A } /\ Fun ( iEdg ` G ) ) -> ( ran ( iEdg ` G ) = (/) <-> ( Edg ` G ) = (/) ) )
11 2 6 10 3bitrd 
 |-  ( ( G e. W /\ ( Vtx ` G ) = { A } /\ Fun ( iEdg ` G ) ) -> ( G e. USGraph <-> ( Edg ` G ) = (/) ) )