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 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) )
icopnfhmeo.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion icopnfhmeo ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ ( ( 𝐽 ↾t ( 0 [,) 1 ) ) Homeo ( 𝐽 ↾t ( 0 [,) +∞ ) ) ) )

Proof

Step Hyp Ref Expression
1 icopnfhmeo.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) )
2 icopnfhmeo.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
3 1 icopnfcnv ⊢ ( 𝐹 : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 0 [,) +∞ ) ↦ ( 𝑦 / ( 1 + 𝑦 ) ) ) )
4 3 simpli ⊢ 𝐹 : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ )
5 0re ⊢ 0 ∈ ℝ
6 1xr ⊢ 1 ∈ ℝ*
7 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( 𝑥 ∈ ( 0 [,) 1 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 1 ) ) )
8 5 6 7 mp2an ⊢ ( 𝑥 ∈ ( 0 [,) 1 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 1 ) )
9 8 simp1bi ⊢ ( 𝑥 ∈ ( 0 [,) 1 ) → 𝑥 ∈ ℝ )
10 9 ssriv ⊢ ( 0 [,) 1 ) ⊆ ℝ
11 10 sseli ⊢ ( 𝑧 ∈ ( 0 [,) 1 ) → 𝑧 ∈ ℝ )
12 11 adantr ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 𝑧 ∈ ℝ )
13 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( 𝑤 ∈ ( 0 [,) 1 ) ↔ ( 𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < 1 ) ) )
14 5 6 13 mp2an ⊢ ( 𝑤 ∈ ( 0 [,) 1 ) ↔ ( 𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < 1 ) )
15 14 simp3bi ⊢ ( 𝑤 ∈ ( 0 [,) 1 ) → 𝑤 < 1 )
16 10 sseli ⊢ ( 𝑤 ∈ ( 0 [,) 1 ) → 𝑤 ∈ ℝ )
17 1re ⊢ 1 ∈ ℝ
18 difrp ⊢ ( ( 𝑤 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑤 < 1 ↔ ( 1 − 𝑤 ) ∈ ℝ+ ) )
19 16 17 18 sylancl ⊢ ( 𝑤 ∈ ( 0 [,) 1 ) → ( 𝑤 < 1 ↔ ( 1 − 𝑤 ) ∈ ℝ+ ) )
20 15 19 mpbid ⊢ ( 𝑤 ∈ ( 0 [,) 1 ) → ( 1 − 𝑤 ) ∈ ℝ+ )
21 20 rpregt0d ⊢ ( 𝑤 ∈ ( 0 [,) 1 ) → ( ( 1 − 𝑤 ) ∈ ℝ ∧ 0 < ( 1 − 𝑤 ) ) )
22 21 adantl ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 1 − 𝑤 ) ∈ ℝ ∧ 0 < ( 1 − 𝑤 ) ) )
23 16 adantl ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 𝑤 ∈ ℝ )
24 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( 𝑧 ∈ ( 0 [,) 1 ) ↔ ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ∧ 𝑧 < 1 ) ) )
25 5 6 24 mp2an ⊢ ( 𝑧 ∈ ( 0 [,) 1 ) ↔ ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ∧ 𝑧 < 1 ) )
26 25 simp3bi ⊢ ( 𝑧 ∈ ( 0 [,) 1 ) → 𝑧 < 1 )
27 difrp ⊢ ( ( 𝑧 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑧 < 1 ↔ ( 1 − 𝑧 ) ∈ ℝ+ ) )
28 11 17 27 sylancl ⊢ ( 𝑧 ∈ ( 0 [,) 1 ) → ( 𝑧 < 1 ↔ ( 1 − 𝑧 ) ∈ ℝ+ ) )
29 26 28 mpbid ⊢ ( 𝑧 ∈ ( 0 [,) 1 ) → ( 1 − 𝑧 ) ∈ ℝ+ )
30 29 adantr ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 1 − 𝑧 ) ∈ ℝ+ )
31 30 rpregt0d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 1 − 𝑧 ) ∈ ℝ ∧ 0 < ( 1 − 𝑧 ) ) )
32 lt2mul2div ⊢ ( ( ( 𝑧 ∈ ℝ ∧ ( ( 1 − 𝑤 ) ∈ ℝ ∧ 0 < ( 1 − 𝑤 ) ) ) ∧ ( 𝑤 ∈ ℝ ∧ ( ( 1 − 𝑧 ) ∈ ℝ ∧ 0 < ( 1 − 𝑧 ) ) ) ) → ( ( 𝑧 · ( 1 − 𝑤 ) ) < ( 𝑤 · ( 1 − 𝑧 ) ) ↔ ( 𝑧 / ( 1 − 𝑧 ) ) < ( 𝑤 / ( 1 − 𝑤 ) ) ) )
33 12 22 23 31 32 syl22anc ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝑧 · ( 1 − 𝑤 ) ) < ( 𝑤 · ( 1 − 𝑧 ) ) ↔ ( 𝑧 / ( 1 − 𝑧 ) ) < ( 𝑤 / ( 1 − 𝑤 ) ) ) )
34 12 23 remulcld ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 · 𝑤 ) ∈ ℝ )
35 12 23 34 ltsub1d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 < 𝑤 ↔ ( 𝑧 − ( 𝑧 · 𝑤 ) ) < ( 𝑤 − ( 𝑧 · 𝑤 ) ) ) )
36 12 recnd ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 𝑧 ∈ ℂ )
37 1cnd ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 1 ∈ ℂ )
38 23 recnd ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → 𝑤 ∈ ℂ )
39 36 37 38 subdid ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 · ( 1 − 𝑤 ) ) = ( ( 𝑧 · 1 ) − ( 𝑧 · 𝑤 ) ) )
40 36 mulid1d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 · 1 ) = 𝑧 )
41 40 oveq1d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝑧 · 1 ) − ( 𝑧 · 𝑤 ) ) = ( 𝑧 − ( 𝑧 · 𝑤 ) ) )
42 39 41 eqtrd ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 · ( 1 − 𝑤 ) ) = ( 𝑧 − ( 𝑧 · 𝑤 ) ) )
43 38 37 36 subdid ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑤 · ( 1 − 𝑧 ) ) = ( ( 𝑤 · 1 ) − ( 𝑤 · 𝑧 ) ) )
44 38 mulid1d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑤 · 1 ) = 𝑤 )
45 38 36 mulcomd ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑤 · 𝑧 ) = ( 𝑧 · 𝑤 ) )
46 44 45 oveq12d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝑤 · 1 ) − ( 𝑤 · 𝑧 ) ) = ( 𝑤 − ( 𝑧 · 𝑤 ) ) )
47 43 46 eqtrd ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑤 · ( 1 − 𝑧 ) ) = ( 𝑤 − ( 𝑧 · 𝑤 ) ) )
48 42 47 breq12d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝑧 · ( 1 − 𝑤 ) ) < ( 𝑤 · ( 1 − 𝑧 ) ) ↔ ( 𝑧 − ( 𝑧 · 𝑤 ) ) < ( 𝑤 − ( 𝑧 · 𝑤 ) ) ) )
49 35 48 bitr4d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 < 𝑤 ↔ ( 𝑧 · ( 1 − 𝑤 ) ) < ( 𝑤 · ( 1 − 𝑧 ) ) ) )
50 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
51 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 1 − 𝑥 ) = ( 1 − 𝑧 ) )
52 50 51 oveq12d ⊢ ( 𝑥 = 𝑧 → ( 𝑥 / ( 1 − 𝑥 ) ) = ( 𝑧 / ( 1 − 𝑧 ) ) )
53 ovex ⊢ ( 𝑧 / ( 1 − 𝑧 ) ) ∈ V
54 52 1 53 fvmpt ⊢ ( 𝑧 ∈ ( 0 [,) 1 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 / ( 1 − 𝑧 ) ) )
55 id ⊢ ( 𝑥 = 𝑤 → 𝑥 = 𝑤 )
56 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 1 − 𝑥 ) = ( 1 − 𝑤 ) )
57 55 56 oveq12d ⊢ ( 𝑥 = 𝑤 → ( 𝑥 / ( 1 − 𝑥 ) ) = ( 𝑤 / ( 1 − 𝑤 ) ) )
58 ovex ⊢ ( 𝑤 / ( 1 − 𝑤 ) ) ∈ V
59 57 1 58 fvmpt ⊢ ( 𝑤 ∈ ( 0 [,) 1 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝑤 / ( 1 − 𝑤 ) ) )
60 54 59 breqan12d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ↔ ( 𝑧 / ( 1 − 𝑧 ) ) < ( 𝑤 / ( 1 − 𝑤 ) ) ) )
61 33 49 60 3bitr4d ⊢ ( ( 𝑧 ∈ ( 0 [,) 1 ) ∧ 𝑤 ∈ ( 0 [,) 1 ) ) → ( 𝑧 < 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ) )
62 61 rgen2 ⊢ ∀ 𝑧 ∈ ( 0 [,) 1 ) ∀ 𝑤 ∈ ( 0 [,) 1 ) ( 𝑧 < 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) )
63 df-isom ⊢ ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ ( 𝐹 : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ ) ∧ ∀ 𝑧 ∈ ( 0 [,) 1 ) ∀ 𝑤 ∈ ( 0 [,) 1 ) ( 𝑧 < 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ) ) )
64 4 62 63 mpbir2an ⊢ 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) )
65 letsr ⊢ ≤ ∈ TosetRel
66 65 elexi ⊢ ≤ ∈ V
67 66 inex1 ⊢ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) ∈ V
68 66 inex1 ⊢ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ∈ V
69 icossxr ⊢ ( 0 [,) 1 ) ⊆ ℝ*
70 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
71 leiso ⊢ ( ( ( 0 [,) 1 ) ⊆ ℝ* ∧ ( 0 [,) +∞ ) ⊆ ℝ* ) → ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ 𝐹 Isom ≤ , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ) )
72 69 70 71 mp2an ⊢ ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ 𝐹 Isom ≤ , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) )
73 64 72 mpbi ⊢ 𝐹 Isom ≤ , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) )
74 isores1 ⊢ ( 𝐹 Isom ≤ , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) )
75 73 74 mpbi ⊢ 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) )
76 isores2 ⊢ ( 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ≤ ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ↔ 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) )
77 75 76 mpbi ⊢ 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) )
78 tsrps ⊢ ( ≤ ∈ TosetRel → ≤ ∈ PosetRel )
79 65 78 ax-mp ⊢ ≤ ∈ PosetRel
80 ledm ⊢ ℝ* = dom ≤
81 80 psssdm ⊢ ( ( ≤ ∈ PosetRel ∧ ( 0 [,) 1 ) ⊆ ℝ* ) → dom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) = ( 0 [,) 1 ) )
82 79 69 81 mp2an ⊢ dom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) = ( 0 [,) 1 )
83 82 eqcomi ⊢ ( 0 [,) 1 ) = dom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) )
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 ⊢ ( ( ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) ∈ V ∧ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ∈ V ∧ 𝐹 Isom ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) , ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ) → 𝐹 ∈ ( ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) ) Homeo ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ) ) )
88 67 68 77 87 mp3an ⊢ 𝐹 ∈ ( ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) ) Homeo ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ) )
89 eqid ⊢ ( ordTop ‘ ≤ ) = ( ordTop ‘ ≤ )
90 2 89 xrrest2 ⊢ ( ( 0 [,) 1 ) ⊆ ℝ → ( 𝐽 ↾t ( 0 [,) 1 ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) 1 ) ) )
91 10 90 ax-mp ⊢ ( 𝐽 ↾t ( 0 [,) 1 ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) 1 ) )
92 iccssico2 ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) 1 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 0 [,) 1 ) )
93 69 92 ordtrestixx ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) 1 ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) )
94 91 93 eqtri ⊢ ( 𝐽 ↾t ( 0 [,) 1 ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) )
95 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
96 2 89 xrrest2 ⊢ ( ( 0 [,) +∞ ) ⊆ ℝ → ( 𝐽 ↾t ( 0 [,) +∞ ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) +∞ ) ) )
97 95 96 ax-mp ⊢ ( 𝐽 ↾t ( 0 [,) +∞ ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) +∞ ) )
98 iccssico2 ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 0 [,) +∞ ) )
99 70 98 ordtrestixx ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,) +∞ ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) )
100 97 99 eqtri ⊢ ( 𝐽 ↾t ( 0 [,) +∞ ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) )
101 94 100 oveq12i ⊢ ( ( 𝐽 ↾t ( 0 [,) 1 ) ) Homeo ( 𝐽 ↾t ( 0 [,) +∞ ) ) ) = ( ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) 1 ) × ( 0 [,) 1 ) ) ) ) Homeo ( ordTop ‘ ( ≤ ∩ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ) )
102 88 101 eleqtrri ⊢ 𝐹 ∈ ( ( 𝐽 ↾t ( 0 [,) 1 ) ) Homeo ( 𝐽 ↾t ( 0 [,) +∞ ) ) )
103 64 102 pm3.2i ⊢ ( 𝐹 Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ ( ( 𝐽 ↾t ( 0 [,) 1 ) ) Homeo ( 𝐽 ↾t ( 0 [,) +∞ ) ) ) )