Step |
Hyp |
Ref |
Expression |
1 |
|
usgruhgr |
|- ( G e. USGraph -> G e. UHGraph ) |
2 |
|
uhgr0vb |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> ( iEdg ` G ) = (/) ) ) |
3 |
1 2
|
syl5ib |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. USGraph -> ( iEdg ` G ) = (/) ) ) |
4 |
|
simpl |
|- ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G e. W ) |
5 |
|
simpr |
|- ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> ( iEdg ` G ) = (/) ) |
6 |
4 5
|
usgr0e |
|- ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G e. USGraph ) |
7 |
6
|
ex |
|- ( G e. W -> ( ( iEdg ` G ) = (/) -> G e. USGraph ) ) |
8 |
7
|
adantr |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( iEdg ` G ) = (/) -> G e. USGraph ) ) |
9 |
3 8
|
impbid |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) ) |