Step |
Hyp |
Ref |
Expression |
1 |
|
eff1o2 |
|- ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) |
2 |
|
f1ocnv |
|- ( ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) -> `' ( exp |` ran log ) : ( CC \ { 0 } ) -1-1-onto-> ran log ) |
3 |
1 2
|
ax-mp |
|- `' ( exp |` ran log ) : ( CC \ { 0 } ) -1-1-onto-> ran log |
4 |
|
dflog2 |
|- log = `' ( exp |` ran log ) |
5 |
|
f1oeq1 |
|- ( log = `' ( exp |` ran log ) -> ( log : ( CC \ { 0 } ) -1-1-onto-> ran log <-> `' ( exp |` ran log ) : ( CC \ { 0 } ) -1-1-onto-> ran log ) ) |
6 |
4 5
|
ax-mp |
|- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log <-> `' ( exp |` ran log ) : ( CC \ { 0 } ) -1-1-onto-> ran log ) |
7 |
3 6
|
mpbir |
|- log : ( CC \ { 0 } ) -1-1-onto-> ran log |