Theorem supsn 9502

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 4597	. . . 4 ⊢ {𝐵} = {𝐵, 𝐵}
2	1	supeq1i 9476	. . 3 ⊢ sup({𝐵}, 𝐴, 𝑅) = sup({𝐵, 𝐵}, 𝐴, 𝑅)
3		suppr 9501	. . . 4 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵, 𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
4	3	3anidm23 1449	. . 3 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵, 𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
5	2, 4	eqtrid 2810	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵}, 𝐴, 𝑅) = if(𝐵𝑅𝐵, 𝐵, 𝐵))
6		ifid 4526	. 2 ⊢ if(𝐵𝑅𝐵, 𝐵, 𝐵) = 𝐵
7	5, 6	eqtrdi 2814	1 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ifcif 4485  {csn 4588  {cpr 4590   class class class wbr 5108   Or wor 5565  supcsup 9469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-po 5566  df-so 5567  df-iota 6520  df-riota 7408  df-sup 9471

This theorem is used by:  supxrmnf  13487  ramz  17247  xpsdsval  24755  ovolctb  25866  nmoo0  31450  nmop0  32645  nmfn0  32646  esumnul  34791  esum0  34792  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  liminf10ex  47057  fourierdlem79  47468  sge0z  47658  sge00  47659