Metamath Proof Explorer


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