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

Metamath Proof Explorer

Theorem edg0usgr

Description: A class without edges is a simple graph. Since ran F = (/) does not generally imply Fun F , but Fun ( iEdgG ) is required for G to be a simple graph, however, this must be provided as assertion. (Contributed by AV, 18-Oct-2020)

Ref Expression
Assertion edg0usgr 
|- ( ( G e. W /\ ( Edg ` G ) = (/) /\ Fun ( iEdg ` G ) ) -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
2 1 a1i 
 |-  ( G e. W -> ( Edg ` G ) = ran ( iEdg ` G ) )
3 2 eqeq1d 
 |-  ( G e. W -> ( ( Edg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) )
4 funrel 
 |-  ( Fun ( iEdg ` G ) -> Rel ( iEdg ` G ) )
5 relrn0 
 |-  ( Rel ( iEdg ` G ) -> ( ( iEdg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) )
6 5 bicomd 
 |-  ( Rel ( iEdg ` G ) -> ( ran ( iEdg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
7 4 6 syl 
 |-  ( Fun ( iEdg ` G ) -> ( ran ( iEdg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
8 simpr 
 |-  ( ( ( iEdg ` G ) = (/) /\ G e. W ) -> G e. W )
9 simpl 
 |-  ( ( ( iEdg ` G ) = (/) /\ G e. W ) -> ( iEdg ` G ) = (/) )
10 8 9 usgr0e 
 |-  ( ( ( iEdg ` G ) = (/) /\ G e. W ) -> G e. USGraph )
11 10 ex 
 |-  ( ( iEdg ` G ) = (/) -> ( G e. W -> G e. USGraph ) )
12 7 11 biimtrdi 
 |-  ( Fun ( iEdg ` G ) -> ( ran ( iEdg ` G ) = (/) -> ( G e. W -> G e. USGraph ) ) )
13 12 com13 
 |-  ( G e. W -> ( ran ( iEdg ` G ) = (/) -> ( Fun ( iEdg ` G ) -> G e. USGraph ) ) )
14 3 13 sylbid 
 |-  ( G e. W -> ( ( Edg ` G ) = (/) -> ( Fun ( iEdg ` G ) -> G e. USGraph ) ) )
15 14 3imp 
 |-  ( ( G e. W /\ ( Edg ` G ) = (/) /\ Fun ( iEdg ` G ) ) -> G e. USGraph )