Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ub Unicode version

Definition df-ub 25253
Description: Define the upper bounds of a set  x. Meaningful if  r is at least a preset, and  x a subset of the field of 
r. Bourbaki E.III.9 def. 5. Experimental. (Contributed by FL, 16-May-2011.)
Assertion
Ref Expression
df-ub  |-  ub  =  ( r  e.  _V ,  x  e.  _V  |->  { a  e.  U. U. r  |  A. b  e.  x  b r
a } )
Distinct variable group:    x, r, a, b

Detailed syntax breakdown of Definition df-ub
StepHypRef Expression
1 cub 25218 . 2  class  ub
2 vr . . 3  set  r
3 vx . . 3  set  x
4 cvv 2788 . . 3  class  _V
5 vb . . . . . . 7  set  b
65cv 1622 . . . . . 6  class  b
7 va . . . . . . 7  set  a
87cv 1622 . . . . . 6  class  a
92cv 1622 . . . . . 6  class  r
106, 8, 9wbr 4023 . . . . 5  wff  b r a
113cv 1622 . . . . 5  class  x
1210, 5, 11wral 2543 . . . 4  wff  A. b  e.  x  b r
a
139cuni 3827 . . . . 5  class  U. r
1413cuni 3827 . . . 4  class  U. U. r
1512, 7, 14crab 2547 . . 3  class  { a  e.  U. U. r  |  A. b  e.  x  b r a }
162, 3, 4, 4, 15cmpt2 5860 . 2  class  ( r  e.  _V ,  x  e.  _V  |->  { a  e. 
U. U. r  |  A. b  e.  x  b
r a } )
171, 16wceq 1623 1  wff  ub  =  ( r  e.  _V ,  x  e.  _V  |->  { a  e.  U. U. r  |  A. b  e.  x  b r
a } )
Colors of variables: wff set class
This definition is referenced by:  ubos  25256
  Copyright terms: Public domain W3C validator