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

Definition df-mxl 25246
Description: Define the maximal elements of a set. I.e. the elements of the set that are not smaller than the other elements. Meaningful if  r is at least a preset. Read  ( mxl `  R
) as the maximal elements of the set  U. U. R preordered by  R. Bourbaki E III 8. Experimental. (Contributed by FL, 16-May-2011.)
Assertion
Ref Expression
df-mxl  |-  mxl  =  ( r  e.  _V  |->  { a  e.  U. U. r  |  A. b  e.  U. U. r ( a r b  -> 
a  =  b ) } )
Distinct variable group:    r, a, b

Detailed syntax breakdown of Definition df-mxl
StepHypRef Expression
1 cmxl 25216 . 2  class  mxl
2 vr . . 3  set  r
3 cvv 2788 . . 3  class  _V
4 va . . . . . . . 8  set  a
54cv 1622 . . . . . . 7  class  a
6 vb . . . . . . . 8  set  b
76cv 1622 . . . . . . 7  class  b
82cv 1622 . . . . . . 7  class  r
95, 7, 8wbr 4023 . . . . . 6  wff  a r b
104, 6weq 1624 . . . . . 6  wff  a  =  b
119, 10wi 4 . . . . 5  wff  ( a r b  ->  a  =  b )
128cuni 3827 . . . . . 6  class  U. r
1312cuni 3827 . . . . 5  class  U. U. r
1411, 6, 13wral 2543 . . . 4  wff  A. b  e.  U. U. r ( a r b  -> 
a  =  b )
1514, 4, 13crab 2547 . . 3  class  { a  e.  U. U. r  |  A. b  e.  U. U. r ( a r b  ->  a  =  b ) }
162, 3, 15cmpt 4077 . 2  class  ( r  e.  _V  |->  { a  e.  U. U. r  |  A. b  e.  U. U. r ( a r b  ->  a  =  b ) } )
171, 16wceq 1623 1  wff  mxl  =  ( r  e.  _V  |->  { a  e.  U. U. r  |  A. b  e.  U. U. r ( a r b  -> 
a  =  b ) } )
Colors of variables: wff set class
This definition is referenced by:  mxlelt  25264
  Copyright terms: Public domain W3C validator