Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  iooelexlt Structured version   Unicode version

Theorem iooelexlt 31730
Description: An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020.)
Assertion
Ref Expression
iooelexlt  |-  ( X  e.  ( A (,) B )  ->  E. y  e.  ( A (,) B
) y  <  X
)
Distinct variable groups:    y, A    y, B    y, X

Proof of Theorem iooelexlt
StepHypRef Expression
1 eliooxr 11701 . . 3  |-  ( X  e.  ( A (,) B )  ->  ( A  e.  RR*  /\  B  e.  RR* ) )
21simpld 460 . 2  |-  ( X  e.  ( A (,) B )  ->  A  e.  RR* )
3 elxr 11424 . . 3  |-  ( A  e.  RR*  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
4 19.3v 1806 . . . . . 6  |-  ( A. y ( X  e.  ( A (,) B
)  /\  A  e.  RR )  <->  ( X  e.  ( A (,) B
)  /\  A  e.  RR ) )
5 ovex 6334 . . . . . . 7  |-  ( ( A  +  X )  /  2 )  e. 
_V
6 nfcv 2580 . . . . . . . 8  |-  F/_ y
( ( A  +  X )  /  2
)
7 nfre1 2883 . . . . . . . 8  |-  F/ y E. y  e.  ( A (,) B ) y  <  X
8 elioore 11674 . . . . . . . . . . . . . . 15  |-  ( X  e.  ( A (,) B )  ->  X  e.  RR )
9 readdcl 9630 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR  /\  X  e.  RR )  ->  ( A  +  X
)  e.  RR )
109rehalfcld 10867 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  X  e.  RR )  ->  ( ( A  +  X )  /  2
)  e.  RR )
118, 10sylan2 476 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR  /\  X  e.  ( A (,) B ) )  -> 
( ( A  +  X )  /  2
)  e.  RR )
1211ancoms 454 . . . . . . . . . . . . 13  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( ( A  +  X )  /  2
)  e.  RR )
1312rexrd 9698 . . . . . . . . . . . 12  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( ( A  +  X )  /  2
)  e.  RR* )
14 eliooord 11702 . . . . . . . . . . . . . . 15  |-  ( X  e.  ( A (,) B )  ->  ( A  <  X  /\  X  <  B ) )
1514simpld 460 . . . . . . . . . . . . . 14  |-  ( X  e.  ( A (,) B )  ->  A  <  X )
1615adantr 466 . . . . . . . . . . . . 13  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  A  <  X )
17 avglt1 10858 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  X  e.  RR )  ->  ( A  <  X  <->  A  <  ( ( A  +  X )  / 
2 ) ) )
188, 17sylan2 476 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR  /\  X  e.  ( A (,) B ) )  -> 
( A  <  X  <->  A  <  ( ( A  +  X )  / 
2 ) ) )
1918ancoms 454 . . . . . . . . . . . . 13  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( A  <  X  <->  A  <  ( ( A  +  X )  / 
2 ) ) )
2016, 19mpbid 213 . . . . . . . . . . . 12  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  A  <  ( ( A  +  X )  /  2 ) )
218rexrd 9698 . . . . . . . . . . . . . 14  |-  ( X  e.  ( A (,) B )  ->  X  e.  RR* )
2221adantr 466 . . . . . . . . . . . . 13  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  X  e.  RR* )
231simprd 464 . . . . . . . . . . . . . 14  |-  ( X  e.  ( A (,) B )  ->  B  e.  RR* )
2423adantr 466 . . . . . . . . . . . . 13  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  B  e.  RR* )
25 avglt2 10859 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR  /\  X  e.  RR )  ->  ( A  <  X  <->  ( ( A  +  X
)  /  2 )  <  X ) )
268, 25sylan2 476 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  X  e.  ( A (,) B ) )  -> 
( A  <  X  <->  ( ( A  +  X
)  /  2 )  <  X ) )
2726ancoms 454 . . . . . . . . . . . . . 14  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( A  <  X  <->  ( ( A  +  X
)  /  2 )  <  X ) )
2816, 27mpbid 213 . . . . . . . . . . . . 13  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( ( A  +  X )  /  2
)  <  X )
2914simprd 464 . . . . . . . . . . . . . 14  |-  ( X  e.  ( A (,) B )  ->  X  <  B )
3029adantr 466 . . . . . . . . . . . . 13  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  X  <  B )
3113, 22, 24, 28, 30xrlttrd 11464 . . . . . . . . . . . 12  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( ( A  +  X )  /  2
)  <  B )
32 elioo1 11684 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( ( A  +  X )  /  2
)  e.  ( A (,) B )  <->  ( (
( A  +  X
)  /  2 )  e.  RR*  /\  A  < 
( ( A  +  X )  /  2
)  /\  ( ( A  +  X )  /  2 )  < 
B ) ) )
331, 32syl 17 . . . . . . . . . . . . 13  |-  ( X  e.  ( A (,) B )  ->  (
( ( A  +  X )  /  2
)  e.  ( A (,) B )  <->  ( (
( A  +  X
)  /  2 )  e.  RR*  /\  A  < 
( ( A  +  X )  /  2
)  /\  ( ( A  +  X )  /  2 )  < 
B ) ) )
3433adantr 466 . . . . . . . . . . . 12  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( ( ( A  +  X )  / 
2 )  e.  ( A (,) B )  <-> 
( ( ( A  +  X )  / 
2 )  e.  RR*  /\  A  <  ( ( A  +  X )  /  2 )  /\  ( ( A  +  X )  /  2
)  <  B )
) )
3513, 20, 31, 34mpbir3and 1188 . . . . . . . . . . 11  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( ( A  +  X )  /  2
)  e.  ( A (,) B ) )
3635, 28jca 534 . . . . . . . . . 10  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( ( ( A  +  X )  / 
2 )  e.  ( A (,) B )  /\  ( ( A  +  X )  / 
2 )  <  X
) )
37 eleq1 2495 . . . . . . . . . . 11  |-  ( y  =  ( ( A  +  X )  / 
2 )  ->  (
y  e.  ( A (,) B )  <->  ( ( A  +  X )  /  2 )  e.  ( A (,) B
) ) )
38 breq1 4426 . . . . . . . . . . 11  |-  ( y  =  ( ( A  +  X )  / 
2 )  ->  (
y  <  X  <->  ( ( A  +  X )  /  2 )  < 
X ) )
3937, 38anbi12d 715 . . . . . . . . . 10  |-  ( y  =  ( ( A  +  X )  / 
2 )  ->  (
( y  e.  ( A (,) B )  /\  y  <  X
)  <->  ( ( ( A  +  X )  /  2 )  e.  ( A (,) B
)  /\  ( ( A  +  X )  /  2 )  < 
X ) ) )
4036, 39syl5ibr 224 . . . . . . . . 9  |-  ( y  =  ( ( A  +  X )  / 
2 )  ->  (
( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  ( y  e.  ( A (,) B
)  /\  y  <  X ) ) )
41 rspe 2880 . . . . . . . . 9  |-  ( ( y  e.  ( A (,) B )  /\  y  <  X )  ->  E. y  e.  ( A (,) B ) y  <  X )
4240, 41syl6 34 . . . . . . . 8  |-  ( y  =  ( ( A  +  X )  / 
2 )  ->  (
( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  E. y  e.  ( A (,) B ) y  <  X ) )
436, 7, 42spcimgf 3159 . . . . . . 7  |-  ( ( ( A  +  X
)  /  2 )  e.  _V  ->  ( A. y ( X  e.  ( A (,) B
)  /\  A  e.  RR )  ->  E. y  e.  ( A (,) B
) y  <  X
) )
445, 43ax-mp 5 . . . . . 6  |-  ( A. y ( X  e.  ( A (,) B
)  /\  A  e.  RR )  ->  E. y  e.  ( A (,) B
) y  <  X
)
454, 44sylbir 216 . . . . 5  |-  ( ( X  e.  ( A (,) B )  /\  A  e.  RR )  ->  E. y  e.  ( A (,) B ) y  <  X )
4645expcom 436 . . . 4  |-  ( A  e.  RR  ->  ( X  e.  ( A (,) B )  ->  E. y  e.  ( A (,) B
) y  <  X
) )
47 simpl 458 . . . . . 6  |-  ( ( X  e.  ( A (,) B )  /\  A  = +oo )  ->  X  e.  ( A (,) B ) )
48 oveq1 6313 . . . . . . . . 9  |-  ( A  = +oo  ->  ( A (,) B )  =  ( +oo (,) B
) )
4948eleq2d 2492 . . . . . . . 8  |-  ( A  = +oo  ->  ( X  e.  ( A (,) B )  <->  X  e.  ( +oo (,) B ) ) )
5049adantl 467 . . . . . . 7  |-  ( ( X  e.  ( A (,) B )  /\  A  = +oo )  ->  ( X  e.  ( A (,) B )  <-> 
X  e.  ( +oo (,) B ) ) )
51 pnfxr 11420 . . . . . . . . . . . . 13  |- +oo  e.  RR*
52 elioo2 11685 . . . . . . . . . . . . 13  |-  ( ( +oo  e.  RR*  /\  B  e.  RR* )  ->  ( X  e.  ( +oo (,) B )  <->  ( X  e.  RR  /\ +oo  <  X  /\  X  <  B
) ) )
5351, 52mpan 674 . . . . . . . . . . . 12  |-  ( B  e.  RR*  ->  ( X  e.  ( +oo (,) B )  <->  ( X  e.  RR  /\ +oo  <  X  /\  X  <  B
) ) )
5453biimpd 210 . . . . . . . . . . 11  |-  ( B  e.  RR*  ->  ( X  e.  ( +oo (,) B )  ->  ( X  e.  RR  /\ +oo  <  X  /\  X  < 
B ) ) )
55 elioore 11674 . . . . . . . . . . . . 13  |-  ( X  e.  ( +oo (,) B )  ->  X  e.  RR )
56 rexr 9694 . . . . . . . . . . . . . . 15  |-  ( X  e.  RR  ->  X  e.  RR* )
57 pnfnlt 11438 . . . . . . . . . . . . . . 15  |-  ( X  e.  RR*  ->  -. +oo  <  X )
5856, 57syl 17 . . . . . . . . . . . . . 14  |-  ( X  e.  RR  ->  -. +oo 
<  X )
5958intn3an2d 1375 . . . . . . . . . . . . 13  |-  ( X  e.  RR  ->  -.  ( X  e.  RR  /\ +oo  <  X  /\  X  <  B ) )
6055, 59syl 17 . . . . . . . . . . . 12  |-  ( X  e.  ( +oo (,) B )  ->  -.  ( X  e.  RR  /\ +oo  <  X  /\  X  <  B ) )
6160a1i 11 . . . . . . . . . . 11  |-  ( B  e.  RR*  ->  ( X  e.  ( +oo (,) B )  ->  -.  ( X  e.  RR  /\ +oo  <  X  /\  X  <  B ) ) )
6254, 61pm2.65d 178 . . . . . . . . . 10  |-  ( B  e.  RR*  ->  -.  X  e.  ( +oo (,) B
) )
6323, 62syl 17 . . . . . . . . 9  |-  ( X  e.  ( A (,) B )  ->  -.  X  e.  ( +oo (,) B ) )
6463pm2.21d 109 . . . . . . . 8  |-  ( X  e.  ( A (,) B )  ->  ( X  e.  ( +oo (,) B )  ->  E. y  e.  ( A (,) B
) y  <  X
) )
6564adantr 466 . . . . . . 7  |-  ( ( X  e.  ( A (,) B )  /\  A  = +oo )  ->  ( X  e.  ( +oo (,) B )  ->  E. y  e.  ( A (,) B ) y  <  X ) )
6650, 65sylbid 218 . . . . . 6  |-  ( ( X  e.  ( A (,) B )  /\  A  = +oo )  ->  ( X  e.  ( A (,) B )  ->  E. y  e.  ( A (,) B ) y  <  X ) )
6747, 66mpd 15 . . . . 5  |-  ( ( X  e.  ( A (,) B )  /\  A  = +oo )  ->  E. y  e.  ( A (,) B ) y  <  X )
6867expcom 436 . . . 4  |-  ( A  = +oo  ->  ( X  e.  ( A (,) B )  ->  E. y  e.  ( A (,) B
) y  <  X
) )
69 19.3v 1806 . . . . . 6  |-  ( A. y ( X  e.  ( A (,) B
)  /\  A  = -oo )  <->  ( X  e.  ( A (,) B
)  /\  A  = -oo ) )
70 ovex 6334 . . . . . . 7  |-  ( X  -  1 )  e. 
_V
71 nfcv 2580 . . . . . . . 8  |-  F/_ y
( X  -  1 )
72 peano2rem 9949 . . . . . . . . . . . . . . . . 17  |-  ( X  e.  RR  ->  ( X  -  1 )  e.  RR )
738, 72syl 17 . . . . . . . . . . . . . . . 16  |-  ( X  e.  ( A (,) B )  ->  ( X  -  1 )  e.  RR )
74 mnflt 11433 . . . . . . . . . . . . . . . . 17  |-  ( ( X  -  1 )  e.  RR  -> -oo  <  ( X  -  1 ) )
7573, 74syl 17 . . . . . . . . . . . . . . . 16  |-  ( X  e.  ( A (,) B )  -> -oo  <  ( X  -  1 ) )
7673rexrd 9698 . . . . . . . . . . . . . . . . 17  |-  ( X  e.  ( A (,) B )  ->  ( X  -  1 )  e.  RR* )
778ltm1d 10547 . . . . . . . . . . . . . . . . 17  |-  ( X  e.  ( A (,) B )  ->  ( X  -  1 )  <  X )
7876, 21, 23, 77, 29xrlttrd 11464 . . . . . . . . . . . . . . . 16  |-  ( X  e.  ( A (,) B )  ->  ( X  -  1 )  <  B )
79 mnfxr 11422 . . . . . . . . . . . . . . . . . 18  |- -oo  e.  RR*
80 elioo2 11685 . . . . . . . . . . . . . . . . . 18  |-  ( ( -oo  e.  RR*  /\  B  e.  RR* )  ->  (
( X  -  1 )  e.  ( -oo (,) B )  <->  ( ( X  -  1 )  e.  RR  /\ -oo  <  ( X  -  1 )  /\  ( X  -  1 )  < 
B ) ) )
8179, 80mpan 674 . . . . . . . . . . . . . . . . 17  |-  ( B  e.  RR*  ->  ( ( X  -  1 )  e.  ( -oo (,) B )  <->  ( ( X  -  1 )  e.  RR  /\ -oo  <  ( X  -  1 )  /\  ( X  -  1 )  < 
B ) ) )
8223, 81syl 17 . . . . . . . . . . . . . . . 16  |-  ( X  e.  ( A (,) B )  ->  (
( X  -  1 )  e.  ( -oo (,) B )  <->  ( ( X  -  1 )  e.  RR  /\ -oo  <  ( X  -  1 )  /\  ( X  -  1 )  < 
B ) ) )
8373, 75, 78, 82mpbir3and 1188 . . . . . . . . . . . . . . 15  |-  ( X  e.  ( A (,) B )  ->  ( X  -  1 )  e.  ( -oo (,) B ) )
8483adantr 466 . . . . . . . . . . . . . 14  |-  ( ( X  e.  ( A (,) B )  /\  A  = -oo )  ->  ( X  -  1 )  e.  ( -oo (,) B ) )
85 oveq1 6313 . . . . . . . . . . . . . . . 16  |-  ( A  = -oo  ->  ( A (,) B )  =  ( -oo (,) B
) )
8685eleq2d 2492 . . . . . . . . . . . . . . 15  |-  ( A  = -oo  ->  (
( X  -  1 )  e.  ( A (,) B )  <->  ( X  -  1 )  e.  ( -oo (,) B
) ) )
8786adantl 467 . . . . . . . . . . . . . 14  |-  ( ( X  e.  ( A (,) B )  /\  A  = -oo )  ->  ( ( X  - 
1 )  e.  ( A (,) B )  <-> 
( X  -  1 )  e.  ( -oo (,) B ) ) )
8884, 87mpbird 235 . . . . . . . . . . . . 13  |-  ( ( X  e.  ( A (,) B )  /\  A  = -oo )  ->  ( X  -  1 )  e.  ( A (,) B ) )
8977adantr 466 . . . . . . . . . . . . 13  |-  ( ( X  e.  ( A (,) B )  /\  A  = -oo )  ->  ( X  -  1 )  <  X )
9088, 89jca 534 . . . . . . . . . . . 12  |-  ( ( X  e.  ( A (,) B )  /\  A  = -oo )  ->  ( ( X  - 
1 )  e.  ( A (,) B )  /\  ( X  - 
1 )  <  X
) )
9190adantr 466 . . . . . . . . . . 11  |-  ( ( ( X  e.  ( A (,) B )  /\  A  = -oo )  /\  y  =  ( X  -  1 ) )  ->  ( ( X  -  1 )  e.  ( A (,) B )  /\  ( X  -  1 )  <  X ) )
92 eleq1 2495 . . . . . . . . . . . . 13  |-  ( y  =  ( X  - 
1 )  ->  (
y  e.  ( A (,) B )  <->  ( X  -  1 )  e.  ( A (,) B
) ) )
93 breq1 4426 . . . . . . . . . . . . 13  |-  ( y  =  ( X  - 
1 )  ->  (
y  <  X  <->  ( X  -  1 )  < 
X ) )
9492, 93anbi12d 715 . . . . . . . . . . . 12  |-  ( y  =  ( X  - 
1 )  ->  (
( y  e.  ( A (,) B )  /\  y  <  X
)  <->  ( ( X  -  1 )  e.  ( A (,) B
)  /\  ( X  -  1 )  < 
X ) ) )
9594adantl 467 . . . . . . . . . . 11  |-  ( ( ( X  e.  ( A (,) B )  /\  A  = -oo )  /\  y  =  ( X  -  1 ) )  ->  ( (
y  e.  ( A (,) B )  /\  y  <  X )  <->  ( ( X  -  1 )  e.  ( A (,) B )  /\  ( X  -  1 )  <  X ) ) )
9691, 95mpbird 235 . . . . . . . . . 10  |-  ( ( ( X  e.  ( A (,) B )  /\  A  = -oo )  /\  y  =  ( X  -  1 ) )  ->  ( y  e.  ( A (,) B
)  /\  y  <  X ) )
9796, 41syl 17 . . . . . . . . 9  |-  ( ( ( X  e.  ( A (,) B )  /\  A  = -oo )  /\  y  =  ( X  -  1 ) )  ->  E. y  e.  ( A (,) B
) y  <  X
)
9897expcom 436 . . . . . . . 8  |-  ( y  =  ( X  - 
1 )  ->  (
( X  e.  ( A (,) B )  /\  A  = -oo )  ->  E. y  e.  ( A (,) B ) y  <  X ) )
9971, 7, 98spcimgf 3159 . . . . . . 7  |-  ( ( X  -  1 )  e.  _V  ->  ( A. y ( X  e.  ( A (,) B
)  /\  A  = -oo )  ->  E. y  e.  ( A (,) B
) y  <  X
) )
10070, 99ax-mp 5 . . . . . 6  |-  ( A. y ( X  e.  ( A (,) B
)  /\  A  = -oo )  ->  E. y  e.  ( A (,) B
) y  <  X
)
10169, 100sylbir 216 . . . . 5  |-  ( ( X  e.  ( A (,) B )  /\  A  = -oo )  ->  E. y  e.  ( A (,) B ) y  <  X )
102101expcom 436 . . . 4  |-  ( A  = -oo  ->  ( X  e.  ( A (,) B )  ->  E. y  e.  ( A (,) B
) y  <  X
) )
10346, 68, 1023jaoi 1327 . . 3  |-  ( ( A  e.  RR  \/  A  = +oo  \/  A  = -oo )  ->  ( X  e.  ( A (,) B )  ->  E. y  e.  ( A (,) B
) y  <  X
) )
1043, 103sylbi 198 . 2  |-  ( A  e.  RR*  ->  ( X  e.  ( A (,) B )  ->  E. y  e.  ( A (,) B
) y  <  X
) )
1052, 104mpcom 37 1  |-  ( X  e.  ( A (,) B )  ->  E. y  e.  ( A (,) B
) y  <  X
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    \/ w3o 981    /\ w3a 982   A.wal 1435    = wceq 1437    e. wcel 1872   E.wrex 2772   _Vcvv 3080   class class class wbr 4423  (class class class)co 6306   RRcr 9546   1c1 9548    + caddc 9550   +oocpnf 9680   -oocmnf 9681   RR*cxr 9682    < clt 9683    - cmin 9868    / cdiv 10277   2c2 10667   (,)cioo 11643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-1st 6808  df-2nd 6809  df-er 7375  df-en 7582  df-dom 7583  df-sdom 7584  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-div 10278  df-2 10676  df-ioo 11647
This theorem is referenced by:  relowlpssretop  31732
  Copyright terms: Public domain W3C validator