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	syl6bi	|- ( 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 )