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

Theorem elicopnf 10892
Description: Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.)
Assertion
Ref Expression
elicopnf  |-  ( A  e.  RR  ->  ( B  e.  ( A [,)  +oo )  <->  ( B  e.  RR  /\  A  <_  B ) ) )

Proof of Theorem elicopnf
StepHypRef Expression
1 pnfxr 10606 . . 3  |-  +oo  e.  RR*
2 elico2 10867 . . 3  |-  ( ( A  e.  RR  /\  +oo 
e.  RR* )  ->  ( B  e.  ( A [,)  +oo )  <->  ( B  e.  RR  /\  A  <_  B  /\  B  <  +oo ) ) )
31, 2mpan2 652 . 2  |-  ( A  e.  RR  ->  ( B  e.  ( A [,)  +oo )  <->  ( B  e.  RR  /\  A  <_  B  /\  B  <  +oo ) ) )
4 ltpnf 10614 . . . . 5  |-  ( B  e.  RR  ->  B  <  +oo )
54adantr 451 . . . 4  |-  ( ( B  e.  RR  /\  A  <_  B )  ->  B  <  +oo )
65pm4.71i 613 . . 3  |-  ( ( B  e.  RR  /\  A  <_  B )  <->  ( ( B  e.  RR  /\  A  <_  B )  /\  B  <  +oo ) )
7 df-3an 937 . . 3  |-  ( ( B  e.  RR  /\  A  <_  B  /\  B  <  +oo )  <->  ( ( B  e.  RR  /\  A  <_  B )  /\  B  <  +oo ) )
86, 7bitr4i 243 . 2  |-  ( ( B  e.  RR  /\  A  <_  B )  <->  ( B  e.  RR  /\  A  <_  B  /\  B  <  +oo ) )
93, 8syl6bbr 254 1  |-  ( A  e.  RR  ->  ( B  e.  ( A [,)  +oo )  <->  ( B  e.  RR  /\  A  <_  B ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 935    e. wcel 1715   class class class wbr 4125  (class class class)co 5981   RRcr 8883    +oocpnf 9011   RR*cxr 9013    < clt 9014    <_ cle 9015   [,)cico 10811
This theorem is referenced by:  elrege0  10899  rexico  12044  limsupgle  12158  limsupgre  12162  rlim3  12179  ello12  12197  lo1bdd2  12205  elo12  12208  lo1resb  12245  rlimresb  12246  o1resb  12247  lo1eq  12249  rlimeq  12250  rlimsqzlem  12329  o1fsum  12479  ovolicopnf  19098  dvfsumrlimge0  19592  dvfsumrlim  19593  dvfsumrlim2  19594  cxp2lim  20493  chebbnd1  20844  chtppilimlem1  20845  chtppilimlem2  20846  chtppilim  20847  chebbnd2  20849  chto1lb  20850  chpchtlim  20851  chpo1ub  20852  vmadivsumb  20855  dchrisumlema  20860  dchrisumlem2  20862  dchrisumlem3  20863  dchrmusumlema  20865  dchrmusum2  20866  dchrvmasumlem2  20870  dchrvmasumiflem1  20873  dchrisum0lema  20886  dchrisum0lem1b  20887  dchrisum0lem2a  20889  dchrisum0lem2  20890  2vmadivsumlem  20912  selbergb  20921  selberg2b  20924  chpdifbndlem1  20925  selberg3lem1  20929  selberg3lem2  20930  selberg4lem1  20932  pntrsumo1  20937  selbergsb  20947  pntrlog2bndlem3  20951  pntpbnd1  20958  pntpbnd2  20959  pntibndlem3  20964  pntlemn  20972  pntlem3  20981  pntleml  20983  pnt2  20985  rge0scvg  23811  itg2addnclem2  25761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615  ax-cnex 8940  ax-resscn 8941  ax-pre-lttri 8958  ax-pre-lttrn 8959
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-nel 2532  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-po 4417  df-so 4418  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-er 6802  df-en 7007  df-dom 7008  df-sdom 7009  df-pnf 9016  df-mnf 9017  df-xr 9018  df-ltxr 9019  df-le 9020  df-ico 10815
  Copyright terms: Public domain W3C validator