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

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

Detailed syntax breakdown of Definition df-lb
StepHypRef Expression
1 clb 25322 . 2  class  lb
2 vr . . 3  set  r
3 vx . . 3  set  x
4 cvv 2801 . . 3  class  _V
5 va . . . . . . 7  set  a
65cv 1631 . . . . . 6  class  a
7 vb . . . . . . 7  set  b
87cv 1631 . . . . . 6  class  b
92cv 1631 . . . . . 6  class  r
106, 8, 9wbr 4039 . . . . 5  wff  a r b
113cv 1631 . . . . 5  class  x
1210, 7, 11wral 2556 . . . 4  wff  A. b  e.  x  a r
b
139cuni 3843 . . . . 5  class  U. r
1413cuni 3843 . . . 4  class  U. U. r
1512, 5, 14crab 2560 . . 3  class  { a  e.  U. U. r  |  A. b  e.  x  a r b }
162, 3, 4, 4, 15cmpt2 5876 . 2  class  ( r  e.  _V ,  x  e.  _V  |->  { a  e. 
U. U. r  |  A. b  e.  x  a
r b } )
171, 16wceq 1632 1  wff  lb  =  ( r  e.  _V ,  x  e.  _V  |->  { a  e.  U. U. r  |  A. b  e.  x  a r
b } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator