Step |
Hyp |
Ref |
Expression |
1 |
|
0nn0 |
|- 0 e. NN0 |
2 |
|
isrusgr |
|- ( ( G e. USGraph /\ 0 e. NN0 ) -> ( G RegUSGraph 0 <-> ( G e. USGraph /\ G RegGraph 0 ) ) ) |
3 |
1 2
|
mpan2 |
|- ( G e. USGraph -> ( G RegUSGraph 0 <-> ( G e. USGraph /\ G RegGraph 0 ) ) ) |
4 |
|
ibar |
|- ( G e. USGraph -> ( G RegGraph 0 <-> ( G e. USGraph /\ G RegGraph 0 ) ) ) |
5 |
|
usgruhgr |
|- ( G e. USGraph -> G e. UHGraph ) |
6 |
|
uhgr0edg0rgrb |
|- ( G e. UHGraph -> ( G RegGraph 0 <-> ( Edg ` G ) = (/) ) ) |
7 |
5 6
|
syl |
|- ( G e. USGraph -> ( G RegGraph 0 <-> ( Edg ` G ) = (/) ) ) |
8 |
3 4 7
|
3bitr2d |
|- ( G e. USGraph -> ( G RegUSGraph 0 <-> ( Edg ` G ) = (/) ) ) |