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 𝐽 )