Metamath Proof Explorer


Theorem xrge0iifhmeo

Description: Expose a homeomorphism from the closed unit interval to the extended nonnegative reals. (Contributed by Thierry Arnoux, 1-Apr-2017)

Ref Expression
Hypotheses xrge0iifhmeo.1 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
xrge0iifhmeo.k 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
Assertion xrge0iifhmeo 𝐹 ∈ ( II Homeo 𝐽 )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
2 xrge0iifhmeo.k 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
3 letsr ≤ ∈ TosetRel
4 tsrps ( ≤ ∈ TosetRel → ≤ ∈ PosetRel )
5 3 4 ax-mp ≤ ∈ PosetRel
6 5 elexi ≤ ∈ V
7 6 inex1 ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ V
8 cnvps ( ≤ ∈ PosetRel → ≤ ∈ PosetRel )
9 5 8 ax-mp ≤ ∈ PosetRel
10 9 elexi ≤ ∈ V
11 10 inex1 ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ∈ V
12 1 xrge0iifiso 𝐹 Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) )
13 iccssxr ( 0 [,] 1 ) ⊆ ℝ*
14 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
15 gtiso ( ( ( 0 [,] 1 ) ⊆ ℝ* ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → ( 𝐹 Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) ↔ 𝐹 Isom ≤ , ≤ ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) ) )
16 13 14 15 mp2an ( 𝐹 Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) ↔ 𝐹 Isom ≤ , ≤ ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) )
17 12 16 mpbi 𝐹 Isom ≤ , ≤ ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) )
18 isores1 ( 𝐹 Isom ≤ , ≤ ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) ↔ 𝐹 Isom ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) , ≤ ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) )
19 17 18 mpbi 𝐹 Isom ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) , ≤ ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) )
20 isores2 ( 𝐹 Isom ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) , ≤ ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) ↔ 𝐹 Isom ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) , ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) )
21 19 20 mpbi 𝐹 Isom ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) , ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) )
22 ledm * = dom ≤
23 22 psssdm ( ( ≤ ∈ PosetRel ∧ ( 0 [,] 1 ) ⊆ ℝ* ) → dom ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) = ( 0 [,] 1 ) )
24 5 13 23 mp2an dom ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) = ( 0 [,] 1 )
25 24 eqcomi ( 0 [,] 1 ) = dom ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
26 lern * = ran ≤
27 df-rn ran ≤ = dom
28 26 27 eqtri * = dom
29 28 psssdm ( ( ≤ ∈ PosetRel ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → dom ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) = ( 0 [,] +∞ ) )
30 9 14 29 mp2an dom ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) = ( 0 [,] +∞ )
31 30 eqcomi ( 0 [,] +∞ ) = dom ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) )
32 25 31 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 [,] +∞ ) ) ) ) ) )
33 7 11 21 32 mp3an 𝐹 ∈ ( ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ) Homeo ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ) )
34 dfii5 II = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
35 iccss2 ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 0 [,] +∞ ) )
36 14 35 cnvordtrestixx ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) )
37 2 36 eqtri 𝐽 = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) )
38 34 37 oveq12i ( II Homeo 𝐽 ) = ( ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ) Homeo ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ) )
39 33 38 eleqtrri 𝐹 ∈ ( II Homeo 𝐽 )