Step |
Hyp |
Ref |
Expression |
1 |
|
hashge0 |
|- ( V e. W -> 0 <_ ( # ` V ) ) |
2 |
1
|
biantrud |
|- ( V e. W -> ( ( # ` V ) <_ 0 <-> ( ( # ` V ) <_ 0 /\ 0 <_ ( # ` V ) ) ) ) |
3 |
|
hashxrcl |
|- ( V e. W -> ( # ` V ) e. RR* ) |
4 |
|
0xr |
|- 0 e. RR* |
5 |
|
xrletri3 |
|- ( ( ( # ` V ) e. RR* /\ 0 e. RR* ) -> ( ( # ` V ) = 0 <-> ( ( # ` V ) <_ 0 /\ 0 <_ ( # ` V ) ) ) ) |
6 |
3 4 5
|
sylancl |
|- ( V e. W -> ( ( # ` V ) = 0 <-> ( ( # ` V ) <_ 0 /\ 0 <_ ( # ` V ) ) ) ) |
7 |
|
hasheq0 |
|- ( V e. W -> ( ( # ` V ) = 0 <-> V = (/) ) ) |
8 |
2 6 7
|
3bitr2d |
|- ( V e. W -> ( ( # ` V ) <_ 0 <-> V = (/) ) ) |