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 e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )
iccpnfhmeo.k 
|- K = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
Assertion iccpnfhmeo 
|- ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ F e. ( II Homeo K ) )

Proof

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