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

Theorem supsn 9510
Description: The supremum of a singleton. (Contributed by NM, 2-Oct-2007.)
Assertion
Ref Expression
supsn ((𝑅 Or 𝐴𝐵𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵)

Proof of Theorem supsn
StepHypRef Expression
1 dfsn2 4644 . . . 4 {𝐵} = {𝐵, 𝐵}
21supeq1i 9485 . . 3 sup({𝐵}, 𝐴, 𝑅) = sup({𝐵, 𝐵}, 𝐴, 𝑅)
3 suppr 9509 . . . 4 ((𝑅 Or 𝐴𝐵𝐴𝐵𝐴) → sup({𝐵, 𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
433anidm23 1420 . . 3 ((𝑅 Or 𝐴𝐵𝐴) → sup({𝐵, 𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
52, 4eqtrid 2787 . 2 ((𝑅 Or 𝐴𝐵𝐴) → sup({𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
6 ifid 4571 . 2 if(𝐵𝑅𝐵, 𝐵, 𝐵) = 𝐵
75, 6eqtrdi 2791 1 ((𝑅 Or 𝐴𝐵𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106  ifcif 4531  {csn 4631  {cpr 4633   class class class wbr 5148   Or wor 5596  supcsup 9478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-po 5597  df-so 5598  df-iota 6516  df-riota 7388  df-sup 9480
This theorem is referenced by:  supxrmnf  13356  ramz  17059  xpsdsval  24407  ovolctb  25539  nmoo0  30820  nmop0  32015  nmfn0  32016  esumnul  34029  esum0  34030  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  liminf10ex  45730  fourierdlem79  46141  sge0z  46331  sge00  46332
  Copyright terms: Public domain W3C validator