Step | Hyp | Ref
| Expression |
1 | | iccssxr 12127 |
. . . 4
⊢ (0[,]1)
⊆ ℝ* |
2 | | xrltso 11850 |
. . . 4
⊢ < Or
ℝ* |
3 | | soss 4977 |
. . . 4
⊢ ((0[,]1)
⊆ ℝ* → ( < Or ℝ* → < Or
(0[,]1))) |
4 | 1, 2, 3 | mp2 9 |
. . 3
⊢ < Or
(0[,]1) |
5 | | iccssxr 12127 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
6 | | soss 4977 |
. . . . 5
⊢
((0[,]+∞) ⊆ ℝ* → ( < Or
ℝ* → < Or (0[,]+∞))) |
7 | 5, 2, 6 | mp2 9 |
. . . 4
⊢ < Or
(0[,]+∞) |
8 | | sopo 4976 |
. . . 4
⊢ ( < Or
(0[,]+∞) → < Po (0[,]+∞)) |
9 | 7, 8 | ax-mp 5 |
. . 3
⊢ < Po
(0[,]+∞) |
10 | | iccpnfhmeo.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))) |
11 | 10 | iccpnfcnv 22551 |
. . . . 5
⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))))) |
12 | 11 | simpli 473 |
. . . 4
⊢ 𝐹:(0[,]1)–1-1-onto→(0[,]+∞) |
13 | | f1ofo 6057 |
. . . 4
⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → 𝐹:(0[,]1)–onto→(0[,]+∞)) |
14 | 12, 13 | ax-mp 5 |
. . 3
⊢ 𝐹:(0[,]1)–onto→(0[,]+∞) |
15 | | 0re 9919 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
16 | | 1re 9918 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
17 | 15, 16 | elicc2i 12110 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (0[,]1) ↔ (𝑧 ∈ ℝ ∧ 0 ≤
𝑧 ∧ 𝑧 ≤ 1)) |
18 | 17 | simp1bi 1069 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0[,]1) → 𝑧 ∈
ℝ) |
19 | 18 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑧 ∈ ℝ) |
20 | 15, 16 | elicc2i 12110 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (0[,]1) ↔ (𝑤 ∈ ℝ ∧ 0 ≤
𝑤 ∧ 𝑤 ≤ 1)) |
21 | 20 | simp1bi 1069 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (0[,]1) → 𝑤 ∈
ℝ) |
22 | 21 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑤 ∈ ℝ) |
23 | | 1red 9934 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 1 ∈ ℝ) |
24 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑧 < 𝑤) |
25 | 20 | simp3bi 1071 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (0[,]1) → 𝑤 ≤ 1) |
26 | 25 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑤 ≤ 1) |
27 | 19, 22, 23, 24, 26 | ltletrd 10076 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑧 < 1) |
28 | 19, 27 | gtned 10051 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 1 ≠ 𝑧) |
29 | 28 | necomd 2837 |
. . . . . . . 8
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑧 ≠ 1) |
30 | | ifnefalse 4048 |
. . . . . . . 8
⊢ (𝑧 ≠ 1 → if(𝑧 = 1, +∞, (𝑧 / (1 − 𝑧))) = (𝑧 / (1 − 𝑧))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → if(𝑧 = 1, +∞, (𝑧 / (1 − 𝑧))) = (𝑧 / (1 − 𝑧))) |
32 | | breq2 4587 |
. . . . . . . 8
⊢ (+∞
= if(𝑤 = 1, +∞,
(𝑤 / (1 − 𝑤))) → ((𝑧 / (1 − 𝑧)) < +∞ ↔ (𝑧 / (1 − 𝑧)) < if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤))))) |
33 | | breq2 4587 |
. . . . . . . 8
⊢ ((𝑤 / (1 − 𝑤)) = if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤))) → ((𝑧 / (1 − 𝑧)) < (𝑤 / (1 − 𝑤)) ↔ (𝑧 / (1 − 𝑧)) < if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤))))) |
34 | | resubcl 10224 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑧
∈ ℝ) → (1 − 𝑧) ∈ ℝ) |
35 | 16, 19, 34 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (1 − 𝑧) ∈ ℝ) |
36 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
37 | 19 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑧 ∈ ℂ) |
38 | | subeq0 10186 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℂ ∧ 𝑧
∈ ℂ) → ((1 − 𝑧) = 0 ↔ 1 = 𝑧)) |
39 | 38 | necon3bid 2826 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ 𝑧
∈ ℂ) → ((1 − 𝑧) ≠ 0 ↔ 1 ≠ 𝑧)) |
40 | 36, 37, 39 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → ((1 − 𝑧) ≠ 0 ↔ 1 ≠ 𝑧)) |
41 | 28, 40 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (1 − 𝑧) ≠ 0) |
42 | 19, 35, 41 | redivcld 10732 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (𝑧 / (1 − 𝑧)) ∈ ℝ) |
43 | | ltpnf 11830 |
. . . . . . . . . 10
⊢ ((𝑧 / (1 − 𝑧)) ∈ ℝ → (𝑧 / (1 − 𝑧)) < +∞) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (𝑧 / (1 − 𝑧)) < +∞) |
45 | 44 | adantr 480 |
. . . . . . . 8
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ 𝑤 = 1) → (𝑧 / (1 − 𝑧)) < +∞) |
46 | | simpl3 1059 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 𝑤 = 1) → 𝑧 < 𝑤) |
47 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) = (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) |
48 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
49 | 47, 48 | icopnfhmeo 22550 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) Isom < , < ((0[,)1),
(0[,)+∞)) ∧ (𝑥
∈ (0[,)1) ↦ (𝑥 /
(1 − 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t
(0[,)1))Homeo((TopOpen‘ℂfld) ↾t
(0[,)+∞)))) |
50 | 49 | simpli 473 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) Isom < , < ((0[,)1),
(0[,)+∞)) |
51 | 50 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 𝑤 = 1) → (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) Isom < , < ((0[,)1),
(0[,)+∞))) |
52 | | simp1 1054 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑧 ∈ (0[,]1)) |
53 | | 0xr 9965 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ* |
54 | 16 | rexri 9976 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ* |
55 | | 0le1 10430 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ≤
1 |
56 | | snunico 12170 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1)
→ ((0[,)1) ∪ {1}) = (0[,]1)) |
57 | 53, 54, 55, 56 | mp3an 1416 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0[,)1)
∪ {1}) = (0[,]1) |
58 | 52, 57 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑧 ∈ ((0[,)1) ∪ {1})) |
59 | | elun 3715 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((0[,)1) ∪ {1})
↔ (𝑧 ∈ (0[,)1)
∨ 𝑧 ∈
{1})) |
60 | 58, 59 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (𝑧 ∈ (0[,)1) ∨ 𝑧 ∈ {1})) |
61 | 60 | ord 391 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (¬ 𝑧 ∈ (0[,)1) → 𝑧 ∈ {1})) |
62 | | elsni 4142 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {1} → 𝑧 = 1) |
63 | 61, 62 | syl6 34 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (¬ 𝑧 ∈ (0[,)1) → 𝑧 = 1)) |
64 | 63 | necon1ad 2799 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (𝑧 ≠ 1 → 𝑧 ∈ (0[,)1))) |
65 | 29, 64 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑧 ∈ (0[,)1)) |
66 | 65 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 𝑤 = 1) → 𝑧 ∈ (0[,)1)) |
67 | | simp2 1055 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑤 ∈ (0[,]1)) |
68 | 67, 57 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → 𝑤 ∈ ((0[,)1) ∪ {1})) |
69 | | elun 3715 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ((0[,)1) ∪ {1})
↔ (𝑤 ∈ (0[,)1)
∨ 𝑤 ∈
{1})) |
70 | 68, 69 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (𝑤 ∈ (0[,)1) ∨ 𝑤 ∈ {1})) |
71 | 70 | ord 391 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (¬ 𝑤 ∈ (0[,)1) → 𝑤 ∈ {1})) |
72 | | elsni 4142 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ {1} → 𝑤 = 1) |
73 | 71, 72 | syl6 34 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (¬ 𝑤 ∈ (0[,)1) → 𝑤 = 1)) |
74 | 73 | con1d 138 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (¬ 𝑤 = 1 → 𝑤 ∈ (0[,)1))) |
75 | 74 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 𝑤 = 1) → 𝑤 ∈ (0[,)1)) |
76 | | isorel 6476 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) Isom < , < ((0[,)1),
(0[,)+∞)) ∧ (𝑧
∈ (0[,)1) ∧ 𝑤
∈ (0[,)1))) → (𝑧
< 𝑤 ↔ ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑧) < ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑤))) |
77 | 51, 66, 75, 76 | syl12anc 1316 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 𝑤 = 1) → (𝑧 < 𝑤 ↔ ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑧) < ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑤))) |
78 | 46, 77 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 𝑤 = 1) → ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑧) < ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑤)) |
79 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
80 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (1 − 𝑥) = (1 − 𝑧)) |
81 | 79, 80 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑥 / (1 − 𝑥)) = (𝑧 / (1 − 𝑧))) |
82 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑧 / (1 − 𝑧)) ∈ V |
83 | 81, 47, 82 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0[,)1) → ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑧) = (𝑧 / (1 − 𝑧))) |
84 | 66, 83 | syl 17 |
. . . . . . . . 9
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 𝑤 = 1) → ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑧) = (𝑧 / (1 − 𝑧))) |
85 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤) |
86 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (1 − 𝑥) = (1 − 𝑤)) |
87 | 85, 86 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝑥 / (1 − 𝑥)) = (𝑤 / (1 − 𝑤))) |
88 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑤 / (1 − 𝑤)) ∈ V |
89 | 87, 47, 88 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (0[,)1) → ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑤) = (𝑤 / (1 − 𝑤))) |
90 | 75, 89 | syl 17 |
. . . . . . . . 9
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 𝑤 = 1) → ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑤) = (𝑤 / (1 − 𝑤))) |
91 | 78, 84, 90 | 3brtr3d 4614 |
. . . . . . . 8
⊢ (((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 𝑤 = 1) → (𝑧 / (1 − 𝑧)) < (𝑤 / (1 − 𝑤))) |
92 | 32, 33, 45, 91 | ifbothda 4073 |
. . . . . . 7
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → (𝑧 / (1 − 𝑧)) < if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤)))) |
93 | 31, 92 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1) ∧ 𝑧 < 𝑤) → if(𝑧 = 1, +∞, (𝑧 / (1 − 𝑧))) < if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤)))) |
94 | 93 | 3expia 1259 |
. . . . 5
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) → (𝑧 < 𝑤 → if(𝑧 = 1, +∞, (𝑧 / (1 − 𝑧))) < if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤))))) |
95 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 = 1 ↔ 𝑧 = 1)) |
96 | 95, 81 | ifbieq2d 4061 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = if(𝑧 = 1, +∞, (𝑧 / (1 − 𝑧)))) |
97 | | pnfex 9972 |
. . . . . . . 8
⊢ +∞
∈ V |
98 | 97, 82 | ifex 4106 |
. . . . . . 7
⊢ if(𝑧 = 1, +∞, (𝑧 / (1 − 𝑧))) ∈ V |
99 | 96, 10, 98 | fvmpt 6191 |
. . . . . 6
⊢ (𝑧 ∈ (0[,]1) → (𝐹‘𝑧) = if(𝑧 = 1, +∞, (𝑧 / (1 − 𝑧)))) |
100 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑥 = 1 ↔ 𝑤 = 1)) |
101 | 100, 87 | ifbieq2d 4061 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤)))) |
102 | 97, 88 | ifex 4106 |
. . . . . . 7
⊢ if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤))) ∈ V |
103 | 101, 10, 102 | fvmpt 6191 |
. . . . . 6
⊢ (𝑤 ∈ (0[,]1) → (𝐹‘𝑤) = if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤)))) |
104 | 99, 103 | breqan12d 4599 |
. . . . 5
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) → ((𝐹‘𝑧) < (𝐹‘𝑤) ↔ if(𝑧 = 1, +∞, (𝑧 / (1 − 𝑧))) < if(𝑤 = 1, +∞, (𝑤 / (1 − 𝑤))))) |
105 | 94, 104 | sylibrd 248 |
. . . 4
⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) → (𝑧 < 𝑤 → (𝐹‘𝑧) < (𝐹‘𝑤))) |
106 | 105 | rgen2a 2960 |
. . 3
⊢
∀𝑧 ∈
(0[,]1)∀𝑤 ∈
(0[,]1)(𝑧 < 𝑤 → (𝐹‘𝑧) < (𝐹‘𝑤)) |
107 | | soisoi 6478 |
. . 3
⊢ ((( <
Or (0[,]1) ∧ < Po (0[,]+∞)) ∧ (𝐹:(0[,]1)–onto→(0[,]+∞) ∧ ∀𝑧 ∈ (0[,]1)∀𝑤 ∈ (0[,]1)(𝑧 < 𝑤 → (𝐹‘𝑧) < (𝐹‘𝑤)))) → 𝐹 Isom < , < ((0[,]1),
(0[,]+∞))) |
108 | 4, 9, 14, 106, 107 | mp4an 705 |
. 2
⊢ 𝐹 Isom < , < ((0[,]1),
(0[,]+∞)) |
109 | | letsr 17050 |
. . . . . 6
⊢ ≤
∈ TosetRel |
110 | 109 | elexi 3186 |
. . . . 5
⊢ ≤
∈ V |
111 | 110 | inex1 4727 |
. . . 4
⊢ ( ≤
∩ ((0[,]1) × (0[,]1))) ∈ V |
112 | 110 | inex1 4727 |
. . . 4
⊢ ( ≤
∩ ((0[,]+∞) × (0[,]+∞))) ∈ V |
113 | | leiso 13100 |
. . . . . . . 8
⊢ (((0[,]1)
⊆ ℝ* ∧ (0[,]+∞) ⊆ ℝ*)
→ (𝐹 Isom < , <
((0[,]1), (0[,]+∞)) ↔ 𝐹 Isom ≤ , ≤ ((0[,]1),
(0[,]+∞)))) |
114 | 1, 5, 113 | mp2an 704 |
. . . . . . 7
⊢ (𝐹 Isom < , < ((0[,]1),
(0[,]+∞)) ↔ 𝐹
Isom ≤ , ≤ ((0[,]1), (0[,]+∞))) |
115 | 108, 114 | mpbi 219 |
. . . . . 6
⊢ 𝐹 Isom ≤ , ≤ ((0[,]1),
(0[,]+∞)) |
116 | | isores1 6484 |
. . . . . 6
⊢ (𝐹 Isom ≤ , ≤ ((0[,]1),
(0[,]+∞)) ↔ 𝐹
Isom ( ≤ ∩ ((0[,]1) × (0[,]1))), ≤ ((0[,]1),
(0[,]+∞))) |
117 | 115, 116 | mpbi 219 |
. . . . 5
⊢ 𝐹 Isom ( ≤ ∩ ((0[,]1)
× (0[,]1))), ≤ ((0[,]1), (0[,]+∞)) |
118 | | isores2 6483 |
. . . . 5
⊢ (𝐹 Isom ( ≤ ∩ ((0[,]1)
× (0[,]1))), ≤ ((0[,]1), (0[,]+∞)) ↔ 𝐹 Isom ( ≤ ∩ ((0[,]1) ×
(0[,]1))), ( ≤ ∩ ((0[,]+∞) × (0[,]+∞)))((0[,]1),
(0[,]+∞))) |
119 | 117, 118 | mpbi 219 |
. . . 4
⊢ 𝐹 Isom ( ≤ ∩ ((0[,]1)
× (0[,]1))), ( ≤ ∩ ((0[,]+∞) ×
(0[,]+∞)))((0[,]1), (0[,]+∞)) |
120 | | tsrps 17044 |
. . . . . . . 8
⊢ ( ≤
∈ TosetRel → ≤ ∈ PosetRel) |
121 | 109, 120 | ax-mp 5 |
. . . . . . 7
⊢ ≤
∈ PosetRel |
122 | | ledm 17047 |
. . . . . . . 8
⊢
ℝ* = dom ≤ |
123 | 122 | psssdm 17039 |
. . . . . . 7
⊢ (( ≤
∈ PosetRel ∧ (0[,]1) ⊆ ℝ*) → dom ( ≤
∩ ((0[,]1) × (0[,]1))) = (0[,]1)) |
124 | 121, 1, 123 | mp2an 704 |
. . . . . 6
⊢ dom (
≤ ∩ ((0[,]1) × (0[,]1))) = (0[,]1) |
125 | 124 | eqcomi 2619 |
. . . . 5
⊢ (0[,]1) =
dom ( ≤ ∩ ((0[,]1) × (0[,]1))) |
126 | 122 | psssdm 17039 |
. . . . . . 7
⊢ (( ≤
∈ PosetRel ∧ (0[,]+∞) ⊆ ℝ*) → dom (
≤ ∩ ((0[,]+∞) × (0[,]+∞))) =
(0[,]+∞)) |
127 | 121, 5, 126 | mp2an 704 |
. . . . . 6
⊢ dom (
≤ ∩ ((0[,]+∞) × (0[,]+∞))) =
(0[,]+∞) |
128 | 127 | eqcomi 2619 |
. . . . 5
⊢
(0[,]+∞) = dom ( ≤ ∩ ((0[,]+∞) ×
(0[,]+∞))) |
129 | 125, 128 | ordthmeo 21415 |
. . . 4
⊢ ((( ≤
∩ ((0[,]1) × (0[,]1))) ∈ V ∧ ( ≤ ∩ ((0[,]+∞)
× (0[,]+∞))) ∈ V ∧ 𝐹 Isom ( ≤ ∩ ((0[,]1) ×
(0[,]1))), ( ≤ ∩ ((0[,]+∞) × (0[,]+∞)))((0[,]1),
(0[,]+∞))) → 𝐹
∈ ((ordTop‘( ≤ ∩ ((0[,]1) ×
(0[,]1))))Homeo(ordTop‘( ≤ ∩ ((0[,]+∞) ×
(0[,]+∞)))))) |
130 | 111, 112,
119, 129 | mp3an 1416 |
. . 3
⊢ 𝐹 ∈ ((ordTop‘( ≤
∩ ((0[,]1) × (0[,]1))))Homeo(ordTop‘( ≤ ∩
((0[,]+∞) × (0[,]+∞))))) |
131 | | dfii5 22496 |
. . . 4
⊢ II =
(ordTop‘( ≤ ∩ ((0[,]1) × (0[,]1)))) |
132 | | iccpnfhmeo.k |
. . . . 5
⊢ 𝐾 = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
133 | | ordtresticc 20837 |
. . . . 5
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) =
(ordTop‘( ≤ ∩ ((0[,]+∞) ×
(0[,]+∞)))) |
134 | 132, 133 | eqtri 2632 |
. . . 4
⊢ 𝐾 = (ordTop‘( ≤ ∩
((0[,]+∞) × (0[,]+∞)))) |
135 | 131, 134 | oveq12i 6561 |
. . 3
⊢
(IIHomeo𝐾) =
((ordTop‘( ≤ ∩ ((0[,]1) × (0[,]1))))Homeo(ordTop‘(
≤ ∩ ((0[,]+∞) × (0[,]+∞))))) |
136 | 130, 135 | eleqtrri 2687 |
. 2
⊢ 𝐹 ∈ (IIHomeo𝐾) |
137 | 108, 136 | pm3.2i 470 |
1
⊢ (𝐹 Isom < , < ((0[,]1),
(0[,]+∞)) ∧ 𝐹
∈ (IIHomeo𝐾)) |