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

Definition df-sup 7683
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 sqrval 12718. See dfsup2 7684 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 7682 . 2
5 vx . . . . . . . . 9
65cv 1368 . . . . . . . 8
7 vy . . . . . . . . 9
87cv 1368 . . . . . . . 8
96, 8, 3wbr 4287 . . . . . . 7
109wn 3 . . . . . 6
1110, 7, 1wral 2710 . . . . 5
128, 6, 3wbr 4287 . . . . . . 7
13 vz . . . . . . . . . 10
1413cv 1368 . . . . . . . . 9
158, 14, 3wbr 4287 . . . . . . . 8
1615, 13, 1wrex 2711 . . . . . . 7
1712, 16wi 4 . . . . . 6
1817, 7, 2wral 2710 . . . . 5
1911, 18wa 369 . . . 4
2019, 5, 2crab 2714 . . 3
2120cuni 4086 . 2
224, 21wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  dfsup2  7684  dfsup2OLD  7685  supeq1  7687  supeq2  7690  supeq3  7691  supeq123d  7692  supexd  7695  supval2  7697  dfinfmr  10299  prdsds  14394  supex2g  28602
  Copyright terms: Public domain W3C validator