| Step | Hyp | Ref
| Expression |
| 1 | | letsr 18638 |
. . . 4
⊢ ≤
∈ TosetRel |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ≤ ∈ TosetRel
) |
| 3 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → 𝑥 ∈
ℝ*) |
| 4 | | xrmulc1cn.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → 𝐶 ∈
ℝ+) |
| 6 | 5 | rpxrd 13078 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → 𝐶 ∈
ℝ*) |
| 7 | 3, 6 | xmulcld 13344 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (𝑥 ·e 𝐶) ∈
ℝ*) |
| 8 | 7 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ* (𝑥 ·e 𝐶) ∈
ℝ*) |
| 9 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝑦 ∈
ℝ*) |
| 10 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐶 ∈
ℝ+) |
| 11 | 10 | rpred 13077 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐶 ∈
ℝ) |
| 12 | 10 | rpne0d 13082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐶 ≠ 0) |
| 13 | | xreceu 32904 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ*
∧ 𝐶 ∈ ℝ
∧ 𝐶 ≠ 0) →
∃!𝑥 ∈
ℝ* (𝐶
·e 𝑥) =
𝑦) |
| 14 | 9, 11, 12, 13 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) →
∃!𝑥 ∈
ℝ* (𝐶
·e 𝑥) =
𝑦) |
| 15 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥 ·e 𝐶) ↔ (𝑥 ·e 𝐶) = 𝑦) |
| 16 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ 𝑥 ∈
ℝ*) |
| 17 | 6 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ 𝐶 ∈
ℝ*) |
| 18 | | xmulcom 13308 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝑥 ·e 𝐶) = (𝐶 ·e 𝑥)) |
| 19 | 16, 17, 18 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ (𝑥
·e 𝐶) =
(𝐶 ·e
𝑥)) |
| 20 | 19 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ ((𝑥
·e 𝐶) =
𝑦 ↔ (𝐶 ·e 𝑥) = 𝑦)) |
| 21 | 15, 20 | bitrid 283 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ (𝑦 = (𝑥 ·e 𝐶) ↔ (𝐶 ·e 𝑥) = 𝑦)) |
| 22 | 21 | reubidva 3396 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) →
(∃!𝑥 ∈
ℝ* 𝑦 =
(𝑥 ·e
𝐶) ↔ ∃!𝑥 ∈ ℝ*
(𝐶 ·e
𝑥) = 𝑦)) |
| 23 | 14, 22 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) →
∃!𝑥 ∈
ℝ* 𝑦 =
(𝑥 ·e
𝐶)) |
| 24 | 23 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ ℝ* ∃!𝑥 ∈ ℝ*
𝑦 = (𝑥 ·e 𝐶)) |
| 25 | | xrmulc1cn.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) |
| 26 | 25 | f1ompt 7131 |
. . . . 5
⊢ (𝐹:ℝ*–1-1-onto→ℝ* ↔ (∀𝑥 ∈ ℝ*
(𝑥 ·e
𝐶) ∈
ℝ* ∧ ∀𝑦 ∈ ℝ* ∃!𝑥 ∈ ℝ*
𝑦 = (𝑥 ·e 𝐶))) |
| 27 | 8, 24, 26 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → 𝐹:ℝ*–1-1-onto→ℝ*) |
| 28 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ 𝑥 ∈
ℝ*) |
| 29 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ 𝑦 ∈
ℝ*) |
| 30 | 4 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ 𝐶 ∈
ℝ+) |
| 31 | | xlemul1 13332 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝑥 ≤ 𝑦 ↔ (𝑥 ·e 𝐶) ≤ (𝑦 ·e 𝐶))) |
| 32 | 28, 29, 30, 31 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ (𝑥 ≤ 𝑦 ↔ (𝑥 ·e 𝐶) ≤ (𝑦 ·e 𝐶))) |
| 33 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑥 ·e 𝐶) ∈ V |
| 34 | 25 | fvmpt2 7027 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ (𝑥
·e 𝐶)
∈ V) → (𝐹‘𝑥) = (𝑥 ·e 𝐶)) |
| 35 | 28, 33, 34 | sylancl 586 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ (𝐹‘𝑥) = (𝑥 ·e 𝐶)) |
| 36 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ·e 𝐶) = (𝑦 ·e 𝐶)) |
| 37 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑦 ·e 𝐶) ∈ V |
| 38 | 36, 25, 37 | fvmpt 7016 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ*
→ (𝐹‘𝑦) = (𝑦 ·e 𝐶)) |
| 39 | 38 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ (𝐹‘𝑦) = (𝑦 ·e 𝐶)) |
| 40 | 35, 39 | breq12d 5156 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ ((𝐹‘𝑥) ≤ (𝐹‘𝑦) ↔ (𝑥 ·e 𝐶) ≤ (𝑦 ·e 𝐶))) |
| 41 | 32, 40 | bitr4d 282 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ (𝑥 ≤ 𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
| 42 | 41 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) →
∀𝑦 ∈
ℝ* (𝑥 ≤
𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
| 43 | 42 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ*
(𝑥 ≤ 𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
| 44 | | df-isom 6570 |
. . . 4
⊢ (𝐹 Isom ≤ , ≤
(ℝ*, ℝ*) ↔ (𝐹:ℝ*–1-1-onto→ℝ* ∧ ∀𝑥 ∈ ℝ*
∀𝑦 ∈
ℝ* (𝑥 ≤
𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦)))) |
| 45 | 27, 43, 44 | sylanbrc 583 |
. . 3
⊢ (𝜑 → 𝐹 Isom ≤ , ≤ (ℝ*,
ℝ*)) |
| 46 | | ledm 18635 |
. . . 4
⊢
ℝ* = dom ≤ |
| 47 | 46, 46 | ordthmeolem 23809 |
. . 3
⊢ (( ≤
∈ TosetRel ∧ ≤ ∈ TosetRel ∧ 𝐹 Isom ≤ , ≤ (ℝ*,
ℝ*)) → 𝐹 ∈ ((ordTop‘ ≤ ) Cn
(ordTop‘ ≤ ))) |
| 48 | 2, 2, 45, 47 | syl3anc 1373 |
. 2
⊢ (𝜑 → 𝐹 ∈ ((ordTop‘ ≤ ) Cn
(ordTop‘ ≤ ))) |
| 49 | | xrmulc1cn.k |
. . 3
⊢ 𝐽 = (ordTop‘ ≤
) |
| 50 | 49, 49 | oveq12i 7443 |
. 2
⊢ (𝐽 Cn 𝐽) = ((ordTop‘ ≤ ) Cn (ordTop‘
≤ )) |
| 51 | 48, 50 | eleqtrrdi 2852 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽)) |