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

Definition df-sup 8972
Description: Define the supremum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the supremum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 could be the set of all positive reals whose square is less than 2; in this case the supremum is defined as the square root of 2 per sqrtval 14679. See dfsup2 8974 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.)
Assertion
Ref Expression
df-sup sup(𝐴, 𝐵, 𝑅) = {𝑥𝐵 ∣ (∀𝑦𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧))}
Distinct variable groups:   𝑥,𝑦,𝑧,𝑅   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧

Detailed syntax breakdown of Definition df-sup
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cR . . 3 class 𝑅
41, 2, 3csup 8970 . 2 class sup(𝐴, 𝐵, 𝑅)
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1541 . . . . . . . 8 class 𝑥
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1541 . . . . . . . 8 class 𝑦
96, 8, 3wbr 5027 . . . . . . 7 wff 𝑥𝑅𝑦
109wn 3 . . . . . 6 wff ¬ 𝑥𝑅𝑦
1110, 7, 1wral 3053 . . . . 5 wff 𝑦𝐴 ¬ 𝑥𝑅𝑦
128, 6, 3wbr 5027 . . . . . . 7 wff 𝑦𝑅𝑥
13 vz . . . . . . . . . 10 setvar 𝑧
1413cv 1541 . . . . . . . . 9 class 𝑧
158, 14, 3wbr 5027 . . . . . . . 8 wff 𝑦𝑅𝑧
1615, 13, 1wrex 3054 . . . . . . 7 wff 𝑧𝐴 𝑦𝑅𝑧
1712, 16wi 4 . . . . . 6 wff (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧)
1817, 7, 2wral 3053 . . . . 5 wff 𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧)
1911, 18wa 399 . . . 4 wff (∀𝑦𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧))
2019, 5, 2crab 3057 . . 3 class {𝑥𝐵 ∣ (∀𝑦𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧))}
2120cuni 4793 . 2 class {𝑥𝐵 ∣ (∀𝑦𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧))}
224, 21wceq 1542 1 wff sup(𝐴, 𝐵, 𝑅) = {𝑥𝐵 ∣ (∀𝑦𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  dfsup2  8974  supeq1  8975  supeq2  8978  supeq3  8979  supeq123d  8980  supexd  8983  supval2  8985  sup00  8994  dfinfre  11692  prdsds  16833  supex2g  35507
  Copyright terms: Public domain W3C validator