# Metamath Proof Explorer

## Theorem iccpnfhmeo

Description: The defined bijection from [ 0 , 1 ] to [ 0 , +oo ] is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses iccpnfhmeo.f ${⊢}{F}=\left({x}\in \left[0,1\right]⟼if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
iccpnfhmeo.k ${⊢}{K}=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]$
Assertion iccpnfhmeo ${⊢}\left({F}{Isom}_{<,<}\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)\wedge {F}\in \left(\mathrm{II}\mathrm{Homeo}{K}\right)\right)$

### Proof

Step Hyp Ref Expression
1 iccpnfhmeo.f ${⊢}{F}=\left({x}\in \left[0,1\right]⟼if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
2 iccpnfhmeo.k ${⊢}{K}=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]$
3 iccssxr ${⊢}\left[0,1\right]\subseteq {ℝ}^{*}$
4 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
5 soss ${⊢}\left[0,1\right]\subseteq {ℝ}^{*}\to \left(<\mathrm{Or}{ℝ}^{*}\to <\mathrm{Or}\left[0,1\right]\right)$
6 3 4 5 mp2 ${⊢}<\mathrm{Or}\left[0,1\right]$
7 iccssxr ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$
8 soss ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\to \left(<\mathrm{Or}{ℝ}^{*}\to <\mathrm{Or}\left[0,\mathrm{+\infty }\right]\right)$
9 7 4 8 mp2 ${⊢}<\mathrm{Or}\left[0,\mathrm{+\infty }\right]$
10 sopo ${⊢}<\mathrm{Or}\left[0,\mathrm{+\infty }\right]\to <\mathrm{Po}\left[0,\mathrm{+\infty }\right]$
11 9 10 ax-mp ${⊢}<\mathrm{Po}\left[0,\mathrm{+\infty }\right]$
12 1 iccpnfcnv ${⊢}\left({F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right]\wedge {{F}}^{-1}=\left({y}\in \left[0,\mathrm{+\infty }\right]⟼if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)\right)\right)$
13 12 simpli ${⊢}{F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right]$
14 f1ofo ${⊢}{F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right]\to {F}:\left[0,1\right]\underset{onto}{⟶}\left[0,\mathrm{+\infty }\right]$
15 13 14 ax-mp ${⊢}{F}:\left[0,1\right]\underset{onto}{⟶}\left[0,\mathrm{+\infty }\right]$
16 elicc01 ${⊢}{z}\in \left[0,1\right]↔\left({z}\in ℝ\wedge 0\le {z}\wedge {z}\le 1\right)$
17 16 simp1bi ${⊢}{z}\in \left[0,1\right]\to {z}\in ℝ$
18 17 3ad2ant1 ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {z}\in ℝ$
19 elicc01 ${⊢}{w}\in \left[0,1\right]↔\left({w}\in ℝ\wedge 0\le {w}\wedge {w}\le 1\right)$
20 19 simp1bi ${⊢}{w}\in \left[0,1\right]\to {w}\in ℝ$
21 20 3ad2ant2 ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {w}\in ℝ$
22 1red ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to 1\in ℝ$
23 simp3 ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {z}<{w}$
24 19 simp3bi ${⊢}{w}\in \left[0,1\right]\to {w}\le 1$
25 24 3ad2ant2 ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {w}\le 1$
26 18 21 22 23 25 ltletrd ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {z}<1$
27 18 26 gtned ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to 1\ne {z}$
28 27 necomd ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {z}\ne 1$
29 ifnefalse ${⊢}{z}\ne 1\to if\left({z}=1,\mathrm{+\infty },\frac{{z}}{1-{z}}\right)=\frac{{z}}{1-{z}}$
30 28 29 syl ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to if\left({z}=1,\mathrm{+\infty },\frac{{z}}{1-{z}}\right)=\frac{{z}}{1-{z}}$
31 breq2 ${⊢}\mathrm{+\infty }=if\left({w}=1,\mathrm{+\infty },\frac{{w}}{1-{w}}\right)\to \left(\frac{{z}}{1-{z}}<\mathrm{+\infty }↔\frac{{z}}{1-{z}}
32 breq2 ${⊢}\frac{{w}}{1-{w}}=if\left({w}=1,\mathrm{+\infty },\frac{{w}}{1-{w}}\right)\to \left(\frac{{z}}{1-{z}}<\frac{{w}}{1-{w}}↔\frac{{z}}{1-{z}}
33 1re ${⊢}1\in ℝ$
34 resubcl ${⊢}\left(1\in ℝ\wedge {z}\in ℝ\right)\to 1-{z}\in ℝ$
35 33 18 34 sylancr ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to 1-{z}\in ℝ$
36 ax-1cn ${⊢}1\in ℂ$
37 18 recnd ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {z}\in ℂ$
38 subeq0 ${⊢}\left(1\in ℂ\wedge {z}\in ℂ\right)\to \left(1-{z}=0↔1={z}\right)$
39 38 necon3bid ${⊢}\left(1\in ℂ\wedge {z}\in ℂ\right)\to \left(1-{z}\ne 0↔1\ne {z}\right)$
40 36 37 39 sylancr ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \left(1-{z}\ne 0↔1\ne {z}\right)$
41 27 40 mpbird ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to 1-{z}\ne 0$
42 18 35 41 redivcld ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \frac{{z}}{1-{z}}\in ℝ$
43 42 ltpnfd ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \frac{{z}}{1-{z}}<\mathrm{+\infty }$
44 43 adantr ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge {w}=1\right)\to \frac{{z}}{1-{z}}<\mathrm{+\infty }$
45 simpl3 ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge ¬{w}=1\right)\to {z}<{w}$
46 eqid ${⊢}\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)=\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)$
47 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
48 46 47 icopnfhmeo ${⊢}\left(\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right){Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left[0,1\right)\right)\mathrm{Homeo}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right)\right)\right)\right)$
49 48 simpli ${⊢}\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right){Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)$
50 49 a1i ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge ¬{w}=1\right)\to \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right){Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)$
51 simp1 ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {z}\in \left[0,1\right]$
52 0xr ${⊢}0\in {ℝ}^{*}$
53 1xr ${⊢}1\in {ℝ}^{*}$
54 0le1 ${⊢}0\le 1$
55 snunico ${⊢}\left(0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\wedge 0\le 1\right)\to \left[0,1\right)\cup \left\{1\right\}=\left[0,1\right]$
56 52 53 54 55 mp3an ${⊢}\left[0,1\right)\cup \left\{1\right\}=\left[0,1\right]$
57 51 56 eleqtrrdi ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {z}\in \left(\left[0,1\right)\cup \left\{1\right\}\right)$
58 elun ${⊢}{z}\in \left(\left[0,1\right)\cup \left\{1\right\}\right)↔\left({z}\in \left[0,1\right)\vee {z}\in \left\{1\right\}\right)$
59 57 58 sylib ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \left({z}\in \left[0,1\right)\vee {z}\in \left\{1\right\}\right)$
60 59 ord ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \left(¬{z}\in \left[0,1\right)\to {z}\in \left\{1\right\}\right)$
61 elsni ${⊢}{z}\in \left\{1\right\}\to {z}=1$
62 60 61 syl6 ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \left(¬{z}\in \left[0,1\right)\to {z}=1\right)$
63 62 necon1ad ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \left({z}\ne 1\to {z}\in \left[0,1\right)\right)$
64 28 63 mpd ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {z}\in \left[0,1\right)$
65 64 adantr ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge ¬{w}=1\right)\to {z}\in \left[0,1\right)$
66 simp2 ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {w}\in \left[0,1\right]$
67 66 56 eleqtrrdi ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to {w}\in \left(\left[0,1\right)\cup \left\{1\right\}\right)$
68 elun ${⊢}{w}\in \left(\left[0,1\right)\cup \left\{1\right\}\right)↔\left({w}\in \left[0,1\right)\vee {w}\in \left\{1\right\}\right)$
69 67 68 sylib ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \left({w}\in \left[0,1\right)\vee {w}\in \left\{1\right\}\right)$
70 69 ord ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \left(¬{w}\in \left[0,1\right)\to {w}\in \left\{1\right\}\right)$
71 elsni ${⊢}{w}\in \left\{1\right\}\to {w}=1$
72 70 71 syl6 ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \left(¬{w}\in \left[0,1\right)\to {w}=1\right)$
73 72 con1d ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \left(¬{w}=1\to {w}\in \left[0,1\right)\right)$
74 73 imp ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge ¬{w}=1\right)\to {w}\in \left[0,1\right)$
75 isorel ${⊢}\left(\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right){Isom}_{<,<}\left(\left[0,1\right),\left[0,\mathrm{+\infty }\right)\right)\wedge \left({z}\in \left[0,1\right)\wedge {w}\in \left[0,1\right)\right)\right)\to \left({z}<{w}↔\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({z}\right)<\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({w}\right)\right)$
76 50 65 74 75 syl12anc ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge ¬{w}=1\right)\to \left({z}<{w}↔\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({z}\right)<\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({w}\right)\right)$
77 45 76 mpbid ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge ¬{w}=1\right)\to \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({z}\right)<\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({w}\right)$
78 id ${⊢}{x}={z}\to {x}={z}$
79 oveq2 ${⊢}{x}={z}\to 1-{x}=1-{z}$
80 78 79 oveq12d ${⊢}{x}={z}\to \frac{{x}}{1-{x}}=\frac{{z}}{1-{z}}$
81 ovex ${⊢}\frac{{z}}{1-{z}}\in \mathrm{V}$
82 80 46 81 fvmpt ${⊢}{z}\in \left[0,1\right)\to \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({z}\right)=\frac{{z}}{1-{z}}$
83 65 82 syl ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge ¬{w}=1\right)\to \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({z}\right)=\frac{{z}}{1-{z}}$
84 id ${⊢}{x}={w}\to {x}={w}$
85 oveq2 ${⊢}{x}={w}\to 1-{x}=1-{w}$
86 84 85 oveq12d ${⊢}{x}={w}\to \frac{{x}}{1-{x}}=\frac{{w}}{1-{w}}$
87 ovex ${⊢}\frac{{w}}{1-{w}}\in \mathrm{V}$
88 86 46 87 fvmpt ${⊢}{w}\in \left[0,1\right)\to \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({w}\right)=\frac{{w}}{1-{w}}$
89 74 88 syl ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge ¬{w}=1\right)\to \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({w}\right)=\frac{{w}}{1-{w}}$
90 77 83 89 3brtr3d ${⊢}\left(\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\wedge ¬{w}=1\right)\to \frac{{z}}{1-{z}}<\frac{{w}}{1-{w}}$
91 31 32 44 90 ifbothda ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to \frac{{z}}{1-{z}}
92 30 91 eqbrtrd ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\wedge {z}<{w}\right)\to if\left({z}=1,\mathrm{+\infty },\frac{{z}}{1-{z}}\right)
93 92 3expia ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\right)\to \left({z}<{w}\to if\left({z}=1,\mathrm{+\infty },\frac{{z}}{1-{z}}\right)
94 eqeq1 ${⊢}{x}={z}\to \left({x}=1↔{z}=1\right)$
95 94 80 ifbieq2d ${⊢}{x}={z}\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)=if\left({z}=1,\mathrm{+\infty },\frac{{z}}{1-{z}}\right)$
96 pnfex ${⊢}\mathrm{+\infty }\in \mathrm{V}$
97 96 81 ifex ${⊢}if\left({z}=1,\mathrm{+\infty },\frac{{z}}{1-{z}}\right)\in \mathrm{V}$
98 95 1 97 fvmpt ${⊢}{z}\in \left[0,1\right]\to {F}\left({z}\right)=if\left({z}=1,\mathrm{+\infty },\frac{{z}}{1-{z}}\right)$
99 eqeq1 ${⊢}{x}={w}\to \left({x}=1↔{w}=1\right)$
100 99 86 ifbieq2d ${⊢}{x}={w}\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)=if\left({w}=1,\mathrm{+\infty },\frac{{w}}{1-{w}}\right)$
101 96 87 ifex ${⊢}if\left({w}=1,\mathrm{+\infty },\frac{{w}}{1-{w}}\right)\in \mathrm{V}$
102 100 1 101 fvmpt ${⊢}{w}\in \left[0,1\right]\to {F}\left({w}\right)=if\left({w}=1,\mathrm{+\infty },\frac{{w}}{1-{w}}\right)$
103 98 102 breqan12d ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\right)\to \left({F}\left({z}\right)<{F}\left({w}\right)↔if\left({z}=1,\mathrm{+\infty },\frac{{z}}{1-{z}}\right)
104 93 103 sylibrd ${⊢}\left({z}\in \left[0,1\right]\wedge {w}\in \left[0,1\right]\right)\to \left({z}<{w}\to {F}\left({z}\right)<{F}\left({w}\right)\right)$
105 104 rgen2 ${⊢}\forall {z}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left({z}<{w}\to {F}\left({z}\right)<{F}\left({w}\right)\right)$
106 soisoi ${⊢}\left(\left(<\mathrm{Or}\left[0,1\right]\wedge <\mathrm{Po}\left[0,\mathrm{+\infty }\right]\right)\wedge \left({F}:\left[0,1\right]\underset{onto}{⟶}\left[0,\mathrm{+\infty }\right]\wedge \forall {z}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left({z}<{w}\to {F}\left({z}\right)<{F}\left({w}\right)\right)\right)\right)\to {F}{Isom}_{<,<}\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)$
107 6 11 15 105 106 mp4an ${⊢}{F}{Isom}_{<,<}\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)$
108 letsr ${⊢}\le \in \mathrm{TosetRel}$
109 108 elexi ${⊢}\le \in \mathrm{V}$
110 109 inex1 ${⊢}\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\in \mathrm{V}$
111 109 inex1 ${⊢}\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\in \mathrm{V}$
112 leiso ${⊢}\left(\left[0,1\right]\subseteq {ℝ}^{*}\wedge \left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\right)\to \left({F}{Isom}_{<,<}\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)↔{F}{Isom}_{\le ,\le }\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)\right)$
113 3 7 112 mp2an ${⊢}{F}{Isom}_{<,<}\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)↔{F}{Isom}_{\le ,\le }\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)$
114 107 113 mpbi ${⊢}{F}{Isom}_{\le ,\le }\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)$
115 isores1 ${⊢}{F}{Isom}_{\le ,\le }\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)↔{F}{Isom}_{\le \cap \left(\left[0,1\right]×\left[0,1\right]\right),\le }\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)$
116 114 115 mpbi ${⊢}{F}{Isom}_{\le \cap \left(\left[0,1\right]×\left[0,1\right]\right),\le }\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)$
117 isores2 ${⊢}{F}{Isom}_{\le \cap \left(\left[0,1\right]×\left[0,1\right]\right),\le }\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)↔{F}{Isom}_{\le \cap \left(\left[0,1\right]×\left[0,1\right]\right),\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)}\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)$
118 116 117 mpbi ${⊢}{F}{Isom}_{\le \cap \left(\left[0,1\right]×\left[0,1\right]\right),\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)}\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)$
119 tsrps ${⊢}\le \in \mathrm{TosetRel}\to \le \in \mathrm{PosetRel}$
120 108 119 ax-mp ${⊢}\le \in \mathrm{PosetRel}$
121 ledm ${⊢}{ℝ}^{*}=\mathrm{dom}\le$
122 121 psssdm ${⊢}\left(\le \in \mathrm{PosetRel}\wedge \left[0,1\right]\subseteq {ℝ}^{*}\right)\to \mathrm{dom}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)=\left[0,1\right]$
123 120 3 122 mp2an ${⊢}\mathrm{dom}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)=\left[0,1\right]$
124 123 eqcomi ${⊢}\left[0,1\right]=\mathrm{dom}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)$
125 121 psssdm ${⊢}\left(\le \in \mathrm{PosetRel}\wedge \left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\right)\to \mathrm{dom}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\right)=\left[0,\mathrm{+\infty }\right]$
126 120 7 125 mp2an ${⊢}\mathrm{dom}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\right)=\left[0,\mathrm{+\infty }\right]$
127 126 eqcomi ${⊢}\left[0,\mathrm{+\infty }\right]=\mathrm{dom}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\right)$
128 124 127 ordthmeo ${⊢}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\in \mathrm{V}\wedge \le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\in \mathrm{V}\wedge {F}{Isom}_{\le \cap \left(\left[0,1\right]×\left[0,1\right]\right),\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)}\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)\right)\to {F}\in \left(\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)\mathrm{Homeo}\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\right)\right)$
129 110 111 118 128 mp3an ${⊢}{F}\in \left(\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)\mathrm{Homeo}\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\right)\right)$
130 dfii5 ${⊢}\mathrm{II}=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)$
131 ordtresticc ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]=\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\right)$
132 2 131 eqtri ${⊢}{K}=\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\right)$
133 130 132 oveq12i ${⊢}\mathrm{II}\mathrm{Homeo}{K}=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)\mathrm{Homeo}\mathrm{ordTop}\left(\le \cap \left(\left[0,\mathrm{+\infty }\right]×\left[0,\mathrm{+\infty }\right]\right)\right)$
134 129 133 eleqtrri ${⊢}{F}\in \left(\mathrm{II}\mathrm{Homeo}{K}\right)$
135 107 134 pm3.2i ${⊢}\left({F}{Isom}_{<,<}\left(\left[0,1\right],\left[0,\mathrm{+\infty }\right]\right)\wedge {F}\in \left(\mathrm{II}\mathrm{Homeo}{K}\right)\right)$