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

Metamath Proof Explorer

Theorem iccpnfcnv

Description: Define a bijection from [ 0 , 1 ] to [ 0 , +oo ] . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypothesis iccpnfhmeo.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) )
Assertion iccpnfcnv ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iccpnfhmeo.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) )
2 0xr ⊢ 0 ∈ ℝ*
3 pnfxr ⊢ +∞ ∈ ℝ*
4 0lepnf ⊢ 0 ≤ +∞
5 ubicc2 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → +∞ ∈ ( 0 [,] +∞ ) )
6 2 3 4 5 mp3an ⊢ +∞ ∈ ( 0 [,] +∞ )
7 6 a1i ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 = 1 ) → +∞ ∈ ( 0 [,] +∞ ) )
8 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
9 1xr ⊢ 1 ∈ ℝ*
10 0le1 ⊢ 0 ≤ 1
11 snunico ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1 ) → ( ( 0 [,) 1 ) ∪ { 1 } ) = ( 0 [,] 1 ) )
12 2 9 10 11 mp3an ⊢ ( ( 0 [,) 1 ) ∪ { 1 } ) = ( 0 [,] 1 )
13 12 eleq2i ⊢ ( 𝑥 ∈ ( ( 0 [,) 1 ) ∪ { 1 } ) ↔ 𝑥 ∈ ( 0 [,] 1 ) )
14 elun ⊢ ( 𝑥 ∈ ( ( 0 [,) 1 ) ∪ { 1 } ) ↔ ( 𝑥 ∈ ( 0 [,) 1 ) ∨ 𝑥 ∈ { 1 } ) )
15 13 14 bitr3i ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ( 0 [,) 1 ) ∨ 𝑥 ∈ { 1 } ) )
16 pm2.53 ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∨ 𝑥 ∈ { 1 } ) → ( ¬ 𝑥 ∈ ( 0 [,) 1 ) → 𝑥 ∈ { 1 } ) )
17 15 16 sylbi ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( ¬ 𝑥 ∈ ( 0 [,) 1 ) → 𝑥 ∈ { 1 } ) )
18 elsni ⊢ ( 𝑥 ∈ { 1 } → 𝑥 = 1 )
19 17 18 syl6 ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( ¬ 𝑥 ∈ ( 0 [,) 1 ) → 𝑥 = 1 ) )
20 19 con1d ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( ¬ 𝑥 = 1 → 𝑥 ∈ ( 0 [,) 1 ) ) )
21 20 imp ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 1 ) → 𝑥 ∈ ( 0 [,) 1 ) )
22 eqid ⊢ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) )
23 22 icopnfcnv ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ ) ∧ ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) = ( 𝑦 ∈ ( 0 [,) +∞ ) ↦ ( 𝑦 / ( 1 + 𝑦 ) ) ) )
24 23 simpli ⊢ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ )
25 f1of ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ ) → ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) 1 ) ⟶ ( 0 [,) +∞ ) )
26 24 25 ax-mp ⊢ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) 1 ) ⟶ ( 0 [,) +∞ )
27 22 fmpt ⊢ ( ∀ 𝑥 ∈ ( 0 [,) 1 ) ( 𝑥 / ( 1 − 𝑥 ) ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) 1 ) ⟶ ( 0 [,) +∞ ) )
28 26 27 mpbir ⊢ ∀ 𝑥 ∈ ( 0 [,) 1 ) ( 𝑥 / ( 1 − 𝑥 ) ) ∈ ( 0 [,) +∞ )
29 28 rspec ⊢ ( 𝑥 ∈ ( 0 [,) 1 ) → ( 𝑥 / ( 1 − 𝑥 ) ) ∈ ( 0 [,) +∞ ) )
30 21 29 syl ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 1 ) → ( 𝑥 / ( 1 − 𝑥 ) ) ∈ ( 0 [,) +∞ ) )
31 8 30 sselid ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 1 ) → ( 𝑥 / ( 1 − 𝑥 ) ) ∈ ( 0 [,] +∞ ) )
32 7 31 ifclda ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∈ ( 0 [,] +∞ ) )
33 32 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∈ ( 0 [,] +∞ ) )
34 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
35 34 a1i ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ 𝑦 = +∞ ) → 1 ∈ ( 0 [,] 1 ) )
36 icossicc ⊢ ( 0 [,) 1 ) ⊆ ( 0 [,] 1 )
37 snunico ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → ( ( 0 [,) +∞ ) ∪ { +∞ } ) = ( 0 [,] +∞ ) )
38 2 3 4 37 mp3an ⊢ ( ( 0 [,) +∞ ) ∪ { +∞ } ) = ( 0 [,] +∞ )
39 38 eleq2i ⊢ ( 𝑦 ∈ ( ( 0 [,) +∞ ) ∪ { +∞ } ) ↔ 𝑦 ∈ ( 0 [,] +∞ ) )
40 elun ⊢ ( 𝑦 ∈ ( ( 0 [,) +∞ ) ∪ { +∞ } ) ↔ ( 𝑦 ∈ ( 0 [,) +∞ ) ∨ 𝑦 ∈ { +∞ } ) )
41 39 40 bitr3i ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) ↔ ( 𝑦 ∈ ( 0 [,) +∞ ) ∨ 𝑦 ∈ { +∞ } ) )
42 pm2.53 ⊢ ( ( 𝑦 ∈ ( 0 [,) +∞ ) ∨ 𝑦 ∈ { +∞ } ) → ( ¬ 𝑦 ∈ ( 0 [,) +∞ ) → 𝑦 ∈ { +∞ } ) )
43 41 42 sylbi ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → ( ¬ 𝑦 ∈ ( 0 [,) +∞ ) → 𝑦 ∈ { +∞ } ) )
44 elsni ⊢ ( 𝑦 ∈ { +∞ } → 𝑦 = +∞ )
45 43 44 syl6 ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → ( ¬ 𝑦 ∈ ( 0 [,) +∞ ) → 𝑦 = +∞ ) )
46 45 con1d ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → ( ¬ 𝑦 = +∞ → 𝑦 ∈ ( 0 [,) +∞ ) ) )
47 46 imp ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → 𝑦 ∈ ( 0 [,) +∞ ) )
48 f1ocnv ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ ) → ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) +∞ ) –1-1-onto→ ( 0 [,) 1 ) )
49 f1of ⊢ ( ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) +∞ ) –1-1-onto→ ( 0 [,) 1 ) → ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) +∞ ) ⟶ ( 0 [,) 1 ) )
50 24 48 49 mp2b ⊢ ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) +∞ ) ⟶ ( 0 [,) 1 )
51 23 simpri ⊢ ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) = ( 𝑦 ∈ ( 0 [,) +∞ ) ↦ ( 𝑦 / ( 1 + 𝑦 ) ) )
52 51 fmpt ⊢ ( ∀ 𝑦 ∈ ( 0 [,) +∞ ) ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ( 0 [,) 1 ) ↔ ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) +∞ ) ⟶ ( 0 [,) 1 ) )
53 50 52 mpbir ⊢ ∀ 𝑦 ∈ ( 0 [,) +∞ ) ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ( 0 [,) 1 )
54 53 rspec ⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ( 0 [,) 1 ) )
55 47 54 syl ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ( 0 [,) 1 ) )
56 36 55 sselid ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ( 0 [,] 1 ) )
57 35 56 ifclda ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ∈ ( 0 [,] 1 ) )
58 57 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ∈ ( 0 [,] 1 ) )
59 eqeq2 ⊢ ( 1 = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) → ( 𝑥 = 1 ↔ 𝑥 = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ) )
60 59 bibi1d ⊢ ( 1 = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) → ( ( 𝑥 = 1 ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ↔ ( 𝑥 = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ) )
61 eqeq2 ⊢ ( ( 𝑦 / ( 1 + 𝑦 ) ) = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) → ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑥 = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ) )
62 61 bibi1d ⊢ ( ( 𝑦 / ( 1 + 𝑦 ) ) = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) → ( ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ↔ ( 𝑥 = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ) )
63 simpr ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → 𝑦 = +∞ )
64 iftrue ⊢ ( 𝑥 = 1 → if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) = +∞ )
65 64 eqeq2d ⊢ ( 𝑥 = 1 → ( 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ↔ 𝑦 = +∞ ) )
66 63 65 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑥 = 1 → 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) )
67 pnfnre ⊢ +∞ ∉ ℝ
68 neleq1 ⊢ ( 𝑦 = +∞ → ( 𝑦 ∉ ℝ ↔ +∞ ∉ ℝ ) )
69 68 adantl ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑦 ∉ ℝ ↔ +∞ ∉ ℝ ) )
70 67 69 mpbiri ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → 𝑦 ∉ ℝ )
71 neleq1 ⊢ ( 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) → ( 𝑦 ∉ ℝ ↔ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∉ ℝ ) )
72 70 71 syl5ibcom ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) → if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∉ ℝ ) )
73 df-nel ⊢ ( if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∉ ℝ ↔ ¬ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∈ ℝ )
74 iffalse ⊢ ( ¬ 𝑥 = 1 → if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) = ( 𝑥 / ( 1 − 𝑥 ) ) )
75 74 adantl ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 1 ) → if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) = ( 𝑥 / ( 1 − 𝑥 ) ) )
76 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
77 76 30 sselid ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 1 ) → ( 𝑥 / ( 1 − 𝑥 ) ) ∈ ℝ )
78 75 77 eqeltrd ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 1 ) → if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∈ ℝ )
79 78 ex ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( ¬ 𝑥 = 1 → if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∈ ℝ ) )
80 79 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( ¬ 𝑥 = 1 → if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∈ ℝ ) )
81 80 con1d ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( ¬ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∈ ℝ → 𝑥 = 1 ) )
82 73 81 biimtrid ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ∉ ℝ → 𝑥 = 1 ) )
83 72 82 syld ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) → 𝑥 = 1 ) )
84 66 83 impbid ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑥 = 1 ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) )
85 eqeq2 ⊢ ( +∞ = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) → ( 𝑦 = +∞ ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) )
86 85 bibi2d ⊢ ( +∞ = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) → ( ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = +∞ ) ↔ ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ) )
87 eqeq2 ⊢ ( ( 𝑥 / ( 1 − 𝑥 ) ) = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) → ( 𝑦 = ( 𝑥 / ( 1 − 𝑥 ) ) ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) )
88 87 bibi2d ⊢ ( ( 𝑥 / ( 1 − 𝑥 ) ) = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) → ( ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = ( 𝑥 / ( 1 − 𝑥 ) ) ) ↔ ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ) )
89 0re ⊢ 0 ∈ ℝ
90 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ( 0 [,) 1 ) ↔ ( ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑦 / ( 1 + 𝑦 ) ) ∧ ( 𝑦 / ( 1 + 𝑦 ) ) < 1 ) ) )
91 89 9 90 mp2an ⊢ ( ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ( 0 [,) 1 ) ↔ ( ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑦 / ( 1 + 𝑦 ) ) ∧ ( 𝑦 / ( 1 + 𝑦 ) ) < 1 ) )
92 55 91 sylib ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → ( ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑦 / ( 1 + 𝑦 ) ) ∧ ( 𝑦 / ( 1 + 𝑦 ) ) < 1 ) )
93 92 simp1d ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → ( 𝑦 / ( 1 + 𝑦 ) ) ∈ ℝ )
94 92 simp3d ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → ( 𝑦 / ( 1 + 𝑦 ) ) < 1 )
95 93 94 gtned ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → 1 ≠ ( 𝑦 / ( 1 + 𝑦 ) ) )
96 95 adantll ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) → 1 ≠ ( 𝑦 / ( 1 + 𝑦 ) ) )
97 96 neneqd ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) → ¬ 1 = ( 𝑦 / ( 1 + 𝑦 ) ) )
98 eqeq1 ⊢ ( 𝑥 = 1 → ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 1 = ( 𝑦 / ( 1 + 𝑦 ) ) ) )
99 98 notbid ⊢ ( 𝑥 = 1 → ( ¬ 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ ¬ 1 = ( 𝑦 / ( 1 + 𝑦 ) ) ) )
100 97 99 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) → ( 𝑥 = 1 → ¬ 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ) )
101 100 imp ⊢ ( ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) ∧ 𝑥 = 1 ) → ¬ 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) )
102 simplr ⊢ ( ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) ∧ 𝑥 = 1 ) → ¬ 𝑦 = +∞ )
103 101 102 2falsed ⊢ ( ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) ∧ 𝑥 = 1 ) → ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = +∞ ) )
104 f1ocnvfvb ⊢ ( ( ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ ) ∧ 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ( ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑥 ) = 𝑦 ↔ ( ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑦 ) = 𝑥 ) )
105 24 104 mp3an1 ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ( ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑥 ) = 𝑦 ↔ ( ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑦 ) = 𝑥 ) )
106 simpl ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → 𝑥 ∈ ( 0 [,) 1 ) )
107 ovex ⊢ ( 𝑥 / ( 1 − 𝑥 ) ) ∈ V
108 22 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ ( 𝑥 / ( 1 − 𝑥 ) ) ∈ V ) → ( ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑥 ) = ( 𝑥 / ( 1 − 𝑥 ) ) )
109 106 107 108 sylancl ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑥 ) = ( 𝑥 / ( 1 − 𝑥 ) ) )
110 109 eqeq1d ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ( ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑥 ) = 𝑦 ↔ ( 𝑥 / ( 1 − 𝑥 ) ) = 𝑦 ) )
111 simpr ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → 𝑦 ∈ ( 0 [,) +∞ ) )
112 ovex ⊢ ( 𝑦 / ( 1 + 𝑦 ) ) ∈ V
113 51 fvmpt2 ⊢ ( ( 𝑦 ∈ ( 0 [,) +∞ ) ∧ ( 𝑦 / ( 1 + 𝑦 ) ) ∈ V ) → ( ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑦 ) = ( 𝑦 / ( 1 + 𝑦 ) ) )
114 111 112 113 sylancl ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑦 ) = ( 𝑦 / ( 1 + 𝑦 ) ) )
115 114 eqeq1d ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ( ◡ ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) ) ‘ 𝑦 ) = 𝑥 ↔ ( 𝑦 / ( 1 + 𝑦 ) ) = 𝑥 ) )
116 105 110 115 3bitr3rd ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑦 / ( 1 + 𝑦 ) ) = 𝑥 ↔ ( 𝑥 / ( 1 − 𝑥 ) ) = 𝑦 ) )
117 eqcom ⊢ ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ ( 𝑦 / ( 1 + 𝑦 ) ) = 𝑥 )
118 eqcom ⊢ ( 𝑦 = ( 𝑥 / ( 1 − 𝑥 ) ) ↔ ( 𝑥 / ( 1 − 𝑥 ) ) = 𝑦 )
119 116 117 118 3bitr4g ⊢ ( ( 𝑥 ∈ ( 0 [,) 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = ( 𝑥 / ( 1 − 𝑥 ) ) ) )
120 21 47 119 syl2an ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 1 ) ∧ ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) ) → ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = ( 𝑥 / ( 1 − 𝑥 ) ) ) )
121 120 an4s ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ( ¬ 𝑥 = 1 ∧ ¬ 𝑦 = +∞ ) ) → ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = ( 𝑥 / ( 1 − 𝑥 ) ) ) )
122 121 anass1rs ⊢ ( ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) ∧ ¬ 𝑥 = 1 ) → ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = ( 𝑥 / ( 1 − 𝑥 ) ) ) )
123 86 88 103 122 ifbothda ⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) → ( 𝑥 = ( 𝑦 / ( 1 + 𝑦 ) ) ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) )
124 60 62 84 123 ifbothda ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) )
125 124 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑥 = if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ↔ 𝑦 = if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) )
126 1 33 58 125 f1ocnv2d ⊢ ( ⊤ → ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ) ) )
127 126 mptru ⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑦 = +∞ , 1 , ( 𝑦 / ( 1 + 𝑦 ) ) ) ) )