# 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 ${⊢}{F}=\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)$
icopnfhmeo.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
Assertion icopnfhmeo ${⊢}\left({F}{Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)\wedge {F}\in \left(\left({J}{↾}_{𝑡}\left[0,1\right)\right)\mathrm{Homeo}\left({J}{↾}_{𝑡}\left[0,\mathrm{+\infty }\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 icopnfhmeo.f ${⊢}{F}=\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)$
2 icopnfhmeo.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
3 1 icopnfcnv ${⊢}\left({F}:\left[0,1\right)\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\wedge {{F}}^{-1}=\left({y}\in \left[0,\mathrm{+\infty }\right)⟼\frac{{y}}{1+{y}}\right)\right)$
4 3 simpli ${⊢}{F}:\left[0,1\right)\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)$
5 0re ${⊢}0\in ℝ$
6 1xr ${⊢}1\in {ℝ}^{*}$
7 elico2 ${⊢}\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)\to \left({x}\in \left[0,1\right)↔\left({x}\in ℝ\wedge 0\le {x}\wedge {x}<1\right)\right)$
8 5 6 7 mp2an ${⊢}{x}\in \left[0,1\right)↔\left({x}\in ℝ\wedge 0\le {x}\wedge {x}<1\right)$
9 8 simp1bi ${⊢}{x}\in \left[0,1\right)\to {x}\in ℝ$
10 9 ssriv ${⊢}\left[0,1\right)\subseteq ℝ$
11 10 sseli ${⊢}{z}\in \left[0,1\right)\to {z}\in ℝ$
12 11 adantr ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {z}\in ℝ$
13 elico2 ${⊢}\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)\to \left({w}\in \left[0,1\right)↔\left({w}\in ℝ\wedge 0\le {w}\wedge {w}<1\right)\right)$
14 5 6 13 mp2an ${⊢}{w}\in \left[0,1\right)↔\left({w}\in ℝ\wedge 0\le {w}\wedge {w}<1\right)$
15 14 simp3bi ${⊢}{w}\in \left[0,1\right)\to {w}<1$
16 10 sseli ${⊢}{w}\in \left[0,1\right)\to {w}\in ℝ$
17 1re ${⊢}1\in ℝ$
18 difrp ${⊢}\left({w}\in ℝ\wedge 1\in ℝ\right)\to \left({w}<1↔1-{w}\in {ℝ}^{+}\right)$
19 16 17 18 sylancl ${⊢}{w}\in \left[0,1\right)\to \left({w}<1↔1-{w}\in {ℝ}^{+}\right)$
20 15 19 mpbid ${⊢}{w}\in \left[0,1\right)\to 1-{w}\in {ℝ}^{+}$
21 20 rpregt0d ${⊢}{w}\in \left[0,1\right)\to \left(1-{w}\in ℝ\wedge 0<1-{w}\right)$
22 21 adantl ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to \left(1-{w}\in ℝ\wedge 0<1-{w}\right)$
23 16 adantl ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {w}\in ℝ$
24 elico2 ${⊢}\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)\to \left({z}\in \left[0,1\right)↔\left({z}\in ℝ\wedge 0\le {z}\wedge {z}<1\right)\right)$
25 5 6 24 mp2an ${⊢}{z}\in \left[0,1\right)↔\left({z}\in ℝ\wedge 0\le {z}\wedge {z}<1\right)$
26 25 simp3bi ${⊢}{z}\in \left[0,1\right)\to {z}<1$
27 difrp ${⊢}\left({z}\in ℝ\wedge 1\in ℝ\right)\to \left({z}<1↔1-{z}\in {ℝ}^{+}\right)$
28 11 17 27 sylancl ${⊢}{z}\in \left[0,1\right)\to \left({z}<1↔1-{z}\in {ℝ}^{+}\right)$
29 26 28 mpbid ${⊢}{z}\in \left[0,1\right)\to 1-{z}\in {ℝ}^{+}$
30 29 adantr ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to 1-{z}\in {ℝ}^{+}$
31 30 rpregt0d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to \left(1-{z}\in ℝ\wedge 0<1-{z}\right)$
32 lt2mul2div ${⊢}\left(\left({z}\in ℝ\wedge \left(1-{w}\in ℝ\wedge 0<1-{w}\right)\right)\wedge \left({w}\in ℝ\wedge \left(1-{z}\in ℝ\wedge 0<1-{z}\right)\right)\right)\to \left({z}\left(1-{w}\right)<{w}\left(1-{z}\right)↔\frac{{z}}{1-{z}}<\frac{{w}}{1-{w}}\right)$
33 12 22 23 31 32 syl22anc ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to \left({z}\left(1-{w}\right)<{w}\left(1-{z}\right)↔\frac{{z}}{1-{z}}<\frac{{w}}{1-{w}}\right)$
34 12 23 remulcld ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {z}{w}\in ℝ$
35 12 23 34 ltsub1d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to \left({z}<{w}↔{z}-{z}{w}<{w}-{z}{w}\right)$
36 12 recnd ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {z}\in ℂ$
37 1cnd ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to 1\in ℂ$
38 23 recnd ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {w}\in ℂ$
39 36 37 38 subdid ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {z}\left(1-{w}\right)={z}\cdot 1-{z}{w}$
40 36 mulid1d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {z}\cdot 1={z}$
41 40 oveq1d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {z}\cdot 1-{z}{w}={z}-{z}{w}$
42 39 41 eqtrd ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {z}\left(1-{w}\right)={z}-{z}{w}$
43 38 37 36 subdid ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {w}\left(1-{z}\right)={w}\cdot 1-{w}{z}$
44 38 mulid1d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {w}\cdot 1={w}$
45 38 36 mulcomd ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {w}{z}={z}{w}$
46 44 45 oveq12d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {w}\cdot 1-{w}{z}={w}-{z}{w}$
47 43 46 eqtrd ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to {w}\left(1-{z}\right)={w}-{z}{w}$
48 42 47 breq12d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to \left({z}\left(1-{w}\right)<{w}\left(1-{z}\right)↔{z}-{z}{w}<{w}-{z}{w}\right)$
49 35 48 bitr4d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to \left({z}<{w}↔{z}\left(1-{w}\right)<{w}\left(1-{z}\right)\right)$
50 id ${⊢}{x}={z}\to {x}={z}$
51 oveq2 ${⊢}{x}={z}\to 1-{x}=1-{z}$
52 50 51 oveq12d ${⊢}{x}={z}\to \frac{{x}}{1-{x}}=\frac{{z}}{1-{z}}$
53 ovex ${⊢}\frac{{z}}{1-{z}}\in \mathrm{V}$
54 52 1 53 fvmpt ${⊢}{z}\in \left[0,1\right)\to {F}\left({z}\right)=\frac{{z}}{1-{z}}$
55 id ${⊢}{x}={w}\to {x}={w}$
56 oveq2 ${⊢}{x}={w}\to 1-{x}=1-{w}$
57 55 56 oveq12d ${⊢}{x}={w}\to \frac{{x}}{1-{x}}=\frac{{w}}{1-{w}}$
58 ovex ${⊢}\frac{{w}}{1-{w}}\in \mathrm{V}$
59 57 1 58 fvmpt ${⊢}{w}\in \left[0,1\right)\to {F}\left({w}\right)=\frac{{w}}{1-{w}}$
60 54 59 breqan12d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to \left({F}\left({z}\right)<{F}\left({w}\right)↔\frac{{z}}{1-{z}}<\frac{{w}}{1-{w}}\right)$
61 33 49 60 3bitr4d ${⊢}\left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\to \left({z}<{w}↔{F}\left({z}\right)<{F}\left({w}\right)\right)$
62 61 rgen2 ${⊢}\forall {z}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\left({z}<{w}↔{F}\left({z}\right)<{F}\left({w}\right)\right)$
63 df-isom ${⊢}{F}{Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)↔\left({F}:\left[0,1\right)\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\wedge \forall {z}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\left({z}<{w}↔{F}\left({z}\right)<{F}\left({w}\right)\right)\right)$
64 4 62 63 mpbir2an ${⊢}{F}{Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)$
65 letsr ${⊢}\le \in \mathrm{TosetRel}$
66 65 elexi ${⊢}\le \in \mathrm{V}$
67 66 inex1 ${⊢}\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\in \mathrm{V}$
68 66 inex1 ${⊢}\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\in \mathrm{V}$
69 icossxr ${⊢}\left[0,1\right)\subseteq {ℝ}^{*}$
70 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
71 leiso ${⊢}\left(\left[0,1\right)\subseteq {ℝ}^{*}\wedge \left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}\right)\to \left({F}{Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)↔{F}{Isom}_{\le ,\le }\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)\right)$
72 69 70 71 mp2an ${⊢}{F}{Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)↔{F}{Isom}_{\le ,\le }\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)$
73 64 72 mpbi ${⊢}{F}{Isom}_{\le ,\le }\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)$
74 isores1 ${⊢}{F}{Isom}_{\le ,\le }\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)↔{F}{Isom}_{\le \cap \left(\left[0,1\right)×\left[0,1\right)\right),\le }\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)$
75 73 74 mpbi ${⊢}{F}{Isom}_{\le \cap \left(\left[0,1\right)×\left[0,1\right)\right),\le }\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)$
76 isores2 ${⊢}{F}{Isom}_{\le \cap \left(\left[0,1\right)×\left[0,1\right)\right),\le }\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)↔{F}{Isom}_{\le \cap \left(\left[0,1\right)×\left[0,1\right)\right),\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)$
77 75 76 mpbi ${⊢}{F}{Isom}_{\le \cap \left(\left[0,1\right)×\left[0,1\right)\right),\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)$
78 tsrps ${⊢}\le \in \mathrm{TosetRel}\to \le \in \mathrm{PosetRel}$
79 65 78 ax-mp ${⊢}\le \in \mathrm{PosetRel}$
80 ledm ${⊢}{ℝ}^{*}=\mathrm{dom}\le$
81 80 psssdm ${⊢}\left(\le \in \mathrm{PosetRel}\wedge \left[0,1\right)\subseteq {ℝ}^{*}\right)\to \mathrm{dom}\left(\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\right)=\left[0,1\right)$
82 79 69 81 mp2an ${⊢}\mathrm{dom}\left(\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\right)=\left[0,1\right)$
83 82 eqcomi ${⊢}\left[0,1\right)=\mathrm{dom}\left(\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\right)$
84 80 psssdm ${⊢}\left(\le \in \mathrm{PosetRel}\wedge \left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}\right)\to \mathrm{dom}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\right)=\left[0,\mathrm{+\infty }\right)$
85 79 70 84 mp2an ${⊢}\mathrm{dom}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\right)=\left[0,\mathrm{+\infty }\right)$
86 85 eqcomi ${⊢}\left[0,\mathrm{+\infty }\right)=\mathrm{dom}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\right)$
87 83 86 ordthmeo ${⊢}\left(\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\in \mathrm{V}\wedge \le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\in \mathrm{V}\wedge {F}{Isom}_{\le \cap \left(\left[0,1\right)×\left[0,1\right)\right),\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)\right)\to {F}\in \left(\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\right)\mathrm{Homeo}\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\right)\right)$
88 67 68 77 87 mp3an ${⊢}{F}\in \left(\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\right)\mathrm{Homeo}\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\right)\right)$
89 eqid ${⊢}\mathrm{ordTop}\left(\le \right)=\mathrm{ordTop}\left(\le \right)$
90 2 89 xrrest2 ${⊢}\left[0,1\right)\subseteq ℝ\to {J}{↾}_{𝑡}\left[0,1\right)=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,1\right)$
91 10 90 ax-mp ${⊢}{J}{↾}_{𝑡}\left[0,1\right)=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,1\right)$
92 iccssico2 ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,1\right)\right)\to \left[{x},{y}\right]\subseteq \left[0,1\right)$
93 69 92 ordtrestixx ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,1\right)=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\right)$
94 91 93 eqtri ${⊢}{J}{↾}_{𝑡}\left[0,1\right)=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\right)$
95 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
96 2 89 xrrest2 ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ\to {J}{↾}_{𝑡}\left[0,\mathrm{+\infty }\right)=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right)$
97 95 96 ax-mp ${⊢}{J}{↾}_{𝑡}\left[0,\mathrm{+\infty }\right)=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right)$
98 iccssico2 ${⊢}\left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to \left[{x},{y}\right]\subseteq \left[0,\mathrm{+\infty }\right)$
99 70 98 ordtrestixx ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right)=\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\right)$
100 97 99 eqtri ${⊢}{J}{↾}_{𝑡}\left[0,\mathrm{+\infty }\right)=\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\right)$
101 94 100 oveq12i ${⊢}\left({J}{↾}_{𝑡}\left[0,1\right)\right)\mathrm{Homeo}\left({J}{↾}_{𝑡}\left[0,\mathrm{+\infty }\right)\right)=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right)×\left[0,1\right)\right)\right)\mathrm{Homeo}\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right)×\left[0,\mathrm{+\infty }\right)\right)\right)$
102 88 101 eleqtrri ${⊢}{F}\in \left(\left({J}{↾}_{𝑡}\left[0,1\right)\right)\mathrm{Homeo}\left({J}{↾}_{𝑡}\left[0,\mathrm{+\infty }\right)\right)\right)$
103 64 102 pm3.2i ${⊢}\left({F}{Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)\wedge {F}\in \left(\left({J}{↾}_{𝑡}\left[0,1\right)\right)\mathrm{Homeo}\left({J}{↾}_{𝑡}\left[0,\mathrm{+\infty }\right)\right)\right)\right)$