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 ⊢ F = x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x
xrge0iifhmeo.k ⊢ J = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
Assertion xrge0iifhmeo ⊢ F ∈ II Homeo J

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢ F = x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x
2 xrge0iifhmeo.k ⊢ J = ordTop ⁡ ≤ ↾ 𝑡 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 → ≤ -1 ∈ PosetRel
9 5 8 ax-mp ⊢ ≤ -1 ∈ PosetRel
10 9 elexi ⊢ ≤ -1 ∈ V
11 10 inex1 ⊢ ≤ -1 ∩ 0 +∞ × 0 +∞ ∈ V
12 1 xrge0iifiso ⊢ F Isom < , < -1 0 1 0 +∞
13 iccssxr ⊢ 0 1 ⊆ ℝ *
14 iccssxr ⊢ 0 +∞ ⊆ ℝ *
15 gtiso ⊢ 0 1 ⊆ ℝ * ∧ 0 +∞ ⊆ ℝ * → F Isom < , < -1 0 1 0 +∞ ↔ F Isom ≤ , ≤ -1 0 1 0 +∞
16 13 14 15 mp2an ⊢ F Isom < , < -1 0 1 0 +∞ ↔ F Isom ≤ , ≤ -1 0 1 0 +∞
17 12 16 mpbi ⊢ F Isom ≤ , ≤ -1 0 1 0 +∞
18 isores1 ⊢ F Isom ≤ , ≤ -1 0 1 0 +∞ ↔ F Isom ≤ ∩ 0 1 × 0 1 , ≤ -1 0 1 0 +∞
19 17 18 mpbi ⊢ F Isom ≤ ∩ 0 1 × 0 1 , ≤ -1 0 1 0 +∞
20 isores2 ⊢ F Isom ≤ ∩ 0 1 × 0 1 , ≤ -1 0 1 0 +∞ ↔ F Isom ≤ ∩ 0 1 × 0 1 , ≤ -1 ∩ 0 +∞ × 0 +∞ 0 1 0 +∞
21 19 20 mpbi ⊢ F Isom ≤ ∩ 0 1 × 0 1 , ≤ -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 ⁡ ≤ -1
28 26 27 eqtri ⊢ ℝ * = dom ⁡ ≤ -1
29 28 psssdm ⊢ ≤ -1 ∈ PosetRel ∧ 0 +∞ ⊆ ℝ * → dom ⁡ ≤ -1 ∩ 0 +∞ × 0 +∞ = 0 +∞
30 9 14 29 mp2an ⊢ dom ⁡ ≤ -1 ∩ 0 +∞ × 0 +∞ = 0 +∞
31 30 eqcomi ⊢ 0 +∞ = dom ⁡ ≤ -1 ∩ 0 +∞ × 0 +∞
32 25 31 ordthmeo ⊢ ≤ ∩ 0 1 × 0 1 ∈ V ∧ ≤ -1 ∩ 0 +∞ × 0 +∞ ∈ V ∧ F Isom ≤ ∩ 0 1 × 0 1 , ≤ -1 ∩ 0 +∞ × 0 +∞ 0 1 0 +∞ → F ∈ ordTop ⁡ ≤ ∩ 0 1 × 0 1 Homeo ordTop ⁡ ≤ -1 ∩ 0 +∞ × 0 +∞
33 7 11 21 32 mp3an ⊢ F ∈ ordTop ⁡ ≤ ∩ 0 1 × 0 1 Homeo ordTop ⁡ ≤ -1 ∩ 0 +∞ × 0 +∞
34 dfii5 ⊢ II = ordTop ⁡ ≤ ∩ 0 1 × 0 1
35 iccss2 ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x y ⊆ 0 +∞
36 14 35 cnvordtrestixx ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ -1 ∩ 0 +∞ × 0 +∞
37 2 36 eqtri ⊢ J = ordTop ⁡ ≤ -1 ∩ 0 +∞ × 0 +∞
38 34 37 oveq12i ⊢ II Homeo J = ordTop ⁡ ≤ ∩ 0 1 × 0 1 Homeo ordTop ⁡ ≤ -1 ∩ 0 +∞ × 0 +∞
39 33 38 eleqtrri ⊢ F ∈ II Homeo J