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

Definition df-sup 7448
 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 12044. See dfsup2 7449 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 7447 . 2
5 vx . . . . . . . . 9
65cv 1652 . . . . . . . 8
7 vy . . . . . . . . 9
87cv 1652 . . . . . . . 8
96, 8, 3wbr 4214 . . . . . . 7
109wn 3 . . . . . 6
1110, 7, 1wral 2707 . . . . 5
128, 6, 3wbr 4214 . . . . . . 7
13 vz . . . . . . . . . 10
1413cv 1652 . . . . . . . . 9
158, 14, 3wbr 4214 . . . . . . . 8
1615, 13, 1wrex 2708 . . . . . . 7
1712, 16wi 4 . . . . . 6
1817, 7, 2wral 2707 . . . . 5
1911, 18wa 360 . . . 4
2019, 5, 2crab 2711 . . 3
2120cuni 4017 . 2
224, 21wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  dfsup2  7449  dfsup2OLD  7450  supeq1  7452  supeq2  7455  supeq3  7456  supeq123d  7457  supexd  7460  supval2  7462  dfinfmr  9987  prdsds  13688  supex2g  26441
 Copyright terms: Public domain W3C validator