Metamath Proof Explorer

Theorem 0grrusgr

Description: The null graph represented by an empty set is a k-regular simple graph for every k. (Contributed by AV, 26-Dec-2020)

Ref Expression
Assertion 0grrusgr 
|- A. k e. NN0* (/) RegUSGraph k

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 vtxval0 
 |-  ( Vtx ` (/) ) = (/)
3 iedgval0 
 |-  ( iEdg ` (/) ) = (/)
4 0vtxrusgr 
 |-  ( ( (/) e. _V /\ ( Vtx ` (/) ) = (/) /\ ( iEdg ` (/) ) = (/) ) -> A. k e. NN0* (/) RegUSGraph k )
5 1 2 3 4 mp3an 
 |-  A. k e. NN0* (/) RegUSGraph k