Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> G e. UHGraph ) |
2 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
3 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
4 |
2 3
|
uhgr0v0e |
|- ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( Edg ` G ) = (/) ) |
5 |
|
uhgriedg0edg0 |
|- ( G e. UHGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) ) |
6 |
5
|
adantr |
|- ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) ) |
7 |
4 6
|
mpbid |
|- ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( iEdg ` G ) = (/) ) |
8 |
1 7
|
usgr0e |
|- ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> G e. USGraph ) |