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∈01⟼ifx=1+∞x1−x
iccpnfhmeo.k ⊢K=ordTop⁡≤↾𝑡0+∞
Assertion iccpnfhmeo ⊢FIsom<,<010+∞∧F∈IIHomeoK

Proof

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