# 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 ${⊢}{F}=\left({x}\in \left[0,1\right]⟼if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
Assertion 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)$

### 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 0xr ${⊢}0\in {ℝ}^{*}$
3 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
4 0lepnf ${⊢}0\le \mathrm{+\infty }$
5 ubicc2 ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge 0\le \mathrm{+\infty }\right)\to \mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$
6 2 3 4 5 mp3an ${⊢}\mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$
7 6 a1i ${⊢}\left({x}\in \left[0,1\right]\wedge {x}=1\right)\to \mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$
8 icossicc ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$
9 1xr ${⊢}1\in {ℝ}^{*}$
10 0le1 ${⊢}0\le 1$
11 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]$
12 2 9 10 11 mp3an ${⊢}\left[0,1\right)\cup \left\{1\right\}=\left[0,1\right]$
13 12 eleq2i ${⊢}{x}\in \left(\left[0,1\right)\cup \left\{1\right\}\right)↔{x}\in \left[0,1\right]$
14 elun ${⊢}{x}\in \left(\left[0,1\right)\cup \left\{1\right\}\right)↔\left({x}\in \left[0,1\right)\vee {x}\in \left\{1\right\}\right)$
15 13 14 bitr3i ${⊢}{x}\in \left[0,1\right]↔\left({x}\in \left[0,1\right)\vee {x}\in \left\{1\right\}\right)$
16 pm2.53 ${⊢}\left({x}\in \left[0,1\right)\vee {x}\in \left\{1\right\}\right)\to \left(¬{x}\in \left[0,1\right)\to {x}\in \left\{1\right\}\right)$
17 15 16 sylbi ${⊢}{x}\in \left[0,1\right]\to \left(¬{x}\in \left[0,1\right)\to {x}\in \left\{1\right\}\right)$
18 elsni ${⊢}{x}\in \left\{1\right\}\to {x}=1$
19 17 18 syl6 ${⊢}{x}\in \left[0,1\right]\to \left(¬{x}\in \left[0,1\right)\to {x}=1\right)$
20 19 con1d ${⊢}{x}\in \left[0,1\right]\to \left(¬{x}=1\to {x}\in \left[0,1\right)\right)$
21 20 imp ${⊢}\left({x}\in \left[0,1\right]\wedge ¬{x}=1\right)\to {x}\in \left[0,1\right)$
22 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)$
23 22 icopnfcnv ${⊢}\left(\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right):\left[0,1\right)\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\wedge {\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}=\left({y}\in \left[0,\mathrm{+\infty }\right)⟼\frac{{y}}{1+{y}}\right)\right)$
24 23 simpli ${⊢}\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right):\left[0,1\right)\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)$
25 f1of ${⊢}\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right):\left[0,1\right)\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\to \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right):\left[0,1\right)⟶\left[0,\mathrm{+\infty }\right)$
26 24 25 ax-mp ${⊢}\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right):\left[0,1\right)⟶\left[0,\mathrm{+\infty }\right)$
27 22 fmpt ${⊢}\forall {x}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\frac{{x}}{1-{x}}\in \left[0,\mathrm{+\infty }\right)↔\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right):\left[0,1\right)⟶\left[0,\mathrm{+\infty }\right)$
28 26 27 mpbir ${⊢}\forall {x}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\frac{{x}}{1-{x}}\in \left[0,\mathrm{+\infty }\right)$
29 28 rspec ${⊢}{x}\in \left[0,1\right)\to \frac{{x}}{1-{x}}\in \left[0,\mathrm{+\infty }\right)$
30 21 29 syl ${⊢}\left({x}\in \left[0,1\right]\wedge ¬{x}=1\right)\to \frac{{x}}{1-{x}}\in \left[0,\mathrm{+\infty }\right)$
31 8 30 sseldi ${⊢}\left({x}\in \left[0,1\right]\wedge ¬{x}=1\right)\to \frac{{x}}{1-{x}}\in \left[0,\mathrm{+\infty }\right]$
32 7 31 ifclda ${⊢}{x}\in \left[0,1\right]\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\in \left[0,\mathrm{+\infty }\right]$
33 32 adantl ${⊢}\left(\top \wedge {x}\in \left[0,1\right]\right)\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\in \left[0,\mathrm{+\infty }\right]$
34 1elunit ${⊢}1\in \left[0,1\right]$
35 34 a1i ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right]\wedge {y}=\mathrm{+\infty }\right)\to 1\in \left[0,1\right]$
36 icossicc ${⊢}\left[0,1\right)\subseteq \left[0,1\right]$
37 snunico ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge 0\le \mathrm{+\infty }\right)\to \left[0,\mathrm{+\infty }\right)\cup \left\{\mathrm{+\infty }\right\}=\left[0,\mathrm{+\infty }\right]$
38 2 3 4 37 mp3an ${⊢}\left[0,\mathrm{+\infty }\right)\cup \left\{\mathrm{+\infty }\right\}=\left[0,\mathrm{+\infty }\right]$
39 38 eleq2i ${⊢}{y}\in \left(\left[0,\mathrm{+\infty }\right)\cup \left\{\mathrm{+\infty }\right\}\right)↔{y}\in \left[0,\mathrm{+\infty }\right]$
40 elun ${⊢}{y}\in \left(\left[0,\mathrm{+\infty }\right)\cup \left\{\mathrm{+\infty }\right\}\right)↔\left({y}\in \left[0,\mathrm{+\infty }\right)\vee {y}\in \left\{\mathrm{+\infty }\right\}\right)$
41 39 40 bitr3i ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]↔\left({y}\in \left[0,\mathrm{+\infty }\right)\vee {y}\in \left\{\mathrm{+\infty }\right\}\right)$
42 pm2.53 ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right)\vee {y}\in \left\{\mathrm{+\infty }\right\}\right)\to \left(¬{y}\in \left[0,\mathrm{+\infty }\right)\to {y}\in \left\{\mathrm{+\infty }\right\}\right)$
43 41 42 sylbi ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]\to \left(¬{y}\in \left[0,\mathrm{+\infty }\right)\to {y}\in \left\{\mathrm{+\infty }\right\}\right)$
44 elsni ${⊢}{y}\in \left\{\mathrm{+\infty }\right\}\to {y}=\mathrm{+\infty }$
45 43 44 syl6 ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]\to \left(¬{y}\in \left[0,\mathrm{+\infty }\right)\to {y}=\mathrm{+\infty }\right)$
46 45 con1d ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]\to \left(¬{y}=\mathrm{+\infty }\to {y}\in \left[0,\mathrm{+\infty }\right)\right)$
47 46 imp ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right]\wedge ¬{y}=\mathrm{+\infty }\right)\to {y}\in \left[0,\mathrm{+\infty }\right)$
48 f1ocnv ${⊢}\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right):\left[0,1\right)\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\to {\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}:\left[0,\mathrm{+\infty }\right)\underset{1-1 onto}{⟶}\left[0,1\right)$
49 f1of ${⊢}{\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}:\left[0,\mathrm{+\infty }\right)\underset{1-1 onto}{⟶}\left[0,1\right)\to {\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}:\left[0,\mathrm{+\infty }\right)⟶\left[0,1\right)$
50 24 48 49 mp2b ${⊢}{\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}:\left[0,\mathrm{+\infty }\right)⟶\left[0,1\right)$
51 23 simpri ${⊢}{\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}=\left({y}\in \left[0,\mathrm{+\infty }\right)⟼\frac{{y}}{1+{y}}\right)$
52 51 fmpt ${⊢}\forall {y}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\frac{{y}}{1+{y}}\in \left[0,1\right)↔{\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}:\left[0,\mathrm{+\infty }\right)⟶\left[0,1\right)$
53 50 52 mpbir ${⊢}\forall {y}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\frac{{y}}{1+{y}}\in \left[0,1\right)$
54 53 rspec ${⊢}{y}\in \left[0,\mathrm{+\infty }\right)\to \frac{{y}}{1+{y}}\in \left[0,1\right)$
55 47 54 syl ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right]\wedge ¬{y}=\mathrm{+\infty }\right)\to \frac{{y}}{1+{y}}\in \left[0,1\right)$
56 36 55 sseldi ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right]\wedge ¬{y}=\mathrm{+\infty }\right)\to \frac{{y}}{1+{y}}\in \left[0,1\right]$
57 35 56 ifclda ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]\to if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)\in \left[0,1\right]$
58 57 adantl ${⊢}\left(\top \wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)\in \left[0,1\right]$
59 eqeq2 ${⊢}1=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)\to \left({x}=1↔{x}=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)\right)$
60 59 bibi1d ${⊢}1=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)\to \left(\left({x}=1↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)↔\left({x}=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)\right)$
61 eqeq2 ${⊢}\frac{{y}}{1+{y}}=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)\to \left({x}=\frac{{y}}{1+{y}}↔{x}=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)\right)$
62 61 bibi1d ${⊢}\frac{{y}}{1+{y}}=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)\to \left(\left({x}=\frac{{y}}{1+{y}}↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)↔\left({x}=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)\right)$
63 simpr ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to {y}=\mathrm{+\infty }$
64 iftrue ${⊢}{x}=1\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)=\mathrm{+\infty }$
65 64 eqeq2d ${⊢}{x}=1\to \left({y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)↔{y}=\mathrm{+\infty }\right)$
66 63 65 syl5ibrcom ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to \left({x}=1\to {y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
67 pnfnre ${⊢}\mathrm{+\infty }\notin ℝ$
68 neleq1 ${⊢}{y}=\mathrm{+\infty }\to \left({y}\notin ℝ↔\mathrm{+\infty }\notin ℝ\right)$
69 68 adantl ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to \left({y}\notin ℝ↔\mathrm{+\infty }\notin ℝ\right)$
70 67 69 mpbiri ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to {y}\notin ℝ$
71 neleq1 ${⊢}{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\to \left({y}\notin ℝ↔if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\notin ℝ\right)$
72 70 71 syl5ibcom ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to \left({y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\notin ℝ\right)$
73 df-nel ${⊢}if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\notin ℝ↔¬if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\in ℝ$
74 iffalse ${⊢}¬{x}=1\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)=\frac{{x}}{1-{x}}$
75 74 adantl ${⊢}\left({x}\in \left[0,1\right]\wedge ¬{x}=1\right)\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)=\frac{{x}}{1-{x}}$
76 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
77 76 30 sseldi ${⊢}\left({x}\in \left[0,1\right]\wedge ¬{x}=1\right)\to \frac{{x}}{1-{x}}\in ℝ$
78 75 77 eqeltrd ${⊢}\left({x}\in \left[0,1\right]\wedge ¬{x}=1\right)\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\in ℝ$
79 78 ex ${⊢}{x}\in \left[0,1\right]\to \left(¬{x}=1\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\in ℝ\right)$
80 79 ad2antrr ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to \left(¬{x}=1\to if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\in ℝ\right)$
81 80 con1d ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to \left(¬if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\in ℝ\to {x}=1\right)$
82 73 81 syl5bi ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to \left(if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\notin ℝ\to {x}=1\right)$
83 72 82 syld ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to \left({y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\to {x}=1\right)$
84 66 83 impbid ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {y}=\mathrm{+\infty }\right)\to \left({x}=1↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
85 eqeq2 ${⊢}\mathrm{+\infty }=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\to \left({y}=\mathrm{+\infty }↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
86 85 bibi2d ${⊢}\mathrm{+\infty }=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\to \left(\left({x}=\frac{{y}}{1+{y}}↔{y}=\mathrm{+\infty }\right)↔\left({x}=\frac{{y}}{1+{y}}↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)\right)$
87 eqeq2 ${⊢}\frac{{x}}{1-{x}}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\to \left({y}=\frac{{x}}{1-{x}}↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
88 87 bibi2d ${⊢}\frac{{x}}{1-{x}}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\to \left(\left({x}=\frac{{y}}{1+{y}}↔{y}=\frac{{x}}{1-{x}}\right)↔\left({x}=\frac{{y}}{1+{y}}↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)\right)$
89 0re ${⊢}0\in ℝ$
90 elico2 ${⊢}\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)\to \left(\frac{{y}}{1+{y}}\in \left[0,1\right)↔\left(\frac{{y}}{1+{y}}\in ℝ\wedge 0\le \frac{{y}}{1+{y}}\wedge \frac{{y}}{1+{y}}<1\right)\right)$
91 89 9 90 mp2an ${⊢}\frac{{y}}{1+{y}}\in \left[0,1\right)↔\left(\frac{{y}}{1+{y}}\in ℝ\wedge 0\le \frac{{y}}{1+{y}}\wedge \frac{{y}}{1+{y}}<1\right)$
92 55 91 sylib ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right]\wedge ¬{y}=\mathrm{+\infty }\right)\to \left(\frac{{y}}{1+{y}}\in ℝ\wedge 0\le \frac{{y}}{1+{y}}\wedge \frac{{y}}{1+{y}}<1\right)$
93 92 simp1d ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right]\wedge ¬{y}=\mathrm{+\infty }\right)\to \frac{{y}}{1+{y}}\in ℝ$
94 92 simp3d ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right]\wedge ¬{y}=\mathrm{+\infty }\right)\to \frac{{y}}{1+{y}}<1$
95 93 94 gtned ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right]\wedge ¬{y}=\mathrm{+\infty }\right)\to 1\ne \frac{{y}}{1+{y}}$
96 95 adantll ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{y}=\mathrm{+\infty }\right)\to 1\ne \frac{{y}}{1+{y}}$
97 96 neneqd ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{y}=\mathrm{+\infty }\right)\to ¬1=\frac{{y}}{1+{y}}$
98 eqeq1 ${⊢}{x}=1\to \left({x}=\frac{{y}}{1+{y}}↔1=\frac{{y}}{1+{y}}\right)$
99 98 notbid ${⊢}{x}=1\to \left(¬{x}=\frac{{y}}{1+{y}}↔¬1=\frac{{y}}{1+{y}}\right)$
100 97 99 syl5ibrcom ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{y}=\mathrm{+\infty }\right)\to \left({x}=1\to ¬{x}=\frac{{y}}{1+{y}}\right)$
101 100 imp ${⊢}\left(\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{y}=\mathrm{+\infty }\right)\wedge {x}=1\right)\to ¬{x}=\frac{{y}}{1+{y}}$
102 simplr ${⊢}\left(\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{y}=\mathrm{+\infty }\right)\wedge {x}=1\right)\to ¬{y}=\mathrm{+\infty }$
103 101 102 2falsed ${⊢}\left(\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{y}=\mathrm{+\infty }\right)\wedge {x}=1\right)\to \left({x}=\frac{{y}}{1+{y}}↔{y}=\mathrm{+\infty }\right)$
104 f1ocnvfvb ${⊢}\left(\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right):\left[0,1\right)\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\wedge {x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to \left(\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({x}\right)={y}↔{\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}\left({y}\right)={x}\right)$
105 24 104 mp3an1 ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to \left(\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({x}\right)={y}↔{\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}\left({y}\right)={x}\right)$
106 simpl ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to {x}\in \left[0,1\right)$
107 ovex ${⊢}\frac{{x}}{1-{x}}\in \mathrm{V}$
108 22 fvmpt2 ${⊢}\left({x}\in \left[0,1\right)\wedge \frac{{x}}{1-{x}}\in \mathrm{V}\right)\to \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({x}\right)=\frac{{x}}{1-{x}}$
109 106 107 108 sylancl ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to \left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({x}\right)=\frac{{x}}{1-{x}}$
110 109 eqeq1d ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to \left(\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)\left({x}\right)={y}↔\frac{{x}}{1-{x}}={y}\right)$
111 simpr ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to {y}\in \left[0,\mathrm{+\infty }\right)$
112 ovex ${⊢}\frac{{y}}{1+{y}}\in \mathrm{V}$
113 51 fvmpt2 ${⊢}\left({y}\in \left[0,\mathrm{+\infty }\right)\wedge \frac{{y}}{1+{y}}\in \mathrm{V}\right)\to {\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}\left({y}\right)=\frac{{y}}{1+{y}}$
114 111 112 113 sylancl ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to {\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}\left({y}\right)=\frac{{y}}{1+{y}}$
115 114 eqeq1d ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to \left({\left({x}\in \left[0,1\right)⟼\frac{{x}}{1-{x}}\right)}^{-1}\left({y}\right)={x}↔\frac{{y}}{1+{y}}={x}\right)$
116 105 110 115 3bitr3rd ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to \left(\frac{{y}}{1+{y}}={x}↔\frac{{x}}{1-{x}}={y}\right)$
117 eqcom ${⊢}{x}=\frac{{y}}{1+{y}}↔\frac{{y}}{1+{y}}={x}$
118 eqcom ${⊢}{y}=\frac{{x}}{1-{x}}↔\frac{{x}}{1-{x}}={y}$
119 116 117 118 3bitr4g ${⊢}\left({x}\in \left[0,1\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to \left({x}=\frac{{y}}{1+{y}}↔{y}=\frac{{x}}{1-{x}}\right)$
120 21 47 119 syl2an ${⊢}\left(\left({x}\in \left[0,1\right]\wedge ¬{x}=1\right)\wedge \left({y}\in \left[0,\mathrm{+\infty }\right]\wedge ¬{y}=\mathrm{+\infty }\right)\right)\to \left({x}=\frac{{y}}{1+{y}}↔{y}=\frac{{x}}{1-{x}}\right)$
121 120 an4s ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge \left(¬{x}=1\wedge ¬{y}=\mathrm{+\infty }\right)\right)\to \left({x}=\frac{{y}}{1+{y}}↔{y}=\frac{{x}}{1-{x}}\right)$
122 121 anass1rs ${⊢}\left(\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{y}=\mathrm{+\infty }\right)\wedge ¬{x}=1\right)\to \left({x}=\frac{{y}}{1+{y}}↔{y}=\frac{{x}}{1-{x}}\right)$
123 86 88 103 122 ifbothda ${⊢}\left(\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{y}=\mathrm{+\infty }\right)\to \left({x}=\frac{{y}}{1+{y}}↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
124 60 62 84 123 ifbothda ${⊢}\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({x}=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
125 124 adantl ${⊢}\left(\top \wedge \left({x}\in \left[0,1\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({x}=if\left({y}=\mathrm{+\infty },1,\frac{{y}}{1+{y}}\right)↔{y}=if\left({x}=1,\mathrm{+\infty },\frac{{x}}{1-{x}}\right)\right)$
126 1 33 58 125 f1ocnv2d ${⊢}\top \to \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)$
127 126 mptru ${⊢}\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)$