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

Theorem elioopnf 11725
Description: Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
Assertion
Ref Expression
elioopnf  |-  ( A  e.  RR*  ->  ( B  e.  ( A (,) +oo )  <->  ( B  e.  RR  /\  A  < 
B ) ) )

Proof of Theorem elioopnf
StepHypRef Expression
1 pnfxr 11409 . . 3  |- +oo  e.  RR*
2 elioo2 11674 . . 3  |-  ( ( A  e.  RR*  /\ +oo  e.  RR* )  ->  ( B  e.  ( A (,) +oo )  <->  ( B  e.  RR  /\  A  < 
B  /\  B  < +oo ) ) )
31, 2mpan2 676 . 2  |-  ( A  e.  RR*  ->  ( B  e.  ( A (,) +oo )  <->  ( B  e.  RR  /\  A  < 
B  /\  B  < +oo ) ) )
4 df-3an 986 . . 3  |-  ( ( B  e.  RR  /\  A  <  B  /\  B  < +oo )  <->  ( ( B  e.  RR  /\  A  <  B )  /\  B  < +oo ) )
5 ltpnf 11419 . . . . 5  |-  ( B  e.  RR  ->  B  < +oo )
65adantr 467 . . . 4  |-  ( ( B  e.  RR  /\  A  <  B )  ->  B  < +oo )
76pm4.71i 637 . . 3  |-  ( ( B  e.  RR  /\  A  <  B )  <->  ( ( B  e.  RR  /\  A  <  B )  /\  B  < +oo ) )
84, 7bitr4i 256 . 2  |-  ( ( B  e.  RR  /\  A  <  B  /\  B  < +oo )  <->  ( B  e.  RR  /\  A  < 
B ) )
93, 8syl6bb 265 1  |-  ( A  e.  RR*  ->  ( B  e.  ( A (,) +oo )  <->  ( B  e.  RR  /\  A  < 
B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 984    e. wcel 1886   class class class wbr 4401  (class class class)co 6288   RRcr 9535   +oocpnf 9669   RR*cxr 9671    < clt 9672   (,)cioo 11632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-pre-lttri 9610  ax-pre-lttrn 9611
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-po 4754  df-so 4755  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-1st 6790  df-2nd 6791  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-ioo 11636
This theorem is referenced by:  mbfmulc2lem  22596  mbfposr  22601  ismbf3d  22603  mbfaddlem  22609  mbfsup  22613  itg2gt0  22711  itg2cnlem1  22712  itg2cnlem2  22713  lhop2  22960  dvfsumlem2  22972  dvfsumlem3  22973  dvfsumrlimge0  22975  dvfsumrlim  22976  dvfsumrlim2  22977  pntpbnd1a  24416  pntpbnd2  24418  pntibndlem2  24422  pntibndlem3  24423  pntlemi  24435  pntlemo  24438  relowlssretop  31759  itg2addnclem2  31987  iblabsnclem  31998  ftc1anclem1  32010  ftc1anclem6  32015  rfcnpre1  37334  regt1loggt0  40334  rege1logbrege0  40356  rege1logbzge0  40357
  Copyright terms: Public domain W3C validator