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 e. ( 0 [,) 1 ) |-> ( x / ( 1 - x ) ) )
icopnfhmeo.j 
|- J = ( TopOpen ` CCfld )
Assertion icopnfhmeo 
|- ( F Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) /\ F e. ( ( J |`t ( 0 [,) 1 ) ) Homeo ( J |`t ( 0 [,) +oo ) ) ) )

Proof

Step Hyp Ref Expression
1 icopnfhmeo.f 
 |-  F = ( x e. ( 0 [,) 1 ) |-> ( x / ( 1 - x ) ) )
2 icopnfhmeo.j 
 |-  J = ( TopOpen ` CCfld )
3 1 icopnfcnv 
 |-  ( F : ( 0 [,) 1 ) -1-1-onto-> ( 0 [,) +oo ) /\ `' F = ( y e. ( 0 [,) +oo ) |-> ( y / ( 1 + y ) ) ) )
4 3 simpli 
 |-  F : ( 0 [,) 1 ) -1-1-onto-> ( 0 [,) +oo )
5 0re 
 |-  0 e. RR
6 1xr 
 |-  1 e. RR*
7 elico2 
 |-  ( ( 0 e. RR /\ 1 e. RR* ) -> ( x e. ( 0 [,) 1 ) <-> ( x e. RR /\ 0 <_ x /\ x < 1 ) ) )
8 5 6 7 mp2an 
 |-  ( x e. ( 0 [,) 1 ) <-> ( x e. RR /\ 0 <_ x /\ x < 1 ) )
9 8 simp1bi 
 |-  ( x e. ( 0 [,) 1 ) -> x e. RR )
10 9 ssriv 
 |-  ( 0 [,) 1 ) C_ RR
11 10 sseli 
 |-  ( z e. ( 0 [,) 1 ) -> z e. RR )
12 11 adantr 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> z e. RR )
13 elico2 
 |-  ( ( 0 e. RR /\ 1 e. RR* ) -> ( w e. ( 0 [,) 1 ) <-> ( w e. RR /\ 0 <_ w /\ w < 1 ) ) )
14 5 6 13 mp2an 
 |-  ( w e. ( 0 [,) 1 ) <-> ( w e. RR /\ 0 <_ w /\ w < 1 ) )
15 14 simp3bi 
 |-  ( w e. ( 0 [,) 1 ) -> w < 1 )
16 10 sseli 
 |-  ( w e. ( 0 [,) 1 ) -> w e. RR )
17 1re 
 |-  1 e. RR
18 difrp 
 |-  ( ( w e. RR /\ 1 e. RR ) -> ( w < 1 <-> ( 1 - w ) e. RR+ ) )
19 16 17 18 sylancl 
 |-  ( w e. ( 0 [,) 1 ) -> ( w < 1 <-> ( 1 - w ) e. RR+ ) )
20 15 19 mpbid 
 |-  ( w e. ( 0 [,) 1 ) -> ( 1 - w ) e. RR+ )
21 20 rpregt0d 
 |-  ( w e. ( 0 [,) 1 ) -> ( ( 1 - w ) e. RR /\ 0 < ( 1 - w ) ) )
22 21 adantl 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( ( 1 - w ) e. RR /\ 0 < ( 1 - w ) ) )
23 16 adantl 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> w e. RR )
24 elico2 
 |-  ( ( 0 e. RR /\ 1 e. RR* ) -> ( z e. ( 0 [,) 1 ) <-> ( z e. RR /\ 0 <_ z /\ z < 1 ) ) )
25 5 6 24 mp2an 
 |-  ( z e. ( 0 [,) 1 ) <-> ( z e. RR /\ 0 <_ z /\ z < 1 ) )
26 25 simp3bi 
 |-  ( z e. ( 0 [,) 1 ) -> z < 1 )
27 difrp 
 |-  ( ( z e. RR /\ 1 e. RR ) -> ( z < 1 <-> ( 1 - z ) e. RR+ ) )
28 11 17 27 sylancl 
 |-  ( z e. ( 0 [,) 1 ) -> ( z < 1 <-> ( 1 - z ) e. RR+ ) )
29 26 28 mpbid 
 |-  ( z e. ( 0 [,) 1 ) -> ( 1 - z ) e. RR+ )
30 29 adantr 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( 1 - z ) e. RR+ )
31 30 rpregt0d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( ( 1 - z ) e. RR /\ 0 < ( 1 - z ) ) )
32 lt2mul2div 
 |-  ( ( ( z e. RR /\ ( ( 1 - w ) e. RR /\ 0 < ( 1 - w ) ) ) /\ ( w e. RR /\ ( ( 1 - z ) e. RR /\ 0 < ( 1 - z ) ) ) ) -> ( ( z x. ( 1 - w ) ) < ( w x. ( 1 - z ) ) <-> ( z / ( 1 - z ) ) < ( w / ( 1 - w ) ) ) )
33 12 22 23 31 32 syl22anc 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( ( z x. ( 1 - w ) ) < ( w x. ( 1 - z ) ) <-> ( z / ( 1 - z ) ) < ( w / ( 1 - w ) ) ) )
34 12 23 remulcld 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( z x. w ) e. RR )
35 12 23 34 ltsub1d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( z < w <-> ( z - ( z x. w ) ) < ( w - ( z x. w ) ) ) )
36 12 recnd 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> z e. CC )
37 1cnd 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> 1 e. CC )
38 23 recnd 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> w e. CC )
39 36 37 38 subdid 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( z x. ( 1 - w ) ) = ( ( z x. 1 ) - ( z x. w ) ) )
40 36 mulid1d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( z x. 1 ) = z )
41 40 oveq1d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( ( z x. 1 ) - ( z x. w ) ) = ( z - ( z x. w ) ) )
42 39 41 eqtrd 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( z x. ( 1 - w ) ) = ( z - ( z x. w ) ) )
43 38 37 36 subdid 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( w x. ( 1 - z ) ) = ( ( w x. 1 ) - ( w x. z ) ) )
44 38 mulid1d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( w x. 1 ) = w )
45 38 36 mulcomd 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( w x. z ) = ( z x. w ) )
46 44 45 oveq12d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( ( w x. 1 ) - ( w x. z ) ) = ( w - ( z x. w ) ) )
47 43 46 eqtrd 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( w x. ( 1 - z ) ) = ( w - ( z x. w ) ) )
48 42 47 breq12d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( ( z x. ( 1 - w ) ) < ( w x. ( 1 - z ) ) <-> ( z - ( z x. w ) ) < ( w - ( z x. w ) ) ) )
49 35 48 bitr4d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( z < w <-> ( z x. ( 1 - w ) ) < ( w x. ( 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 ) ) e. _V
54 52 1 53 fvmpt 
 |-  ( z e. ( 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 ) ) e. _V
59 57 1 58 fvmpt 
 |-  ( w e. ( 0 [,) 1 ) -> ( F ` w ) = ( w / ( 1 - w ) ) )
60 54 59 breqan12d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( ( F ` z ) < ( F ` w ) <-> ( z / ( 1 - z ) ) < ( w / ( 1 - w ) ) ) )
61 33 49 60 3bitr4d 
 |-  ( ( z e. ( 0 [,) 1 ) /\ w e. ( 0 [,) 1 ) ) -> ( z < w <-> ( F ` z ) < ( F ` w ) ) )
62 61 rgen2 
 |-  A. z e. ( 0 [,) 1 ) A. w e. ( 0 [,) 1 ) ( z < w <-> ( F ` z ) < ( F ` w ) )
63 df-isom 
 |-  ( F Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) <-> ( F : ( 0 [,) 1 ) -1-1-onto-> ( 0 [,) +oo ) /\ A. z e. ( 0 [,) 1 ) A. w e. ( 0 [,) 1 ) ( z < w <-> ( F ` z ) < ( F ` w ) ) ) )
64 4 62 63 mpbir2an 
 |-  F Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +oo ) )
65 letsr 
 |-  <_ e. TosetRel
66 65 elexi 
 |-  <_ e. _V
67 66 inex1 
 |-  ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) e. _V
68 66 inex1 
 |-  ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) e. _V
69 icossxr 
 |-  ( 0 [,) 1 ) C_ RR*
70 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
71 leiso 
 |-  ( ( ( 0 [,) 1 ) C_ RR* /\ ( 0 [,) +oo ) C_ RR* ) -> ( F Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) <-> F Isom <_ , <_ ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) ) )
72 69 70 71 mp2an 
 |-  ( F Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) <-> F Isom <_ , <_ ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) )
73 64 72 mpbi 
 |-  F Isom <_ , <_ ( ( 0 [,) 1 ) , ( 0 [,) +oo ) )
74 isores1 
 |-  ( F Isom <_ , <_ ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) <-> F Isom ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) , <_ ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) )
75 73 74 mpbi 
 |-  F Isom ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) , <_ ( ( 0 [,) 1 ) , ( 0 [,) +oo ) )
76 isores2 
 |-  ( F Isom ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) , <_ ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) <-> F Isom ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) , ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) )
77 75 76 mpbi 
 |-  F Isom ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) , ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ( ( 0 [,) 1 ) , ( 0 [,) +oo ) )
78 tsrps 
 |-  ( <_ e. TosetRel -> <_ e. PosetRel )
79 65 78 ax-mp 
 |-  <_ e. PosetRel
80 ledm 
 |-  RR* = dom <_
81 80 psssdm 
 |-  ( ( <_ e. PosetRel /\ ( 0 [,) 1 ) C_ RR* ) -> dom ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) = ( 0 [,) 1 ) )
82 79 69 81 mp2an 
 |-  dom ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) = ( 0 [,) 1 )
83 82 eqcomi 
 |-  ( 0 [,) 1 ) = dom ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) )
84 80 psssdm 
 |-  ( ( <_ e. PosetRel /\ ( 0 [,) +oo ) C_ RR* ) -> dom ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) = ( 0 [,) +oo ) )
85 79 70 84 mp2an 
 |-  dom ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) = ( 0 [,) +oo )
86 85 eqcomi 
 |-  ( 0 [,) +oo ) = dom ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) )
87 83 86 ordthmeo 
 |-  ( ( ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) e. _V /\ ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) e. _V /\ F Isom ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) , ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) ) -> F e. ( ( ordTop ` ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) ) Homeo ( ordTop ` ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ) ) )
88 67 68 77 87 mp3an 
 |-  F e. ( ( ordTop ` ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) ) Homeo ( ordTop ` ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ) )
89 eqid 
 |-  ( ordTop ` <_ ) = ( ordTop ` <_ )
90 2 89 xrrest2 
 |-  ( ( 0 [,) 1 ) C_ RR -> ( J |`t ( 0 [,) 1 ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,) 1 ) ) )
91 10 90 ax-mp 
 |-  ( J |`t ( 0 [,) 1 ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,) 1 ) )
92 iccssico2 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) 1 ) ) -> ( x [,] y ) C_ ( 0 [,) 1 ) )
93 69 92 ordtrestixx 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,) 1 ) ) = ( ordTop ` ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) )
94 91 93 eqtri 
 |-  ( J |`t ( 0 [,) 1 ) ) = ( ordTop ` ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) )
95 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
96 2 89 xrrest2 
 |-  ( ( 0 [,) +oo ) C_ RR -> ( J |`t ( 0 [,) +oo ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,) +oo ) ) )
97 95 96 ax-mp 
 |-  ( J |`t ( 0 [,) +oo ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,) +oo ) )
98 iccssico2 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x [,] y ) C_ ( 0 [,) +oo ) )
99 70 98 ordtrestixx 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,) +oo ) ) = ( ordTop ` ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
100 97 99 eqtri 
 |-  ( J |`t ( 0 [,) +oo ) ) = ( ordTop ` ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
101 94 100 oveq12i 
 |-  ( ( J |`t ( 0 [,) 1 ) ) Homeo ( J |`t ( 0 [,) +oo ) ) ) = ( ( ordTop ` ( <_ i^i ( ( 0 [,) 1 ) X. ( 0 [,) 1 ) ) ) ) Homeo ( ordTop ` ( <_ i^i ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ) )
102 88 101 eleqtrri 
 |-  F e. ( ( J |`t ( 0 [,) 1 ) ) Homeo ( J |`t ( 0 [,) +oo ) ) )
103 64 102 pm3.2i 
 |-  ( F Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) /\ F e. ( ( J |`t ( 0 [,) 1 ) ) Homeo ( J |`t ( 0 [,) +oo ) ) ) )