Metamath Proof Explorer

Theorem 0uhgrrusgr

Description: The null graph as hypergraph is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Assertion 0uhgrrusgr 
|- ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> A. k e. NN0* G RegUSGraph k )

Proof

Step Hyp Ref Expression
1 uhgr0vb 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> ( iEdg ` G ) = (/) ) )
2 1 biimpd 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph -> ( iEdg ` G ) = (/) ) )
3 2 ex 
 |-  ( G e. UHGraph -> ( ( Vtx ` G ) = (/) -> ( G e. UHGraph -> ( iEdg ` G ) = (/) ) ) )
4 3 pm2.43a 
 |-  ( G e. UHGraph -> ( ( Vtx ` G ) = (/) -> ( iEdg ` G ) = (/) ) )
5 4 imp 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( iEdg ` G ) = (/) )
6 0vtxrusgr 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) -> A. k e. NN0* G RegUSGraph k )
7 5 6 mpd3an3 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> A. k e. NN0* G RegUSGraph k )