Metamath Proof Explorer

Theorem 0vtxrusgr

Description: A graph with no vertices and an empty edge function 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 0vtxrusgr 
|- ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) -> A. k e. NN0* G RegUSGraph k )

Proof

Step Hyp Ref Expression
1 usgr0v 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) -> G e. USGraph )
2 1 adantr 
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) /\ k e. NN0* ) -> G e. USGraph )
3 0vtxrgr 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> A. v e. NN0* G RegGraph v )
4 breq2 
 |-  ( v = k -> ( G RegGraph v <-> G RegGraph k ) )
5 4 rspccv 
 |-  ( A. v e. NN0* G RegGraph v -> ( k e. NN0* -> G RegGraph k ) )
6 3 5 syl 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( k e. NN0* -> G RegGraph k ) )
7 6 3adant3 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) -> ( k e. NN0* -> G RegGraph k ) )
8 7 imp 
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) /\ k e. NN0* ) -> G RegGraph k )
9 isrusgr 
 |-  ( ( G e. W /\ k e. NN0* ) -> ( G RegUSGraph k <-> ( G e. USGraph /\ G RegGraph k ) ) )
10 9 3ad2antl1 
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) /\ k e. NN0* ) -> ( G RegUSGraph k <-> ( G e. USGraph /\ G RegGraph k ) ) )
11 2 8 10 mpbir2and 
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) /\ k e. NN0* ) -> G RegUSGraph k )
12 11 ralrimiva 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) -> A. k e. NN0* G RegUSGraph k )