This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) )
iccpnfhmeo.k ⊢ 𝐾 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
Assertion iccpnfhmeo ( 𝐹 Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) ∧ 𝐹 ∈ ( II Homeo 𝐾 ) )

Proof

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