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

Theorem supsn 9366
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 4597 . . . 4 {𝐵} = {𝐵, 𝐵}
21supeq1i 9341 . . 3 sup({𝐵}, 𝐴, 𝑅) = sup({𝐵, 𝐵}, 𝐴, 𝑅)
3 suppr 9365 . . . 4 ((𝑅 Or 𝐴𝐵𝐴𝐵𝐴) → sup({𝐵, 𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
433anidm23 1421 . . 3 ((𝑅 Or 𝐴𝐵𝐴) → sup({𝐵, 𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
52, 4eqtrid 2788 . 2 ((𝑅 Or 𝐴𝐵𝐴) → sup({𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
6 ifid 4524 . 2 if(𝐵𝑅𝐵, 𝐵, 𝐵) = 𝐵
75, 6eqtrdi 2792 1 ((𝑅 Or 𝐴𝐵𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  ifcif 4484  {csn 4584  {cpr 4586   class class class wbr 5103   Or wor 5542  supcsup 9334
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
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 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-po 5543  df-so 5544  df-iota 6445  df-riota 7307  df-sup 9336
This theorem is referenced by:  supxrmnf  13190  ramz  16851  xpsdsval  23680  ovolctb  24800  nmoo0  29578  nmop0  30773  nmfn0  30774  esumnul  32475  esum0  32476  ovoliunnfl  36052  voliunnfl  36054  volsupnfl  36055  liminf10ex  43910  fourierdlem79  44321  sge0z  44511  sge00  44512
  Copyright terms: Public domain W3C validator