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 = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )
Assertion iccpnfcnv 
|- ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ `' F = ( y e. ( 0 [,] +oo ) |-> if ( y = +oo , 1 , ( y / ( 1 + y ) ) ) ) )

Proof

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