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 = x ∈ 0 1 ⟼ x 1 − x
icopnfhmeo.j ⊢ J = TopOpen ⁡ ℂ fld
Assertion icopnfhmeo ⊢ F Isom < , < 0 1 0 +∞ ∧ F ∈ J ↾ 𝑡 0 1 Homeo J ↾ 𝑡 0 +∞

Proof

Step Hyp Ref Expression
1 icopnfhmeo.f ⊢ F = x ∈ 0 1 ⟼ x 1 − x
2 icopnfhmeo.j ⊢ J = TopOpen ⁡ ℂ fld
3 1 icopnfcnv ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞ ∧ F -1 = y ∈ 0 +∞ ⟼ y 1 + y
4 3 simpli ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞
5 0re ⊢ 0 ∈ ℝ
6 1xr ⊢ 1 ∈ ℝ *
7 elico2 ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ * → x ∈ 0 1 ↔ x ∈ ℝ ∧ 0 ≤ x ∧ x < 1
8 5 6 7 mp2an ⊢ x ∈ 0 1 ↔ x ∈ ℝ ∧ 0 ≤ x ∧ x < 1
9 8 simp1bi ⊢ x ∈ 0 1 → x ∈ ℝ
10 9 ssriv ⊢ 0 1 ⊆ ℝ
11 10 sseli ⊢ z ∈ 0 1 → z ∈ ℝ
12 11 adantr ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z ∈ ℝ
13 elico2 ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ * → w ∈ 0 1 ↔ w ∈ ℝ ∧ 0 ≤ w ∧ w < 1
14 5 6 13 mp2an ⊢ w ∈ 0 1 ↔ w ∈ ℝ ∧ 0 ≤ w ∧ w < 1
15 14 simp3bi ⊢ w ∈ 0 1 → w < 1
16 10 sseli ⊢ w ∈ 0 1 → w ∈ ℝ
17 1re ⊢ 1 ∈ ℝ
18 difrp ⊢ w ∈ ℝ ∧ 1 ∈ ℝ → w < 1 ↔ 1 − w ∈ ℝ +
19 16 17 18 sylancl ⊢ w ∈ 0 1 → w < 1 ↔ 1 − w ∈ ℝ +
20 15 19 mpbid ⊢ w ∈ 0 1 → 1 − w ∈ ℝ +
21 20 rpregt0d ⊢ w ∈ 0 1 → 1 − w ∈ ℝ ∧ 0 < 1 − w
22 21 adantl ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → 1 − w ∈ ℝ ∧ 0 < 1 − w
23 16 adantl ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → w ∈ ℝ
24 elico2 ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ * → z ∈ 0 1 ↔ z ∈ ℝ ∧ 0 ≤ z ∧ z < 1
25 5 6 24 mp2an ⊢ z ∈ 0 1 ↔ z ∈ ℝ ∧ 0 ≤ z ∧ z < 1
26 25 simp3bi ⊢ z ∈ 0 1 → z < 1
27 difrp ⊢ z ∈ ℝ ∧ 1 ∈ ℝ → z < 1 ↔ 1 − z ∈ ℝ +
28 11 17 27 sylancl ⊢ z ∈ 0 1 → z < 1 ↔ 1 − z ∈ ℝ +
29 26 28 mpbid ⊢ z ∈ 0 1 → 1 − z ∈ ℝ +
30 29 adantr ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → 1 − z ∈ ℝ +
31 30 rpregt0d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → 1 − z ∈ ℝ ∧ 0 < 1 − z
32 lt2mul2div ⊢ z ∈ ℝ ∧ 1 − w ∈ ℝ ∧ 0 < 1 − w ∧ w ∈ ℝ ∧ 1 − z ∈ ℝ ∧ 0 < 1 − z → z ⁢ 1 − w < w ⁢ 1 − z ↔ z 1 − z < w 1 − w
33 12 22 23 31 32 syl22anc ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z ⁢ 1 − w < w ⁢ 1 − z ↔ z 1 − z < w 1 − w
34 12 23 remulcld ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z ⁢ w ∈ ℝ
35 12 23 34 ltsub1d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z < w ↔ z − z ⁢ w < w − z ⁢ w
36 12 recnd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z ∈ ℂ
37 1cnd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → 1 ∈ ℂ
38 23 recnd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → w ∈ ℂ
39 36 37 38 subdid ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z ⁢ 1 − w = z ⋅ 1 − z ⁢ w
40 36 mulridd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z ⋅ 1 = z
41 40 oveq1d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z ⋅ 1 − z ⁢ w = z − z ⁢ w
42 39 41 eqtrd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z ⁢ 1 − w = z − z ⁢ w
43 38 37 36 subdid ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → w ⁢ 1 − z = w ⋅ 1 − w ⁢ z
44 38 mulridd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → w ⋅ 1 = w
45 38 36 mulcomd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → w ⁢ z = z ⁢ w
46 44 45 oveq12d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → w ⋅ 1 − w ⁢ z = w − z ⁢ w
47 43 46 eqtrd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → w ⁢ 1 − z = w − z ⁢ w
48 42 47 breq12d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z ⁢ 1 − w < w ⁢ 1 − z ↔ z − z ⁢ w < w − z ⁢ w
49 35 48 bitr4d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z < w ↔ z ⁢ 1 − w < w ⁢ 1 − z
50 id ⊢ x = z → x = z
51 oveq2 ⊢ x = z → 1 − x = 1 − z
52 50 51 oveq12d ⊢ x = z → x 1 − x = z 1 − z
53 ovex ⊢ z 1 − z ∈ V
54 52 1 53 fvmpt ⊢ z ∈ 0 1 → F ⁡ z = z 1 − z
55 id ⊢ x = w → x = w
56 oveq2 ⊢ x = w → 1 − x = 1 − w
57 55 56 oveq12d ⊢ x = w → x 1 − x = w 1 − w
58 ovex ⊢ w 1 − w ∈ V
59 57 1 58 fvmpt ⊢ w ∈ 0 1 → F ⁡ w = w 1 − w
60 54 59 breqan12d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → F ⁡ z < F ⁡ w ↔ z 1 − z < w 1 − w
61 33 49 60 3bitr4d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z < w ↔ F ⁡ z < F ⁡ w
62 61 rgen2 ⊢ ∀ z ∈ 0 1 ∀ w ∈ 0 1 z < w ↔ F ⁡ z < F ⁡ w
63 df-isom ⊢ F Isom < , < 0 1 0 +∞ ↔ F : 0 1 ⟶ 1-1 onto 0 +∞ ∧ ∀ z ∈ 0 1 ∀ w ∈ 0 1 z < w ↔ F ⁡ z < F ⁡ w
64 4 62 63 mpbir2an ⊢ F 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 +∞ ⊆ ℝ * → F Isom < , < 0 1 0 +∞ ↔ F Isom ≤ , ≤ 0 1 0 +∞
72 69 70 71 mp2an ⊢ F Isom < , < 0 1 0 +∞ ↔ F Isom ≤ , ≤ 0 1 0 +∞
73 64 72 mpbi ⊢ F Isom ≤ , ≤ 0 1 0 +∞
74 isores1 ⊢ F Isom ≤ , ≤ 0 1 0 +∞ ↔ F Isom ≤ ∩ 0 1 × 0 1 , ≤ 0 1 0 +∞
75 73 74 mpbi ⊢ F Isom ≤ ∩ 0 1 × 0 1 , ≤ 0 1 0 +∞
76 isores2 ⊢ F Isom ≤ ∩ 0 1 × 0 1 , ≤ 0 1 0 +∞ ↔ F Isom ≤ ∩ 0 1 × 0 1 , ≤ ∩ 0 +∞ × 0 +∞ 0 1 0 +∞
77 75 76 mpbi ⊢ F 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 ∧ F Isom ≤ ∩ 0 1 × 0 1 , ≤ ∩ 0 +∞ × 0 +∞ 0 1 0 +∞ → F ∈ ordTop ⁡ ≤ ∩ 0 1 × 0 1 Homeo ordTop ⁡ ≤ ∩ 0 +∞ × 0 +∞
88 67 68 77 87 mp3an ⊢ F ∈ ordTop ⁡ ≤ ∩ 0 1 × 0 1 Homeo ordTop ⁡ ≤ ∩ 0 +∞ × 0 +∞
89 eqid ⊢ ordTop ⁡ ≤ = ordTop ⁡ ≤
90 2 89 xrrest2 ⊢ 0 1 ⊆ ℝ → J ↾ 𝑡 0 1 = ordTop ⁡ ≤ ↾ 𝑡 0 1
91 10 90 ax-mp ⊢ J ↾ 𝑡 0 1 = ordTop ⁡ ≤ ↾ 𝑡 0 1
92 iccssico2 ⊢ x ∈ 0 1 ∧ y ∈ 0 1 → x y ⊆ 0 1
93 69 92 ordtrestixx ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 1 = ordTop ⁡ ≤ ∩ 0 1 × 0 1
94 91 93 eqtri ⊢ J ↾ 𝑡 0 1 = ordTop ⁡ ≤ ∩ 0 1 × 0 1
95 rge0ssre ⊢ 0 +∞ ⊆ ℝ
96 2 89 xrrest2 ⊢ 0 +∞ ⊆ ℝ → J ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
97 95 96 ax-mp ⊢ J ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
98 iccssico2 ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x y ⊆ 0 +∞
99 70 98 ordtrestixx ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ ∩ 0 +∞ × 0 +∞
100 97 99 eqtri ⊢ J ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ ∩ 0 +∞ × 0 +∞
101 94 100 oveq12i ⊢ J ↾ 𝑡 0 1 Homeo J ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ ∩ 0 1 × 0 1 Homeo ordTop ⁡ ≤ ∩ 0 +∞ × 0 +∞
102 88 101 eleqtrri ⊢ F ∈ J ↾ 𝑡 0 1 Homeo J ↾ 𝑡 0 +∞
103 64 102 pm3.2i ⊢ F Isom < , < 0 1 0 +∞ ∧ F ∈ J ↾ 𝑡 0 1 Homeo J ↾ 𝑡 0 +∞