Metamath Proof Explorer


Theorem icopnfhmeo

Description: The defined bijection from [ 0 , 1 ) to [ 0 , +oo ) is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses icopnfhmeo.f 𝐹 = ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) )
icopnfhmeo.j 𝐽 = ( TopOpen ‘ ℂfld )
Assertion icopnfhmeo ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ ( ( 𝐽t ( 0 [,) 1 ) ) Homeo ( 𝐽t ( 0 [,) +∞ ) ) ) )

Proof

Step Hyp Ref Expression
1 icopnfhmeo.f 𝐹 = ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) )
2 icopnfhmeo.j 𝐽 = ( TopOpen ‘ ℂfld )
3 1 icopnfcnv ( 𝐹 : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ ) ∧ 𝐹 = ( 𝑦 ∈ ( 0 [,) +∞ ) ↦ ( 𝑦 / ( 1 + 𝑦 ) ) ) )
4 3 simpli 𝐹 : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ )
5 0re 0 ∈ ℝ
6 1xr 1 ∈ ℝ*
7 elico2 ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( 𝑥 ∈ ( 0 [,) 1 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 < 1 ) ) )
8 5 6 7 mp2an ( 𝑥 ∈ ( 0 [,) 1 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 < 1 ) )
9 8 simp1bi ( 𝑥 ∈ ( 0 [,) 1 ) → 𝑥 ∈ ℝ )
10 9 ssriv ( 0 [,) 1 ) ⊆ ℝ
11 10 sseli ( 𝑧 ∈ ( 0 [,) 1 ) → 𝑧 ∈ ℝ )
12 11 adantr ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 𝑧 ∈ ℝ )
13 elico2 ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( 𝑤 ∈ ( 0 [,) 1 ) ↔ ( 𝑤 ∈ ℝ ∧ 0 ≤ 𝑤𝑤 < 1 ) ) )
14 5 6 13 mp2an ( 𝑤 ∈ ( 0 [,) 1 ) ↔ ( 𝑤 ∈ ℝ ∧ 0 ≤ 𝑤𝑤 < 1 ) )
15 14 simp3bi ( 𝑤 ∈ ( 0 [,) 1 ) → 𝑤 < 1 )
16 10 sseli ( 𝑤 ∈ ( 0 [,) 1 ) → 𝑤 ∈ ℝ )
17 1re 1 ∈ ℝ
18 difrp ( ( 𝑤 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑤 < 1 ↔ ( 1 − 𝑤 ) ∈ ℝ+ ) )
19 16 17 18 sylancl ( 𝑤 ∈ ( 0 [,) 1 ) → ( 𝑤 < 1 ↔ ( 1 − 𝑤 ) ∈ ℝ+ ) )
20 15 19 mpbid ( 𝑤 ∈ ( 0 [,) 1 ) → ( 1 − 𝑤 ) ∈ ℝ+ )
21 20 rpregt0d ( 𝑤 ∈ ( 0 [,) 1 ) → ( ( 1 − 𝑤 ) ∈ ℝ ∧ 0 < ( 1 − 𝑤 ) ) )
22 21 adantl ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 1 − 𝑤 ) ∈ ℝ ∧ 0 < ( 1 − 𝑤 ) ) )
23 16 adantl ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 𝑤 ∈ ℝ )
24 elico2 ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( 𝑧 ∈ ( 0 [,) 1 ) ↔ ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧𝑧 < 1 ) ) )
25 5 6 24 mp2an ( 𝑧 ∈ ( 0 [,) 1 ) ↔ ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧𝑧 < 1 ) )
26 25 simp3bi ( 𝑧 ∈ ( 0 [,) 1 ) → 𝑧 < 1 )
27 difrp ( ( 𝑧 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑧 < 1 ↔ ( 1 − 𝑧 ) ∈ ℝ+ ) )
28 11 17 27 sylancl ( 𝑧 ∈ ( 0 [,) 1 ) → ( 𝑧 < 1 ↔ ( 1 − 𝑧 ) ∈ ℝ+ ) )
29 26 28 mpbid ( 𝑧 ∈ ( 0 [,) 1 ) → ( 1 − 𝑧 ) ∈ ℝ+ )
30 29 adantr ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 1 − 𝑧 ) ∈ ℝ+ )
31 30 rpregt0d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 1 − 𝑧 ) ∈ ℝ ∧ 0 < ( 1 − 𝑧 ) ) )
32 lt2mul2div ( ( ( 𝑧 ∈ ℝ ∧ ( ( 1 − 𝑤 ) ∈ ℝ ∧ 0 < ( 1 − 𝑤 ) ) ) ∧ ( 𝑤 ∈ ℝ ∧ ( ( 1 − 𝑧 ) ∈ ℝ ∧ 0 < ( 1 − 𝑧 ) ) ) ) → ( ( 𝑧 · ( 1 − 𝑤 ) ) < ( 𝑤 · ( 1 − 𝑧 ) ) ↔ ( 𝑧 / ( 1 − 𝑧 ) ) < ( 𝑤 / ( 1 − 𝑤 ) ) ) )
33 12 22 23 31 32 syl22anc ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝑧 · ( 1 − 𝑤 ) ) < ( 𝑤 · ( 1 − 𝑧 ) ) ↔ ( 𝑧 / ( 1 − 𝑧 ) ) < ( 𝑤 / ( 1 − 𝑤 ) ) ) )
34 12 23 remulcld ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 · 𝑤 ) ∈ ℝ )
35 12 23 34 ltsub1d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 < 𝑤 ↔ ( 𝑧 − ( 𝑧 · 𝑤 ) ) < ( 𝑤 − ( 𝑧 · 𝑤 ) ) ) )
36 12 recnd ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 𝑧 ∈ ℂ )
37 1cnd ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 1 ∈ ℂ )
38 23 recnd ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 𝑤 ∈ ℂ )
39 36 37 38 subdid ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 · ( 1 − 𝑤 ) ) = ( ( 𝑧 · 1 ) − ( 𝑧 · 𝑤 ) ) )
40 36 mulid1d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 · 1 ) = 𝑧 )
41 40 oveq1d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝑧 · 1 ) − ( 𝑧 · 𝑤 ) ) = ( 𝑧 − ( 𝑧 · 𝑤 ) ) )
42 39 41 eqtrd ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 · ( 1 − 𝑤 ) ) = ( 𝑧 − ( 𝑧 · 𝑤 ) ) )
43 38 37 36 subdid ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑤 · ( 1 − 𝑧 ) ) = ( ( 𝑤 · 1 ) − ( 𝑤 · 𝑧 ) ) )
44 38 mulid1d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑤 · 1 ) = 𝑤 )
45 38 36 mulcomd ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑤 · 𝑧 ) = ( 𝑧 · 𝑤 ) )
46 44 45 oveq12d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝑤 · 1 ) − ( 𝑤 · 𝑧 ) ) = ( 𝑤 − ( 𝑧 · 𝑤 ) ) )
47 43 46 eqtrd ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑤 · ( 1 − 𝑧 ) ) = ( 𝑤 − ( 𝑧 · 𝑤 ) ) )
48 42 47 breq12d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝑧 · ( 1 − 𝑤 ) ) < ( 𝑤 · ( 1 − 𝑧 ) ) ↔ ( 𝑧 − ( 𝑧 · 𝑤 ) ) < ( 𝑤 − ( 𝑧 · 𝑤 ) ) ) )
49 35 48 bitr4d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 < 𝑤 ↔ ( 𝑧 · ( 1 − 𝑤 ) ) < ( 𝑤 · ( 1 − 𝑧 ) ) ) )
50 id ( 𝑥 = 𝑧𝑥 = 𝑧 )
51 oveq2 ( 𝑥 = 𝑧 → ( 1 − 𝑥 ) = ( 1 − 𝑧 ) )
52 50 51 oveq12d ( 𝑥 = 𝑧 → ( 𝑥 / ( 1 − 𝑥 ) ) = ( 𝑧 / ( 1 − 𝑧 ) ) )
53 ovex ( 𝑧 / ( 1 − 𝑧 ) ) ∈ V
54 52 1 53 fvmpt ( 𝑧 ∈ ( 0 [,) 1 ) → ( 𝐹𝑧 ) = ( 𝑧 / ( 1 − 𝑧 ) ) )
55 id ( 𝑥 = 𝑤𝑥 = 𝑤 )
56 oveq2 ( 𝑥 = 𝑤 → ( 1 − 𝑥 ) = ( 1 − 𝑤 ) )
57 55 56 oveq12d ( 𝑥 = 𝑤 → ( 𝑥 / ( 1 − 𝑥 ) ) = ( 𝑤 / ( 1 − 𝑤 ) ) )
58 ovex ( 𝑤 / ( 1 − 𝑤 ) ) ∈ V
59 57 1 58 fvmpt ( 𝑤 ∈ ( 0 [,) 1 ) → ( 𝐹𝑤 ) = ( 𝑤 / ( 1 − 𝑤 ) ) )
60 54 59 breqan12d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝐹𝑧 ) < ( 𝐹𝑤 ) ↔ ( 𝑧 / ( 1 − 𝑧 ) ) < ( 𝑤 / ( 1 − 𝑤 ) ) ) )
61 33 49 60 3bitr4d ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 < 𝑤 ↔ ( 𝐹𝑧 ) < ( 𝐹𝑤 ) ) )
62 61 rgen2 𝑧 ∈ ( 0 [,) 1 ) ∀ 𝑤 ∈ ( 0 [,) 1 ) ( 𝑧 < 𝑤 ↔ ( 𝐹𝑧 ) < ( 𝐹𝑤 ) )
63 df-isom ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ ( 𝐹 : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ ) ∧ ∀ 𝑧 ∈ ( 0 [,) 1 ) ∀ 𝑤 ∈ ( 0 [,) 1 ) ( 𝑧 < 𝑤 ↔ ( 𝐹𝑧 ) < ( 𝐹𝑤 ) ) ) )
64 4 62 63 mpbir2an 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) )
65 letsr ≤ ∈ TosetRel
66 65 elexi ≤ ∈ V
67 66 inex1 ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) ∈ V
68 66 inex1 ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ∈ V
69 icossxr ( 0 [,) 1 ) ⊆ ℝ*
70 icossxr ( 0 [,) +∞ ) ⊆ ℝ*
71 leiso ( ( ( 0 [,) 1 ) ⊆ ℝ* ∧ ( 0 [,) +∞ ) ⊆ ℝ* ) → ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ 𝐹 Isom ≤ , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ) )
72 69 70 71 mp2an ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ 𝐹 Isom ≤ , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) )
73 64 72 mpbi 𝐹 Isom ≤ , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) )
74 isores1 ( 𝐹 Isom ≤ , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) )
75 73 74 mpbi 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) )
76 isores2 ( 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) )
77 75 76 mpbi 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) )
78 tsrps ( ≤ ∈ TosetRel → ≤ ∈ PosetRel )
79 65 78 ax-mp ≤ ∈ PosetRel
80 ledm * = dom ≤
81 80 psssdm ( ( ≤ ∈ PosetRel ∧ ( 0 [,) 1 ) ⊆ ℝ* ) → dom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) = ( 0 [,) 1 ) )
82 79 69 81 mp2an dom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) = ( 0 [,) 1 )
83 82 eqcomi ( 0 [,) 1 ) = dom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) )
84 80 psssdm ( ( ≤ ∈ PosetRel ∧ ( 0 [,) +∞ ) ⊆ ℝ* ) → dom ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) = ( 0 [,) +∞ ) )
85 79 70 84 mp2an dom ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) = ( 0 [,) +∞ )
86 85 eqcomi ( 0 [,) +∞ ) = dom ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) )
87 83 86 ordthmeo ( ( ( ≤ ∩ ( ( 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 [,) +∞ ) ) ) ) ) )
88 67 68 77 87 mp3an 𝐹 ∈ ( ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) ) Homeo ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ) )
89 eqid ( ordTop ‘ ≤ ) = ( ordTop ‘ ≤ )
90 2 89 xrrest2 ( ( 0 [,) 1 ) ⊆ ℝ → ( 𝐽t ( 0 [,) 1 ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) 1 ) ) )
91 10 90 ax-mp ( 𝐽t ( 0 [,) 1 ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) 1 ) )
92 iccssico2 ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) 1 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 0 [,) 1 ) )
93 69 92 ordtrestixx ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) 1 ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) )
94 91 93 eqtri ( 𝐽t ( 0 [,) 1 ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) )
95 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
96 2 89 xrrest2 ( ( 0 [,) +∞ ) ⊆ ℝ → ( 𝐽t ( 0 [,) +∞ ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) +∞ ) ) )
97 95 96 ax-mp ( 𝐽t ( 0 [,) +∞ ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) +∞ ) )
98 iccssico2 ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 0 [,) +∞ ) )
99 70 98 ordtrestixx ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) +∞ ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) )
100 97 99 eqtri ( 𝐽t ( 0 [,) +∞ ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) )
101 94 100 oveq12i ( ( 𝐽t ( 0 [,) 1 ) ) Homeo ( 𝐽t ( 0 [,) +∞ ) ) ) = ( ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) ) Homeo ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ) )
102 88 101 eleqtrri 𝐹 ∈ ( ( 𝐽t ( 0 [,) 1 ) ) Homeo ( 𝐽t ( 0 [,) +∞ ) ) )
103 64 102 pm3.2i ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ ( ( 𝐽t ( 0 [,) 1 ) ) Homeo ( 𝐽t ( 0 [,) +∞ ) ) ) )