MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iccpnfcnv Structured version   Unicode version

Theorem iccpnfcnv 21172
Description: Define a bijection from  [ 0 ,  1 ] to  [
0 , +oo ]. (Contributed by Mario Carneiro, 9-Sep-2015.)
Hypothesis
Ref Expression
iccpnfhmeo.f  |-  F  =  ( x  e.  ( 0 [,] 1 ) 
|->  if ( x  =  1 , +oo , 
( x  /  (
1  -  x ) ) ) )
Assertion
Ref Expression
iccpnfcnv  |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo )  /\  `' F  =  ( y  e.  ( 0 [,] +oo )  |->  if ( y  = +oo ,  1 ,  ( y  /  (
1  +  y ) ) ) ) )
Distinct variable groups:    x, y    y, F
Allowed substitution hint:    F( x)

Proof of Theorem iccpnfcnv
StepHypRef Expression
1 iccpnfhmeo.f . . 3  |-  F  =  ( x  e.  ( 0 [,] 1 ) 
|->  if ( x  =  1 , +oo , 
( x  /  (
1  -  x ) ) ) )
2 0xr 9629 . . . . . . 7  |-  0  e.  RR*
3 pnfxr 11310 . . . . . . 7  |- +oo  e.  RR*
4 0lepnf 11329 . . . . . . 7  |-  0  <_ +oo
5 ubicc2 11626 . . . . . . 7  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  <_ +oo )  -> +oo  e.  ( 0 [,] +oo ) )
62, 3, 4, 5mp3an 1319 . . . . . 6  |- +oo  e.  ( 0 [,] +oo )
76a1i 11 . . . . 5  |-  ( ( x  e.  ( 0 [,] 1 )  /\  x  =  1 )  -> +oo  e.  (
0 [,] +oo )
)
8 ssun1 3660 . . . . . . 7  |-  ( 0 [,) +oo )  C_  ( ( 0 [,) +oo )  u.  { +oo } )
9 snunico 11636 . . . . . . . 8  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  <_ +oo )  ->  ( ( 0 [,) +oo )  u.  { +oo } )  =  ( 0 [,] +oo ) )
102, 3, 4, 9mp3an 1319 . . . . . . 7  |-  ( ( 0 [,) +oo )  u.  { +oo } )  =  ( 0 [,] +oo )
118, 10sseqtri 3529 . . . . . 6  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
12 1re 9584 . . . . . . . . . . . . . . 15  |-  1  e.  RR
1312rexri 9635 . . . . . . . . . . . . . 14  |-  1  e.  RR*
14 0le1 10065 . . . . . . . . . . . . . 14  |-  0  <_  1
15 snunico 11636 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR*  /\  1  e.  RR*  /\  0  <_ 
1 )  ->  (
( 0 [,) 1
)  u.  { 1 } )  =  ( 0 [,] 1 ) )
162, 13, 14, 15mp3an 1319 . . . . . . . . . . . . 13  |-  ( ( 0 [,) 1 )  u.  { 1 } )  =  ( 0 [,] 1 )
1716eleq2i 2538 . . . . . . . . . . . 12  |-  ( x  e.  ( ( 0 [,) 1 )  u. 
{ 1 } )  <-> 
x  e.  ( 0 [,] 1 ) )
18 elun 3638 . . . . . . . . . . . 12  |-  ( x  e.  ( ( 0 [,) 1 )  u. 
{ 1 } )  <-> 
( x  e.  ( 0 [,) 1 )  \/  x  e.  {
1 } ) )
1917, 18bitr3i 251 . . . . . . . . . . 11  |-  ( x  e.  ( 0 [,] 1 )  <->  ( x  e.  ( 0 [,) 1
)  \/  x  e. 
{ 1 } ) )
20 pm2.53 373 . . . . . . . . . . 11  |-  ( ( x  e.  ( 0 [,) 1 )  \/  x  e.  { 1 } )  ->  ( -.  x  e.  (
0 [,) 1 )  ->  x  e.  {
1 } ) )
2119, 20sylbi 195 . . . . . . . . . 10  |-  ( x  e.  ( 0 [,] 1 )  ->  ( -.  x  e.  (
0 [,) 1 )  ->  x  e.  {
1 } ) )
22 elsni 4045 . . . . . . . . . 10  |-  ( x  e.  { 1 }  ->  x  =  1 )
2321, 22syl6 33 . . . . . . . . 9  |-  ( x  e.  ( 0 [,] 1 )  ->  ( -.  x  e.  (
0 [,) 1 )  ->  x  =  1 ) )
2423con1d 124 . . . . . . . 8  |-  ( x  e.  ( 0 [,] 1 )  ->  ( -.  x  =  1  ->  x  e.  ( 0 [,) 1 ) ) )
2524imp 429 . . . . . . 7  |-  ( ( x  e.  ( 0 [,] 1 )  /\  -.  x  =  1
)  ->  x  e.  ( 0 [,) 1
) )
26 eqid 2460 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) )  =  ( x  e.  ( 0 [,) 1
)  |->  ( x  / 
( 1  -  x
) ) )
2726icopnfcnv 21170 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
2827simpli 458 . . . . . . . . . 10  |-  ( x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) ) : ( 0 [,) 1 ) -1-1-onto-> ( 0 [,) +oo )
29 f1of 5807 . . . . . . . . . 10  |-  ( ( 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 ) )
3028, 29ax-mp 5 . . . . . . . . 9  |-  ( x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) ) : ( 0 [,) 1 ) --> ( 0 [,) +oo )
3126fmpt 6033 . . . . . . . . 9  |-  ( A. x  e.  ( 0 [,) 1 ) ( x  /  ( 1  -  x ) )  e.  ( 0 [,) +oo )  <->  ( x  e.  ( 0 [,) 1
)  |->  ( x  / 
( 1  -  x
) ) ) : ( 0 [,) 1
) --> ( 0 [,) +oo ) )
3230, 31mpbir 209 . . . . . . . 8  |-  A. x  e.  ( 0 [,) 1
) ( x  / 
( 1  -  x
) )  e.  ( 0 [,) +oo )
3332rspec 2825 . . . . . . 7  |-  ( x  e.  ( 0 [,) 1 )  ->  (
x  /  ( 1  -  x ) )  e.  ( 0 [,) +oo ) )
3425, 33syl 16 . . . . . 6  |-  ( ( x  e.  ( 0 [,] 1 )  /\  -.  x  =  1
)  ->  ( x  /  ( 1  -  x ) )  e.  ( 0 [,) +oo ) )
3511, 34sseldi 3495 . . . . 5  |-  ( ( x  e.  ( 0 [,] 1 )  /\  -.  x  =  1
)  ->  ( x  /  ( 1  -  x ) )  e.  ( 0 [,] +oo ) )
367, 35ifclda 3964 . . . 4  |-  ( x  e.  ( 0 [,] 1 )  ->  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  e.  ( 0 [,] +oo ) )
3736adantl 466 . . 3  |-  ( ( T.  /\  x  e.  ( 0 [,] 1
) )  ->  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  e.  ( 0 [,] +oo ) )
38 1elunit 11628 . . . . . 6  |-  1  e.  ( 0 [,] 1
)
3938a1i 11 . . . . 5  |-  ( ( y  e.  ( 0 [,] +oo )  /\  y  = +oo )  ->  1  e.  ( 0 [,] 1 ) )
40 ssun1 3660 . . . . . . 7  |-  ( 0 [,) 1 )  C_  ( ( 0 [,) 1 )  u.  {
1 } )
4140, 16sseqtri 3529 . . . . . 6  |-  ( 0 [,) 1 )  C_  ( 0 [,] 1
)
4210eleq2i 2538 . . . . . . . . . . . 12  |-  ( y  e.  ( ( 0 [,) +oo )  u. 
{ +oo } )  <->  y  e.  ( 0 [,] +oo ) )
43 elun 3638 . . . . . . . . . . . 12  |-  ( y  e.  ( ( 0 [,) +oo )  u. 
{ +oo } )  <->  ( y  e.  ( 0 [,) +oo )  \/  y  e.  { +oo } ) )
4442, 43bitr3i 251 . . . . . . . . . . 11  |-  ( y  e.  ( 0 [,] +oo )  <->  ( y  e.  ( 0 [,) +oo )  \/  y  e.  { +oo } ) )
45 pm2.53 373 . . . . . . . . . . 11  |-  ( ( y  e.  ( 0 [,) +oo )  \/  y  e.  { +oo } )  ->  ( -.  y  e.  ( 0 [,) +oo )  -> 
y  e.  { +oo } ) )
4644, 45sylbi 195 . . . . . . . . . 10  |-  ( y  e.  ( 0 [,] +oo )  ->  ( -.  y  e.  ( 0 [,) +oo )  -> 
y  e.  { +oo } ) )
47 elsni 4045 . . . . . . . . . 10  |-  ( y  e.  { +oo }  ->  y  = +oo )
4846, 47syl6 33 . . . . . . . . 9  |-  ( y  e.  ( 0 [,] +oo )  ->  ( -.  y  e.  ( 0 [,) +oo )  -> 
y  = +oo )
)
4948con1d 124 . . . . . . . 8  |-  ( y  e.  ( 0 [,] +oo )  ->  ( -.  y  = +oo  ->  y  e.  ( 0 [,) +oo ) ) )
5049imp 429 . . . . . . 7  |-  ( ( y  e.  ( 0 [,] +oo )  /\  -.  y  = +oo )  ->  y  e.  ( 0 [,) +oo )
)
51 f1ocnv 5819 . . . . . . . . . 10  |-  ( ( 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
) )
52 f1of 5807 . . . . . . . . . 10  |-  ( `' ( 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 ) )
5328, 51, 52mp2b 10 . . . . . . . . 9  |-  `' ( x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) ) : ( 0 [,) +oo ) --> ( 0 [,) 1 )
5427simpri 462 . . . . . . . . . 10  |-  `' ( x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) )  =  ( y  e.  ( 0 [,) +oo )  |->  ( y  /  ( 1  +  y ) ) )
5554fmpt 6033 . . . . . . . . 9  |-  ( A. y  e.  ( 0 [,) +oo ) ( y  /  ( 1  +  y ) )  e.  ( 0 [,) 1 )  <->  `' (
x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) ) : ( 0 [,) +oo ) --> ( 0 [,) 1 ) )
5653, 55mpbir 209 . . . . . . . 8  |-  A. y  e.  ( 0 [,) +oo ) ( y  / 
( 1  +  y ) )  e.  ( 0 [,) 1 )
5756rspec 2825 . . . . . . 7  |-  ( y  e.  ( 0 [,) +oo )  ->  ( y  /  ( 1  +  y ) )  e.  ( 0 [,) 1
) )
5850, 57syl 16 . . . . . 6  |-  ( ( y  e.  ( 0 [,] +oo )  /\  -.  y  = +oo )  ->  ( y  / 
( 1  +  y ) )  e.  ( 0 [,) 1 ) )
5941, 58sseldi 3495 . . . . 5  |-  ( ( y  e.  ( 0 [,] +oo )  /\  -.  y  = +oo )  ->  ( y  / 
( 1  +  y ) )  e.  ( 0 [,] 1 ) )
6039, 59ifclda 3964 . . . 4  |-  ( y  e.  ( 0 [,] +oo )  ->  if ( y  = +oo , 
1 ,  ( y  /  ( 1  +  y ) ) )  e.  ( 0 [,] 1 ) )
6160adantl 466 . . 3  |-  ( ( T.  /\  y  e.  ( 0 [,] +oo ) )  ->  if ( y  = +oo ,  1 ,  ( y  /  ( 1  +  y ) ) )  e.  ( 0 [,] 1 ) )
62 eqeq2 2475 . . . . . 6  |-  ( 1  =  if ( y  = +oo ,  1 ,  ( y  / 
( 1  +  y ) ) )  -> 
( x  =  1  <-> 
x  =  if ( y  = +oo , 
1 ,  ( y  /  ( 1  +  y ) ) ) ) )
6362bibi1d 319 . . . . 5  |-  ( 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 ) ) ) ) ) )
64 eqeq2 2475 . . . . . 6  |-  ( ( y  /  ( 1  +  y ) )  =  if ( y  = +oo ,  1 ,  ( y  / 
( 1  +  y ) ) )  -> 
( x  =  ( y  /  ( 1  +  y ) )  <-> 
x  =  if ( y  = +oo , 
1 ,  ( y  /  ( 1  +  y ) ) ) ) )
6564bibi1d 319 . . . . 5  |-  ( ( 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 ) ) ) ) ) )
66 simpr 461 . . . . . . 7  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  y  = +oo )  ->  y  = +oo )
67 iftrue 3938 . . . . . . . 8  |-  ( x  =  1  ->  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  = +oo )
6867eqeq2d 2474 . . . . . . 7  |-  ( x  =  1  ->  (
y  =  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  <-> 
y  = +oo )
)
6966, 68syl5ibrcom 222 . . . . . 6  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  y  = +oo )  ->  ( x  =  1  ->  y  =  if ( x  =  1 , +oo , 
( x  /  (
1  -  x ) ) ) ) )
70 pnfnre 9624 . . . . . . . . 9  |- +oo  e/  RR
71 neleq1 2798 . . . . . . . . . 10  |-  ( y  = +oo  ->  (
y  e/  RR  <-> +oo  e/  RR ) )
7271adantl 466 . . . . . . . . 9  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  y  = +oo )  ->  ( y  e/  RR  <-> +oo  e/  RR ) )
7370, 72mpbiri 233 . . . . . . . 8  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  y  = +oo )  ->  y  e/  RR )
74 neleq1 2798 . . . . . . . 8  |-  ( y  =  if ( x  =  1 , +oo ,  ( x  / 
( 1  -  x
) ) )  -> 
( y  e/  RR  <->  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  e/  RR ) )
7573, 74syl5ibcom 220 . . . . . . 7  |-  ( ( ( 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 ) )
76 df-nel 2658 . . . . . . . 8  |-  ( if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  e/  RR  <->  -.  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  e.  RR )
77 iffalse 3941 . . . . . . . . . . . . 13  |-  ( -.  x  =  1  ->  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  =  ( x  /  ( 1  -  x ) ) )
7877adantl 466 . . . . . . . . . . . 12  |-  ( ( x  e.  ( 0 [,] 1 )  /\  -.  x  =  1
)  ->  if (
x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  =  ( x  / 
( 1  -  x
) ) )
79 0re 9585 . . . . . . . . . . . . . 14  |-  0  e.  RR
80 icossre 11594 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\ +oo  e.  RR* )  ->  (
0 [,) +oo )  C_  RR )
8179, 3, 80mp2an 672 . . . . . . . . . . . . 13  |-  ( 0 [,) +oo )  C_  RR
8281, 34sseldi 3495 . . . . . . . . . . . 12  |-  ( ( x  e.  ( 0 [,] 1 )  /\  -.  x  =  1
)  ->  ( x  /  ( 1  -  x ) )  e.  RR )
8378, 82eqeltrd 2548 . . . . . . . . . . 11  |-  ( ( x  e.  ( 0 [,] 1 )  /\  -.  x  =  1
)  ->  if (
x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  e.  RR )
8483ex 434 . . . . . . . . . 10  |-  ( x  e.  ( 0 [,] 1 )  ->  ( -.  x  =  1  ->  if ( x  =  1 , +oo , 
( x  /  (
1  -  x ) ) )  e.  RR ) )
8584ad2antrr 725 . . . . . . . . 9  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  y  = +oo )  ->  ( -.  x  =  1  ->  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  e.  RR ) )
8685con1d 124 . . . . . . . 8  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  y  = +oo )  ->  ( -.  if ( x  =  1 , +oo , 
( x  /  (
1  -  x ) ) )  e.  RR  ->  x  =  1 ) )
8776, 86syl5bi 217 . . . . . . 7  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  y  = +oo )  ->  ( if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) )  e/  RR  ->  x  =  1 ) )
8875, 87syld 44 . . . . . 6  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  y  = +oo )  ->  ( y  =  if ( x  =  1 , +oo ,  ( x  / 
( 1  -  x
) ) )  ->  x  =  1 ) )
8969, 88impbid 191 . . . . 5  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  y  = +oo )  ->  ( x  =  1  <->  y  =  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) ) ) )
90 eqeq2 2475 . . . . . . 7  |-  ( +oo  =  if ( x  =  1 , +oo , 
( x  /  (
1  -  x ) ) )  ->  (
y  = +oo  <->  y  =  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) ) ) )
9190bibi2d 318 . . . . . 6  |-  ( +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 ) ) ) ) ) )
92 eqeq2 2475 . . . . . . 7  |-  ( ( x  /  ( 1  -  x ) )  =  if ( x  =  1 , +oo ,  ( x  / 
( 1  -  x
) ) )  -> 
( y  =  ( x  /  ( 1  -  x ) )  <-> 
y  =  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) ) ) )
9392bibi2d 318 . . . . . 6  |-  ( ( 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 ) ) ) ) ) )
94 elico2 11577 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) )
9579, 13, 94mp2an 672 . . . . . . . . . . . . . 14  |-  ( ( y  /  ( 1  +  y ) )  e.  ( 0 [,) 1 )  <->  ( (
y  /  ( 1  +  y ) )  e.  RR  /\  0  <_  ( y  /  (
1  +  y ) )  /\  ( y  /  ( 1  +  y ) )  <  1 ) )
9658, 95sylib 196 . . . . . . . . . . . . 13  |-  ( ( y  e.  ( 0 [,] +oo )  /\  -.  y  = +oo )  ->  ( ( y  /  ( 1  +  y ) )  e.  RR  /\  0  <_ 
( y  /  (
1  +  y ) )  /\  ( y  /  ( 1  +  y ) )  <  1 ) )
9796simp1d 1003 . . . . . . . . . . . 12  |-  ( ( y  e.  ( 0 [,] +oo )  /\  -.  y  = +oo )  ->  ( y  / 
( 1  +  y ) )  e.  RR )
9896simp3d 1005 . . . . . . . . . . . 12  |-  ( ( y  e.  ( 0 [,] +oo )  /\  -.  y  = +oo )  ->  ( y  / 
( 1  +  y ) )  <  1
)
9997, 98gtned 9708 . . . . . . . . . . 11  |-  ( ( y  e.  ( 0 [,] +oo )  /\  -.  y  = +oo )  ->  1  =/=  (
y  /  ( 1  +  y ) ) )
10099adantll 713 . . . . . . . . . 10  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  -.  y  = +oo )  ->  1  =/=  ( y  /  (
1  +  y ) ) )
101100neneqd 2662 . . . . . . . . 9  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  -.  y  = +oo )  ->  -.  1  =  ( y  /  ( 1  +  y ) ) )
102 eqeq1 2464 . . . . . . . . . 10  |-  ( x  =  1  ->  (
x  =  ( y  /  ( 1  +  y ) )  <->  1  =  ( y  /  (
1  +  y ) ) ) )
103102notbid 294 . . . . . . . . 9  |-  ( x  =  1  ->  ( -.  x  =  (
y  /  ( 1  +  y ) )  <->  -.  1  =  (
y  /  ( 1  +  y ) ) ) )
104101, 103syl5ibrcom 222 . . . . . . . 8  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  -.  y  = +oo )  ->  (
x  =  1  ->  -.  x  =  (
y  /  ( 1  +  y ) ) ) )
105104imp 429 . . . . . . 7  |-  ( ( ( ( x  e.  ( 0 [,] 1
)  /\  y  e.  ( 0 [,] +oo ) )  /\  -.  y  = +oo )  /\  x  =  1
)  ->  -.  x  =  ( y  / 
( 1  +  y ) ) )
106 simplr 754 . . . . . . 7  |-  ( ( ( ( x  e.  ( 0 [,] 1
)  /\  y  e.  ( 0 [,] +oo ) )  /\  -.  y  = +oo )  /\  x  =  1
)  ->  -.  y  = +oo )
107105, 1062falsed 351 . . . . . 6  |-  ( ( ( ( x  e.  ( 0 [,] 1
)  /\  y  e.  ( 0 [,] +oo ) )  /\  -.  y  = +oo )  /\  x  =  1
)  ->  ( x  =  ( y  / 
( 1  +  y ) )  <->  y  = +oo ) )
108 f1ocnvfvb 6164 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
10928, 108mp3an1 1306 . . . . . . . . . . 11  |-  ( ( 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 ) )
110 simpl 457 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( 0 [,) 1 )  /\  y  e.  ( 0 [,) +oo ) )  ->  x  e.  ( 0 [,) 1 ) )
111 ovex 6300 . . . . . . . . . . . . 13  |-  ( x  /  ( 1  -  x ) )  e. 
_V
11226fvmpt2 5948 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( 0 [,) 1 )  /\  ( x  /  (
1  -  x ) )  e.  _V )  ->  ( ( x  e.  ( 0 [,) 1
)  |->  ( x  / 
( 1  -  x
) ) ) `  x )  =  ( x  /  ( 1  -  x ) ) )
113110, 111, 112sylancl 662 . . . . . . . . . . . 12  |-  ( ( x  e.  ( 0 [,) 1 )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( ( x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) ) `
 x )  =  ( x  /  (
1  -  x ) ) )
114113eqeq1d 2462 . . . . . . . . . . 11  |-  ( ( x  e.  ( 0 [,) 1 )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( ( ( x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) ) `  x )  =  y  <->  ( x  /  ( 1  -  x ) )  =  y ) )
115 simpr 461 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( 0 [,) 1 )  /\  y  e.  ( 0 [,) +oo ) )  ->  y  e.  ( 0 [,) +oo )
)
116 ovex 6300 . . . . . . . . . . . . 13  |-  ( y  /  ( 1  +  y ) )  e. 
_V
11754fvmpt2 5948 . . . . . . . . . . . . 13  |-  ( ( y  e.  ( 0 [,) +oo )  /\  ( y  /  (
1  +  y ) )  e.  _V )  ->  ( `' ( x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) ) `
 y )  =  ( y  /  (
1  +  y ) ) )
118115, 116, 117sylancl 662 . . . . . . . . . . . 12  |-  ( ( x  e.  ( 0 [,) 1 )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( `' ( x  e.  ( 0 [,) 1 )  |->  ( x  /  ( 1  -  x ) ) ) `  y )  =  ( y  / 
( 1  +  y ) ) )
119118eqeq1d 2462 . . . . . . . . . . 11  |-  ( ( x  e.  ( 0 [,) 1 )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( ( `' ( x  e.  ( 0 [,) 1 ) 
|->  ( x  /  (
1  -  x ) ) ) `  y
)  =  x  <->  ( y  /  ( 1  +  y ) )  =  x ) )
120109, 114, 1193bitr3rd 284 . . . . . . . . . 10  |-  ( ( x  e.  ( 0 [,) 1 )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( ( y  /  ( 1  +  y ) )  =  x  <->  ( x  / 
( 1  -  x
) )  =  y ) )
121 eqcom 2469 . . . . . . . . . 10  |-  ( x  =  ( y  / 
( 1  +  y ) )  <->  ( y  /  ( 1  +  y ) )  =  x )
122 eqcom 2469 . . . . . . . . . 10  |-  ( y  =  ( x  / 
( 1  -  x
) )  <->  ( x  /  ( 1  -  x ) )  =  y )
123120, 121, 1223bitr4g 288 . . . . . . . . 9  |-  ( ( x  e.  ( 0 [,) 1 )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  =  ( y  /  (
1  +  y ) )  <->  y  =  ( x  /  ( 1  -  x ) ) ) )
12425, 50, 123syl2an 477 . . . . . . . 8  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  -.  x  =  1 )  /\  (
y  e.  ( 0 [,] +oo )  /\  -.  y  = +oo ) )  ->  (
x  =  ( y  /  ( 1  +  y ) )  <->  y  =  ( x  /  (
1  -  x ) ) ) )
125124an4s 823 . . . . . . 7  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  ( -.  x  =  1  /\  -.  y  = +oo ) )  ->  (
x  =  ( y  /  ( 1  +  y ) )  <->  y  =  ( x  /  (
1  -  x ) ) ) )
126125anass1rs 805 . . . . . 6  |-  ( ( ( ( x  e.  ( 0 [,] 1
)  /\  y  e.  ( 0 [,] +oo ) )  /\  -.  y  = +oo )  /\  -.  x  =  1 )  ->  ( x  =  ( y  / 
( 1  +  y ) )  <->  y  =  ( x  /  (
1  -  x ) ) ) )
12791, 93, 107, 126ifbothda 3967 . . . . 5  |-  ( ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo )
)  /\  -.  y  = +oo )  ->  (
x  =  ( y  /  ( 1  +  y ) )  <->  y  =  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) ) ) )
12863, 65, 89, 127ifbothda 3967 . . . 4  |-  ( ( x  e.  ( 0 [,] 1 )  /\  y  e.  ( 0 [,] +oo ) )  ->  ( x  =  if ( y  = +oo ,  1 ,  ( y  /  (
1  +  y ) ) )  <->  y  =  if ( x  =  1 , +oo ,  ( x  /  ( 1  -  x ) ) ) ) )
129128adantl 466 . . 3  |-  ( ( 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 ) ) ) ) )
1301, 37, 61, 129f1ocnv2d 6501 . 2  |-  ( T. 
->  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo )  /\  `' F  =  (
y  e.  ( 0 [,] +oo )  |->  if ( y  = +oo ,  1 ,  ( y  /  ( 1  +  y ) ) ) ) ) )
131130trud 1383 1  |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo )  /\  `' F  =  ( y  e.  ( 0 [,] +oo )  |->  if ( y  = +oo ,  1 ,  ( y  /  (
1  +  y ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 968    = wceq 1374   T. wtru 1375    e. wcel 1762    =/= wne 2655    e/ wnel 2656   A.wral 2807   _Vcvv 3106    u. cun 3467    C_ wss 3469   ifcif 3932   {csn 4020   class class class wbr 4440    |-> cmpt 4498   `'ccnv 4991   -->wf 5575   -1-1-onto->wf1o 5578   ` cfv 5579  (class class class)co 6275   RRcr 9480   0cc0 9481   1c1 9482    + caddc 9484   +oocpnf 9614   RR*cxr 9616    < clt 9617    <_ cle 9618    - cmin 9794    / cdiv 10195   [,)cico 11520   [,]cicc 11521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-po 4793  df-so 4794  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-er 7301  df-en 7507  df-dom 7508  df-sdom 7509  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9796  df-neg 9797  df-div 10196  df-rp 11210  df-ico 11524  df-icc 11525
This theorem is referenced by:  iccpnfhmeo  21173  xrhmeo  21174
  Copyright terms: Public domain W3C validator