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

Definition df-sup 7404
 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 11997. See dfsup2 7405 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 7403 . 2
5 vx . . . . . . . . 9
65cv 1648 . . . . . . . 8
7 vy . . . . . . . . 9
87cv 1648 . . . . . . . 8
96, 8, 3wbr 4172 . . . . . . 7
109wn 3 . . . . . 6
1110, 7, 1wral 2666 . . . . 5
128, 6, 3wbr 4172 . . . . . . 7
13 vz . . . . . . . . . 10
1413cv 1648 . . . . . . . . 9
158, 14, 3wbr 4172 . . . . . . . 8
1615, 13, 1wrex 2667 . . . . . . 7
1712, 16wi 4 . . . . . 6
1817, 7, 2wral 2666 . . . . 5
1911, 18wa 359 . . . 4
2019, 5, 2crab 2670 . . 3
2120cuni 3975 . 2
224, 21wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  dfsup2  7405  dfsup2OLD  7406  supeq1  7408  supeq2  7411  supexd  7414  supval2  7416  dfinfmr  9941  prdsds  13641  supex2g  26329  supeq123d  27026
 Copyright terms: Public domain W3C validator