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

Step	Hyp	Ref	Expression
1		dfsn2 4590	. . . 4 ⊢ {𝐵} = {𝐵, 𝐵}
2	1	supeq1i 9340	. . 3 ⊢ sup({𝐵}, 𝐴, 𝑅) = sup({𝐵, 𝐵}, 𝐴, 𝑅)
3		suppr 9365	. . . 4 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵, 𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
4	3	3anidm23 1423	. . 3 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵, 𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
5	2, 4	eqtrid 2780	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
6		ifid 4517	. 2 ⊢ if(𝐵𝑅𝐵, 𝐵, 𝐵) = 𝐵
7	5, 6	eqtrdi 2784	1 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ifcif 4476  {csn 4577  {cpr 4579   class class class wbr 5095   Or wor 5528  supcsup 9333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-po 5529  df-so 5530  df-iota 6444  df-riota 7311  df-sup 9335

This theorem is referenced by:  supxrmnf  13220  ramz  16941  xpsdsval  24299  ovolctb  25421  nmoo0  30775  nmop0  31970  nmfn0  31971  esumnul  34084  esum0  34085  ovoliunnfl  37725  voliunnfl  37727  volsupnfl  37728  liminf10ex  45899  fourierdlem79  46310  sge0z  46500  sge00  46501