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

Definition df-sup 7190
Description: Define the supremum of class  A. It is meaningful when  R is a relation that strictly orders  B and when the supremum exists. For example,  R could be 'less than',  B could be the set of real numbers, and  A 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 11717. See dfsup2 7191 for alternate definition not requiring dummy variables.

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

Assertion
Ref Expression
df-sup  |-  sup ( A ,  B ,  R )  =  U. { x  e.  B  |  ( A. y  e.  A  -.  x R y  /\  A. y  e.  B  (
y R x  ->  E. z  e.  A  y R z ) ) }
Distinct variable groups:    x, y,
z, R    x, A, y, z    x, B, y, z

Detailed syntax breakdown of Definition df-sup
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cR . . 3  class  R
41, 2, 3csup 7189 . 2  class  sup ( A ,  B ,  R )
5 vx . . . . . . . . 9  set  x
65cv 1623 . . . . . . . 8  class  x
7 vy . . . . . . . . 9  set  y
87cv 1623 . . . . . . . 8  class  y
96, 8, 3wbr 4025 . . . . . . 7  wff  x R y
109wn 5 . . . . . 6  wff  -.  x R y
1110, 7, 1wral 2545 . . . . 5  wff  A. y  e.  A  -.  x R y
128, 6, 3wbr 4025 . . . . . . 7  wff  y R x
13 vz . . . . . . . . . 10  set  z
1413cv 1623 . . . . . . . . 9  class  z
158, 14, 3wbr 4025 . . . . . . . 8  wff  y R z
1615, 13, 1wrex 2546 . . . . . . 7  wff  E. z  e.  A  y R
z
1712, 16wi 6 . . . . . 6  wff  ( y R x  ->  E. z  e.  A  y R
z )
1817, 7, 2wral 2545 . . . . 5  wff  A. y  e.  B  ( y R x  ->  E. z  e.  A  y R
z )
1911, 18wa 360 . . . 4  wff  ( A. y  e.  A  -.  x R y  /\  A. y  e.  B  (
y R x  ->  E. z  e.  A  y R z ) )
2019, 5, 2crab 2549 . . 3  class  { x  e.  B  |  ( A. y  e.  A  -.  x R y  /\  A. y  e.  B  ( y R x  ->  E. z  e.  A  y R z ) ) }
2120cuni 3829 . 2  class  U. {
x  e.  B  | 
( A. y  e.  A  -.  x R y  /\  A. y  e.  B  ( y R x  ->  E. z  e.  A  y R
z ) ) }
224, 21wceq 1624 1  wff  sup ( A ,  B ,  R )  =  U. { x  e.  B  |  ( A. y  e.  A  -.  x R y  /\  A. y  e.  B  (
y R x  ->  E. z  e.  A  y R z ) ) }
Colors of variables: wff set class
This definition is referenced by:  dfsup2  7191  dfsup2OLD  7192  supeq1  7194  supeq2  7197  supexd  7200  supval2  7202  dfinfmr  9727  prdsds  13358  supexr  25031  supex2g  25819  supeq123d  26558
  Copyright terms: Public domain W3C validator