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∈01⟼x1−x
icopnfhmeo.j ⊢J=TopOpen⁡ℂfld
Assertion icopnfhmeo ⊢FIsom<,<010+∞∧F∈J↾𝑡01HomeoJ↾𝑡0+∞

Proof

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