Theorem usgr0edg0rusgr

Description: A simple graph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018) (Revised by AV, 19-Dec-2020) (Proof shortened by AV, 24-Dec-2020)

	Ref	Expression
Assertion	usgr0edg0rusgr	|- ( G e. USGraph -> ( G RegUSGraph 0 <-> ( Edg ` G ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		0nn0	|- 0 e. NN0
2		isrusgr	|- ( ( G e. USGraph /\ 0 e. NN0 ) -> ( G RegUSGraph 0 <-> ( G e. USGraph /\ G RegGraph 0 ) ) )
3	1 2	mpan2	|- ( G e. USGraph -> ( G RegUSGraph 0 <-> ( G e. USGraph /\ G RegGraph 0 ) ) )
4		ibar	|- ( G e. USGraph -> ( G RegGraph 0 <-> ( G e. USGraph /\ G RegGraph 0 ) ) )
5		usgruhgr	|- ( G e. USGraph -> G e. UHGraph )
6		uhgr0edg0rgrb	|- ( G e. UHGraph -> ( G RegGraph 0 <-> ( Edg ` G ) = (/) ) )
7	5 6	syl	|- ( G e. USGraph -> ( G RegGraph 0 <-> ( Edg ` G ) = (/) ) )
8	3 4 7	3bitr2d	|- ( G e. USGraph -> ( G RegUSGraph 0 <-> ( Edg ` G ) = (/) ) )