Metamath Proof Explorer

Theorem iccpnfhmeo

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

Ref Expression
Hypotheses iccpnfhmeo.f ⊢ F = x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x
iccpnfhmeo.k ⊢ K = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
Assertion iccpnfhmeo ⊢ F Isom < , < 0 1 0 +∞ ∧ F ∈ II Homeo K

Proof

Step Hyp Ref Expression
1 iccpnfhmeo.f ⊢ F = x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x
2 iccpnfhmeo.k ⊢ K = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
3 iccssxr ⊢ 0 1 ⊆ ℝ *
4 xrltso ⊢ < Or ℝ *
5 soss ⊢ 0 1 ⊆ ℝ * → < Or ℝ * → < Or 0 1
6 3 4 5 mp2 ⊢ < Or 0 1
7 iccssxr ⊢ 0 +∞ ⊆ ℝ *
8 soss ⊢ 0 +∞ ⊆ ℝ * → < Or ℝ * → < Or 0 +∞
9 7 4 8 mp2 ⊢ < Or 0 +∞
10 sopo ⊢ < Or 0 +∞ → < Po 0 +∞
11 9 10 ax-mp ⊢ < Po 0 +∞
12 1 iccpnfcnv ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞ ∧ F -1 = y ∈ 0 +∞ ⟼ if y = +∞ 1 y 1 + y
13 12 simpli ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞
14 f1ofo ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞ → F : 0 1 ⟶ onto 0 +∞
15 13 14 ax-mp ⊢ F : 0 1 ⟶ onto 0 +∞
16 elicc01 ⊢ z ∈ 0 1 ↔ z ∈ ℝ ∧ 0 ≤ z ∧ z ≤ 1
17 16 simp1bi ⊢ z ∈ 0 1 → z ∈ ℝ
18 17 3ad2ant1 ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z ∈ ℝ
19 elicc01 ⊢ w ∈ 0 1 ↔ w ∈ ℝ ∧ 0 ≤ w ∧ w ≤ 1
20 19 simp1bi ⊢ w ∈ 0 1 → w ∈ ℝ
21 20 3ad2ant2 ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → w ∈ ℝ
22 1red ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → 1 ∈ ℝ
23 simp3 ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z < w
24 19 simp3bi ⊢ w ∈ 0 1 → w ≤ 1
25 24 3ad2ant2 ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → w ≤ 1
26 18 21 22 23 25 ltletrd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z < 1
27 18 26 gtned ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → 1 ≠ z
28 27 necomd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z ≠ 1
29 ifnefalse ⊢ z ≠ 1 → if z = 1 +∞ z 1 − z = z 1 − z
30 28 29 syl ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → if z = 1 +∞ z 1 − z = z 1 − z
31 breq2 ⊢ +∞ = if w = 1 +∞ w 1 − w → z 1 − z < +∞ ↔ z 1 − z < if w = 1 +∞ w 1 − w
32 breq2 ⊢ w 1 − w = if w = 1 +∞ w 1 − w → z 1 − z < w 1 − w ↔ z 1 − z < if w = 1 +∞ w 1 − w
33 1re ⊢ 1 ∈ ℝ
34 resubcl ⊢ 1 ∈ ℝ ∧ z ∈ ℝ → 1 − z ∈ ℝ
35 33 18 34 sylancr ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → 1 − z ∈ ℝ
36 ax-1cn ⊢ 1 ∈ ℂ
37 18 recnd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z ∈ ℂ
38 subeq0 ⊢ 1 ∈ ℂ ∧ z ∈ ℂ → 1 − z = 0 ↔ 1 = z
39 38 necon3bid ⊢ 1 ∈ ℂ ∧ z ∈ ℂ → 1 − z ≠ 0 ↔ 1 ≠ z
40 36 37 39 sylancr ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → 1 − z ≠ 0 ↔ 1 ≠ z
41 27 40 mpbird ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → 1 − z ≠ 0
42 18 35 41 redivcld ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z 1 − z ∈ ℝ
43 42 ltpnfd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z 1 − z < +∞
44 43 adantr ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ w = 1 → z 1 − z < +∞
45 simpl3 ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ ¬ w = 1 → z < w
46 eqid ⊢ x ∈ 0 1 ⟼ x 1 − x = x ∈ 0 1 ⟼ x 1 − x
47 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
48 46 47 icopnfhmeo ⊢ x ∈ 0 1 ⟼ x 1 − x Isom < , < 0 1 0 +∞ ∧ x ∈ 0 1 ⟼ x 1 − x ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 0 1 Homeo TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞
49 48 simpli ⊢ x ∈ 0 1 ⟼ x 1 − x Isom < , < 0 1 0 +∞
50 49 a1i ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ ¬ w = 1 → x ∈ 0 1 ⟼ x 1 − x Isom < , < 0 1 0 +∞
51 simp1 ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z ∈ 0 1
52 0xr ⊢ 0 ∈ ℝ *
53 1xr ⊢ 1 ∈ ℝ *
54 0le1 ⊢ 0 ≤ 1
55 snunico ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ 0 ≤ 1 → 0 1 ∪ 1 = 0 1
56 52 53 54 55 mp3an ⊢ 0 1 ∪ 1 = 0 1
57 51 56 eleqtrrdi ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z ∈ 0 1 ∪ 1
58 elun ⊢ z ∈ 0 1 ∪ 1 ↔ z ∈ 0 1 ∨ z ∈ 1
59 57 58 sylib ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z ∈ 0 1 ∨ z ∈ 1
60 59 ord ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → ¬ z ∈ 0 1 → z ∈ 1
61 elsni ⊢ z ∈ 1 → z = 1
62 60 61 syl6 ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → ¬ z ∈ 0 1 → z = 1
63 62 necon1ad ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z ≠ 1 → z ∈ 0 1
64 28 63 mpd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z ∈ 0 1
65 64 adantr ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ ¬ w = 1 → z ∈ 0 1
66 simp2 ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → w ∈ 0 1
67 66 56 eleqtrrdi ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → w ∈ 0 1 ∪ 1
68 elun ⊢ w ∈ 0 1 ∪ 1 ↔ w ∈ 0 1 ∨ w ∈ 1
69 67 68 sylib ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → w ∈ 0 1 ∨ w ∈ 1
70 69 ord ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → ¬ w ∈ 0 1 → w ∈ 1
71 elsni ⊢ w ∈ 1 → w = 1
72 70 71 syl6 ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → ¬ w ∈ 0 1 → w = 1
73 72 con1d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → ¬ w = 1 → w ∈ 0 1
74 73 imp ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ ¬ w = 1 → w ∈ 0 1
75 isorel ⊢ x ∈ 0 1 ⟼ x 1 − x Isom < , < 0 1 0 +∞ ∧ z ∈ 0 1 ∧ w ∈ 0 1 → z < w ↔ x ∈ 0 1 ⟼ x 1 − x ⁡ z < x ∈ 0 1 ⟼ x 1 − x ⁡ w
76 50 65 74 75 syl12anc ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ ¬ w = 1 → z < w ↔ x ∈ 0 1 ⟼ x 1 − x ⁡ z < x ∈ 0 1 ⟼ x 1 − x ⁡ w
77 45 76 mpbid ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ ¬ w = 1 → x ∈ 0 1 ⟼ x 1 − x ⁡ z < x ∈ 0 1 ⟼ x 1 − x ⁡ w
78 id ⊢ x = z → x = z
79 oveq2 ⊢ x = z → 1 − x = 1 − z
80 78 79 oveq12d ⊢ x = z → x 1 − x = z 1 − z
81 ovex ⊢ z 1 − z ∈ V
82 80 46 81 fvmpt ⊢ z ∈ 0 1 → x ∈ 0 1 ⟼ x 1 − x ⁡ z = z 1 − z
83 65 82 syl ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ ¬ w = 1 → x ∈ 0 1 ⟼ x 1 − x ⁡ z = z 1 − z
84 id ⊢ x = w → x = w
85 oveq2 ⊢ x = w → 1 − x = 1 − w
86 84 85 oveq12d ⊢ x = w → x 1 − x = w 1 − w
87 ovex ⊢ w 1 − w ∈ V
88 86 46 87 fvmpt ⊢ w ∈ 0 1 → x ∈ 0 1 ⟼ x 1 − x ⁡ w = w 1 − w
89 74 88 syl ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ ¬ w = 1 → x ∈ 0 1 ⟼ x 1 − x ⁡ w = w 1 − w
90 77 83 89 3brtr3d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w ∧ ¬ w = 1 → z 1 − z < w 1 − w
91 31 32 44 90 ifbothda ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → z 1 − z < if w = 1 +∞ w 1 − w
92 30 91 eqbrtrd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 ∧ z < w → if z = 1 +∞ z 1 − z < if w = 1 +∞ w 1 − w
93 92 3expia ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z < w → if z = 1 +∞ z 1 − z < if w = 1 +∞ w 1 − w
94 eqeq1 ⊢ x = z → x = 1 ↔ z = 1
95 94 80 ifbieq2d ⊢ x = z → if x = 1 +∞ x 1 − x = if z = 1 +∞ z 1 − z
96 pnfex ⊢ +∞ ∈ V
97 96 81 ifex ⊢ if z = 1 +∞ z 1 − z ∈ V
98 95 1 97 fvmpt ⊢ z ∈ 0 1 → F ⁡ z = if z = 1 +∞ z 1 − z
99 eqeq1 ⊢ x = w → x = 1 ↔ w = 1
100 99 86 ifbieq2d ⊢ x = w → if x = 1 +∞ x 1 − x = if w = 1 +∞ w 1 − w
101 96 87 ifex ⊢ if w = 1 +∞ w 1 − w ∈ V
102 100 1 101 fvmpt ⊢ w ∈ 0 1 → F ⁡ w = if w = 1 +∞ w 1 − w
103 98 102 breqan12d ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → F ⁡ z < F ⁡ w ↔ if z = 1 +∞ z 1 − z < if w = 1 +∞ w 1 − w
104 93 103 sylibrd ⊢ z ∈ 0 1 ∧ w ∈ 0 1 → z < w → F ⁡ z < F ⁡ w
105 104 rgen2 ⊢ ∀ z ∈ 0 1 ∀ w ∈ 0 1 z < w → F ⁡ z < F ⁡ w
106 soisoi ⊢ < Or 0 1 ∧ < Po 0 +∞ ∧ F : 0 1 ⟶ onto 0 +∞ ∧ ∀ z ∈ 0 1 ∀ w ∈ 0 1 z < w → F ⁡ z < F ⁡ w → F Isom < , < 0 1 0 +∞
107 6 11 15 105 106 mp4an ⊢ F Isom < , < 0 1 0 +∞
108 letsr ⊢ ≤ ∈ TosetRel
109 108 elexi ⊢ ≤ ∈ V
110 109 inex1 ⊢ ≤ ∩ 0 1 × 0 1 ∈ V
111 109 inex1 ⊢ ≤ ∩ 0 +∞ × 0 +∞ ∈ V
112 leiso ⊢ 0 1 ⊆ ℝ * ∧ 0 +∞ ⊆ ℝ * → F Isom < , < 0 1 0 +∞ ↔ F Isom ≤ , ≤ 0 1 0 +∞
113 3 7 112 mp2an ⊢ F Isom < , < 0 1 0 +∞ ↔ F Isom ≤ , ≤ 0 1 0 +∞
114 107 113 mpbi ⊢ F Isom ≤ , ≤ 0 1 0 +∞
115 isores1 ⊢ F Isom ≤ , ≤ 0 1 0 +∞ ↔ F Isom ≤ ∩ 0 1 × 0 1 , ≤ 0 1 0 +∞
116 114 115 mpbi ⊢ F Isom ≤ ∩ 0 1 × 0 1 , ≤ 0 1 0 +∞
117 isores2 ⊢ F Isom ≤ ∩ 0 1 × 0 1 , ≤ 0 1 0 +∞ ↔ F Isom ≤ ∩ 0 1 × 0 1 , ≤ ∩ 0 +∞ × 0 +∞ 0 1 0 +∞
118 116 117 mpbi ⊢ F Isom ≤ ∩ 0 1 × 0 1 , ≤ ∩ 0 +∞ × 0 +∞ 0 1 0 +∞
119 tsrps ⊢ ≤ ∈ TosetRel → ≤ ∈ PosetRel
120 108 119 ax-mp ⊢ ≤ ∈ PosetRel
121 ledm ⊢ ℝ * = dom ⁡ ≤
122 121 psssdm ⊢ ≤ ∈ PosetRel ∧ 0 1 ⊆ ℝ * → dom ⁡ ≤ ∩ 0 1 × 0 1 = 0 1
123 120 3 122 mp2an ⊢ dom ⁡ ≤ ∩ 0 1 × 0 1 = 0 1
124 123 eqcomi ⊢ 0 1 = dom ⁡ ≤ ∩ 0 1 × 0 1
125 121 psssdm ⊢ ≤ ∈ PosetRel ∧ 0 +∞ ⊆ ℝ * → dom ⁡ ≤ ∩ 0 +∞ × 0 +∞ = 0 +∞
126 120 7 125 mp2an ⊢ dom ⁡ ≤ ∩ 0 +∞ × 0 +∞ = 0 +∞
127 126 eqcomi ⊢ 0 +∞ = dom ⁡ ≤ ∩ 0 +∞ × 0 +∞
128 124 127 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 +∞
129 110 111 118 128 mp3an ⊢ F ∈ ordTop ⁡ ≤ ∩ 0 1 × 0 1 Homeo ordTop ⁡ ≤ ∩ 0 +∞ × 0 +∞
130 dfii5 ⊢ II = ordTop ⁡ ≤ ∩ 0 1 × 0 1
131 ordtresticc ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ ∩ 0 +∞ × 0 +∞
132 2 131 eqtri ⊢ K = ordTop ⁡ ≤ ∩ 0 +∞ × 0 +∞
133 130 132 oveq12i ⊢ II Homeo K = ordTop ⁡ ≤ ∩ 0 1 × 0 1 Homeo ordTop ⁡ ≤ ∩ 0 +∞ × 0 +∞
134 129 133 eleqtrri ⊢ F ∈ II Homeo K
135 107 134 pm3.2i ⊢ F Isom < , < 0 1 0 +∞ ∧ F ∈ II Homeo K