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

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

Detailed syntax breakdown of Definition df-mnl
StepHypRef Expression
1 cmnl 25320 . 2  class  mnl
2 vr . . 3  set  r
3 cvv 2801 . . 3  class  _V
4 vb . . . . . . . 8  set  b
54cv 1631 . . . . . . 7  class  b
6 va . . . . . . . 8  set  a
76cv 1631 . . . . . . 7  class  a
82cv 1631 . . . . . . 7  class  r
95, 7, 8wbr 4039 . . . . . 6  wff  b r a
104, 6weq 1633 . . . . . 6  wff  b  =  a
119, 10wi 4 . . . . 5  wff  ( b r a  ->  b  =  a )
128cuni 3843 . . . . . 6  class  U. r
1312cuni 3843 . . . . 5  class  U. U. r
1411, 4, 13wral 2556 . . . 4  wff  A. b  e.  U. U. r ( b r a  -> 
b  =  a )
1514, 6, 13crab 2560 . . 3  class  { a  e.  U. U. r  |  A. b  e.  U. U. r ( b r a  ->  b  =  a ) }
162, 3, 15cmpt 4093 . 2  class  ( r  e.  _V  |->  { a  e.  U. U. r  |  A. b  e.  U. U. r ( b r a  ->  b  =  a ) } )
171, 16wceq 1632 1  wff  mnl  =  ( r  e.  _V  |->  { a  e.  U. U. r  |  A. b  e.  U. U. r ( b r a  -> 
b  =  a ) } )
Colors of variables: wff set class
This definition is referenced by:  mnlelt2  25369
  Copyright terms: Public domain W3C validator