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