Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
2 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
3 |
1 2
|
uhgrvd00 |
|- ( G e. UHGraph -> ( A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = 0 -> ( Edg ` G ) = (/) ) ) |
4 |
3
|
com12 |
|- ( A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = 0 -> ( G e. UHGraph -> ( Edg ` G ) = (/) ) ) |
5 |
4
|
adantl |
|- ( ( 0 e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = 0 ) -> ( G e. UHGraph -> ( Edg ` G ) = (/) ) ) |
6 |
|
eqid |
|- ( VtxDeg ` G ) = ( VtxDeg ` G ) |
7 |
1 6
|
rgrprop |
|- ( G RegGraph 0 -> ( 0 e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = 0 ) ) |
8 |
5 7
|
syl11 |
|- ( G e. UHGraph -> ( G RegGraph 0 -> ( Edg ` G ) = (/) ) ) |
9 |
|
uhgr0edg0rgr |
|- ( ( G e. UHGraph /\ ( Edg ` G ) = (/) ) -> G RegGraph 0 ) |
10 |
9
|
ex |
|- ( G e. UHGraph -> ( ( Edg ` G ) = (/) -> G RegGraph 0 ) ) |
11 |
8 10
|
impbid |
|- ( G e. UHGraph -> ( G RegGraph 0 <-> ( Edg ` G ) = (/) ) ) |