Step | Hyp | Ref
| Expression |
1 | | letsr 18099 |
. . . 4
⊢ ≤
∈ TosetRel |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ≤ ∈ TosetRel
) |
3 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → 𝑥 ∈
ℝ*) |
4 | | xrmulc1cn.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
5 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → 𝐶 ∈
ℝ+) |
6 | 5 | rpxrd 12629 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → 𝐶 ∈
ℝ*) |
7 | 3, 6 | xmulcld 12892 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (𝑥 ·e 𝐶) ∈
ℝ*) |
8 | 7 | ralrimiva 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ* (𝑥 ·e 𝐶) ∈
ℝ*) |
9 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝑦 ∈
ℝ*) |
10 | 4 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐶 ∈
ℝ+) |
11 | 10 | rpred 12628 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐶 ∈
ℝ) |
12 | 10 | rpne0d 12633 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) → 𝐶 ≠ 0) |
13 | | xreceu 30916 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ*
∧ 𝐶 ∈ ℝ
∧ 𝐶 ≠ 0) →
∃!𝑥 ∈
ℝ* (𝐶
·e 𝑥) =
𝑦) |
14 | 9, 11, 12, 13 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) →
∃!𝑥 ∈
ℝ* (𝐶
·e 𝑥) =
𝑦) |
15 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥 ·e 𝐶) ↔ (𝑥 ·e 𝐶) = 𝑦) |
16 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ 𝑥 ∈
ℝ*) |
17 | 6 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ 𝐶 ∈
ℝ*) |
18 | | xmulcom 12856 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝑥 ·e 𝐶) = (𝐶 ·e 𝑥)) |
19 | 16, 17, 18 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ (𝑥
·e 𝐶) =
(𝐶 ·e
𝑥)) |
20 | 19 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ ((𝑥
·e 𝐶) =
𝑦 ↔ (𝐶 ·e 𝑥) = 𝑦)) |
21 | 15, 20 | syl5bb 286 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 ∈ ℝ*)
→ (𝑦 = (𝑥 ·e 𝐶) ↔ (𝐶 ·e 𝑥) = 𝑦)) |
22 | 21 | reubidva 3300 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) →
(∃!𝑥 ∈
ℝ* 𝑦 =
(𝑥 ·e
𝐶) ↔ ∃!𝑥 ∈ ℝ*
(𝐶 ·e
𝑥) = 𝑦)) |
23 | 14, 22 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ*) →
∃!𝑥 ∈
ℝ* 𝑦 =
(𝑥 ·e
𝐶)) |
24 | 23 | ralrimiva 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ ℝ* ∃!𝑥 ∈ ℝ*
𝑦 = (𝑥 ·e 𝐶)) |
25 | | xrmulc1cn.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) |
26 | 25 | f1ompt 6928 |
. . . . 5
⊢ (𝐹:ℝ*–1-1-onto→ℝ* ↔ (∀𝑥 ∈ ℝ*
(𝑥 ·e
𝐶) ∈
ℝ* ∧ ∀𝑦 ∈ ℝ* ∃!𝑥 ∈ ℝ*
𝑦 = (𝑥 ·e 𝐶))) |
27 | 8, 24, 26 | sylanbrc 586 |
. . . 4
⊢ (𝜑 → 𝐹:ℝ*–1-1-onto→ℝ*) |
28 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ 𝑥 ∈
ℝ*) |
29 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ 𝑦 ∈
ℝ*) |
30 | 4 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ 𝐶 ∈
ℝ+) |
31 | | xlemul1 12880 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝑥 ≤ 𝑦 ↔ (𝑥 ·e 𝐶) ≤ (𝑦 ·e 𝐶))) |
32 | 28, 29, 30, 31 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ (𝑥 ≤ 𝑦 ↔ (𝑥 ·e 𝐶) ≤ (𝑦 ·e 𝐶))) |
33 | | ovex 7246 |
. . . . . . . . 9
⊢ (𝑥 ·e 𝐶) ∈ V |
34 | 25 | fvmpt2 6829 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ (𝑥
·e 𝐶)
∈ V) → (𝐹‘𝑥) = (𝑥 ·e 𝐶)) |
35 | 28, 33, 34 | sylancl 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ (𝐹‘𝑥) = (𝑥 ·e 𝐶)) |
36 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ·e 𝐶) = (𝑦 ·e 𝐶)) |
37 | | ovex 7246 |
. . . . . . . . . 10
⊢ (𝑦 ·e 𝐶) ∈ V |
38 | 36, 25, 37 | fvmpt 6818 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ*
→ (𝐹‘𝑦) = (𝑦 ·e 𝐶)) |
39 | 38 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ (𝐹‘𝑦) = (𝑦 ·e 𝐶)) |
40 | 35, 39 | breq12d 5066 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ ((𝐹‘𝑥) ≤ (𝐹‘𝑦) ↔ (𝑥 ·e 𝐶) ≤ (𝑦 ·e 𝐶))) |
41 | 32, 40 | bitr4d 285 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 ∈ ℝ*)
→ (𝑥 ≤ 𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
42 | 41 | ralrimiva 3105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) →
∀𝑦 ∈
ℝ* (𝑥 ≤
𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
43 | 42 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ*
(𝑥 ≤ 𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
44 | | df-isom 6389 |
. . . 4
⊢ (𝐹 Isom ≤ , ≤
(ℝ*, ℝ*) ↔ (𝐹:ℝ*–1-1-onto→ℝ* ∧ ∀𝑥 ∈ ℝ*
∀𝑦 ∈
ℝ* (𝑥 ≤
𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦)))) |
45 | 27, 43, 44 | sylanbrc 586 |
. . 3
⊢ (𝜑 → 𝐹 Isom ≤ , ≤ (ℝ*,
ℝ*)) |
46 | | ledm 18096 |
. . . 4
⊢
ℝ* = dom ≤ |
47 | 46, 46 | ordthmeolem 22698 |
. . 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 7225 |
. 2
⊢ (𝐽 Cn 𝐽) = ((ordTop‘ ≤ ) Cn (ordTop‘
≤ )) |
51 | 48, 50 | eleqtrrdi 2849 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽)) |