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 ) = (/) ) )