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

Theorem ioorp 13339
Description: The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
Assertion
Ref Expression
ioorp (0(,)+∞) = ℝ+

Proof of Theorem ioorp
StepHypRef Expression
1 ioopos 13338 . 2 (0(,)+∞) = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2 df-rp 12913 . 2 + = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
31, 2eqtr4i 2767 1 (0(,)+∞) = ℝ+
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  {crab 3406   class class class wbr 5104  (class class class)co 7354  cr 11047  0cc0 11048  +∞cpnf 11183   < clt 11186  +crp 12912  (,)cioo 13261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7669  ax-cnex 11104  ax-resscn 11105  ax-1cn 11106  ax-addrcl 11109  ax-rnegex 11119  ax-cnre 11121  ax-pre-lttri 11122  ax-pre-lttrn 11123
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5530  df-po 5544  df-so 5545  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7357  df-oprab 7358  df-mpo 7359  df-1st 7918  df-2nd 7919  df-er 8645  df-en 8881  df-dom 8882  df-sdom 8883  df-pnf 11188  df-mnf 11189  df-xr 11190  df-ltxr 11191  df-le 11192  df-rp 12913  df-ioo 13265
This theorem is referenced by:  rpsup  13768  advlog  26005  advlogexp  26006  logccv  26014  cxpcn3  26097  loglesqrt  26107  rlimcnp  26311  rlimcnp2  26312  divsqrtsumlem  26325  amgmlem  26335  logfacbnd3  26567  logexprlim  26569  dchrisum0lem2a  26861  logdivsum  26877  log2sumbnd  26888  elxrge02  31683  xrge0iifcnv  32405  xrge0iifiso  32407  xrge0iifhom  32409  xrge0mulc1cn  32413  esumdivc  32573  signsply0  33054  rpsqrtcn  33097  logdivsqrle  33154  itg2gt0cn  36122  dvasin  36151  hoicvrrex  44767  amgmwlem  47219
  Copyright terms: Public domain W3C validator