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

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢F=x∈01⟼ifx=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 ⊢≤∩01×01∈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 ⊢FIsom<,<-1010+∞
13 iccssxr ⊢01⊆ℝ*
14 iccssxr ⊢0+∞⊆ℝ*
15 gtiso ⊢01⊆ℝ*∧0+∞⊆ℝ*→FIsom<,<-1010+∞↔FIsom≤,≤-1010+∞
16 13 14 15 mp2an ⊢FIsom<,<-1010+∞↔FIsom≤,≤-1010+∞
17 12 16 mpbi ⊢FIsom≤,≤-1010+∞
18 isores1 ⊢FIsom≤,≤-1010+∞↔FIsom≤∩01×01,≤-1010+∞
19 17 18 mpbi ⊢FIsom≤∩01×01,≤-1010+∞
20 isores2 ⊢FIsom≤∩01×01,≤-1010+∞↔FIsom≤∩01×01,≤-1∩0+∞×0+∞010+∞
21 19 20 mpbi ⊢FIsom≤∩01×01,≤-1∩0+∞×0+∞010+∞
22 ledm ⊢ℝ*=dom⁡≤
23 22 psssdm ⊢≤∈PosetRel∧01⊆ℝ*→dom⁡≤∩01×01=01
24 5 13 23 mp2an ⊢dom⁡≤∩01×01=01
25 24 eqcomi ⊢01=dom⁡≤∩01×01
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 ⊢≤∩01×01∈V∧≤-1∩0+∞×0+∞∈V∧FIsom≤∩01×01,≤-1∩0+∞×0+∞010+∞→F∈ordTop⁡≤∩01×01HomeoordTop⁡≤-1∩0+∞×0+∞
33 7 11 21 32 mp3an ⊢F∈ordTop⁡≤∩01×01HomeoordTop⁡≤-1∩0+∞×0+∞
34 dfii5 ⊢II=ordTop⁡≤∩01×01
35 iccss2 ⊢x∈0+∞∧y∈0+∞→xy⊆0+∞
36 14 35 cnvordtrestixx ⊢ordTop⁡≤↾𝑡0+∞=ordTop⁡≤-1∩0+∞×0+∞
37 2 36 eqtri ⊢J=ordTop⁡≤-1∩0+∞×0+∞
38 34 37 oveq12i ⊢IIHomeoJ=ordTop⁡≤∩01×01HomeoordTop⁡≤-1∩0+∞×0+∞
39 33 38 eleqtrri ⊢F∈IIHomeoJ