Metamath Proof Explorer

Theorem 0edg0rgr

Description: A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Assertion 0edg0rgr 
|- ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G RegGraph 0 )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( G e. W /\ ( iEdg ` G ) = (/) ) /\ v e. ( Vtx ` G ) ) -> v e. ( Vtx ` G ) )
2 simplr 
 |-  ( ( ( G e. W /\ ( iEdg ` G ) = (/) ) /\ v e. ( Vtx ` G ) ) -> ( iEdg ` G ) = (/) )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 3 4 vtxdg0e 
 |-  ( ( v e. ( Vtx ` G ) /\ ( iEdg ` G ) = (/) ) -> ( ( VtxDeg ` G ) ` v ) = 0 )
6 1 2 5 syl2anc 
 |-  ( ( ( G e. W /\ ( iEdg ` G ) = (/) ) /\ v e. ( Vtx ` G ) ) -> ( ( VtxDeg ` G ) ` v ) = 0 )
7 6 ralrimiva 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = 0 )
8 0xnn0 
 |-  0 e. NN0*
9 7 8 jctil 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> ( 0 e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = 0 ) )
10 8 a1i 
 |-  ( ( iEdg ` G ) = (/) -> 0 e. NN0* )
11 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
12 3 11 isrgr 
 |-  ( ( G e. W /\ 0 e. NN0* ) -> ( G RegGraph 0 <-> ( 0 e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = 0 ) ) )
13 10 12 sylan2 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> ( G RegGraph 0 <-> ( 0 e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = 0 ) ) )
14 9 13 mpbird 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G RegGraph 0 )