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 syl5bi ( ( ( 𝑥 ∈ ( 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 + 𝑦 ) ) ) ) )