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

Definition df-sup 7921
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 13070. See dfsup2 7922 for alternate definition not requiring dummy variables.

We will also use this notation for "infimum" by replacing with . (Contributed by NM, 22-May-1999.)

Assertion
Ref Expression
df-sup
Distinct variable groups:   , , ,   , , ,   , , ,

Detailed syntax breakdown of Definition df-sup
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cR . . 3
41, 2, 3csup 7920 . 2
5 vx . . . . . . . . 9
65cv 1394 . . . . . . . 8
7 vy . . . . . . . . 9
87cv 1394 . . . . . . . 8
96, 8, 3wbr 4452 . . . . . . 7
109wn 3 . . . . . 6
1110, 7, 1wral 2807 . . . . 5
128, 6, 3wbr 4452 . . . . . . 7
13 vz . . . . . . . . . 10
1413cv 1394 . . . . . . . . 9
158, 14, 3wbr 4452 . . . . . . . 8
1615, 13, 1wrex 2808 . . . . . . 7
1712, 16wi 4 . . . . . 6
1817, 7, 2wral 2807 . . . . 5
1911, 18wa 369 . . . 4
2019, 5, 2crab 2811 . . 3
2120cuni 4249 . 2
224, 21wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  dfsup2  7922  dfsup2OLD  7923  supeq1  7925  supeq2  7928  supeq3  7929  supeq123d  7930  supexd  7933  supval2  7935  dfinfmr  10545  prdsds  14861  supex2g  30228
  Copyright terms: Public domain W3C validator