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

Theorem supex 7470
Description: A supremum is a set. (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
supex.1  |-  R  Or  A
Assertion
Ref Expression
supex  |-  sup ( B ,  A ,  R )  e.  _V

Proof of Theorem supex
StepHypRef Expression
1 supex.1 . 2  |-  R  Or  A
2 id 21 . . 3  |-  ( R  Or  A  ->  R  Or  A )
32supexd 7460 . 2  |-  ( R  Or  A  ->  sup ( B ,  A ,  R )  e.  _V )
41, 3ax-mp 8 1  |-  sup ( B ,  A ,  R )  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   _Vcvv 2958    Or wor 4504   supcsup 7447
This theorem is referenced by:  infmxrgelb  10915  limsupval  12270  limsupgval  12272  limsupgre  12277  gcdval  13010  odzval  13179  pczpre  13223  prmreclem1  13286  ramval  13378  ramcl2lem  13379  prdsdsfn  13689  prdsdsval  13702  imasdsfn  13742  imasdsval  13743  odval  15174  odf  15177  gexval  15214  nmoval  18751  xrge0tsms2  18868  metdsval  18879  ovolval  19372  ovolf  19380  mbfsup  19558  mbfinf  19559  itg2val  19622  itg2monolem1  19644  itg2mono  19647  mdegval  19988  mdegxrf  19993  plyeq0lem  20131  dgrval  20149  elqaalem1  20238  elqaalem3  20240  nmooval  22266  nmopval  23361  nmfnval  23381  lmdvg  24340  esumval  24443  ballotlemi  24760  erdszelem3  24881  erdszelem6  24884  gtinf  26324  pellfundval  26945  dgraaval  27328  dgraaf  27331
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405  ax-un 4703
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rmo 2715  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-po 4505  df-so 4506  df-sup 7448
  Copyright terms: Public domain W3C validator