| Step |
Hyp |
Ref |
Expression |
| 1 |
|
relogiso |
⊢ ( log ↾ ℝ+ ) Isom < , < ( ℝ+ , ℝ ) |
| 2 |
|
df-isom |
⊢ ( ( log ↾ ℝ+ ) Isom < , < ( ℝ+ , ℝ ) ↔ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ ∧ ∀ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ) ) |
| 3 |
1 2
|
mpbi |
⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ ∧ ∀ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ) |
| 4 |
3
|
simpri |
⊢ ∀ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) |
| 5 |
|
breq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 < 𝑦 ↔ 𝐴 < 𝑦 ) ) |
| 6 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( ( log ↾ ℝ+ ) ‘ 𝑥 ) = ( ( log ↾ ℝ+ ) ‘ 𝐴 ) ) |
| 7 |
6
|
breq1d |
⊢ ( 𝑥 = 𝐴 → ( ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ) |
| 8 |
5 7
|
bibi12d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ↔ ( 𝐴 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ) ) |
| 9 |
|
breq2 |
⊢ ( 𝑦 = 𝐵 → ( 𝐴 < 𝑦 ↔ 𝐴 < 𝐵 ) ) |
| 10 |
|
fveq2 |
⊢ ( 𝑦 = 𝐵 → ( ( log ↾ ℝ+ ) ‘ 𝑦 ) = ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ) |
| 11 |
10
|
breq2d |
⊢ ( 𝑦 = 𝐵 → ( ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ) ) |
| 12 |
9 11
|
bibi12d |
⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ↔ ( 𝐴 < 𝐵 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ) ) ) |
| 13 |
8 12
|
rspc2v |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) → ( 𝐴 < 𝐵 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ) ) ) |
| 14 |
4 13
|
mpi |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 < 𝐵 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ) ) |
| 15 |
|
fvres |
⊢ ( 𝐴 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝐴 ) = ( log ‘ 𝐴 ) ) |
| 16 |
|
fvres |
⊢ ( 𝐵 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝐵 ) = ( log ‘ 𝐵 ) ) |
| 17 |
15 16
|
breqan12d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ↔ ( log ‘ 𝐴 ) < ( log ‘ 𝐵 ) ) ) |
| 18 |
14 17
|
bitrd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 < 𝐵 ↔ ( log ‘ 𝐴 ) < ( log ‘ 𝐵 ) ) ) |