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

Definition df-mre 13801
Description: Define a Moore collection, which is a family of subsets of a base set which preserve arbitrary intersection. Elements of a Moore collection are termed closed; Moore collections generalize the notion of closedness from topologies (cldmre 17132) and vector spaces (lssmre 16032) to the most general setting in which such concepts make sense. Definition of Moore collection of sets in [Schechter] p. 78. A Moore collection may also be called a closure system (Section 0.6 in [Gratzer] p. 23.) The name Moore collection is after Eliakim Hastings Moore, who discussed these systems in Part I of [Moore] p. 53 to 76.

See ismre 13805, mresspw 13807, mre1cl 13809 and mreintcl 13810 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 13815); as such the disjoint union of all Moore collections is sometimes considered as  U. ran Moore, justified by mreunirn 13816. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.)

Assertion
Ref Expression
df-mre  |- Moore  =  ( x  e.  _V  |->  { c  e.  ~P ~P x  |  ( x  e.  c  /\  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
Distinct variable group:    s, c, x

Detailed syntax breakdown of Definition df-mre
StepHypRef Expression
1 cmre 13797 . 2  class Moore
2 vx . . 3  set  x
3 cvv 2948 . . 3  class  _V
4 vc . . . . . 6  set  c
52, 4wel 1726 . . . . 5  wff  x  e.  c
6 vs . . . . . . . . 9  set  s
76cv 1651 . . . . . . . 8  class  s
8 c0 3620 . . . . . . . 8  class  (/)
97, 8wne 2598 . . . . . . 7  wff  s  =/=  (/)
107cint 4042 . . . . . . . 8  class  |^| s
114cv 1651 . . . . . . . 8  class  c
1210, 11wcel 1725 . . . . . . 7  wff  |^| s  e.  c
139, 12wi 4 . . . . . 6  wff  ( s  =/=  (/)  ->  |^| s  e.  c )
1411cpw 3791 . . . . . 6  class  ~P c
1513, 6, 14wral 2697 . . . . 5  wff  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c )
165, 15wa 359 . . . 4  wff  ( x  e.  c  /\  A. s  e.  ~P  c
( s  =/=  (/)  ->  |^| s  e.  c ) )
172cv 1651 . . . . . 6  class  x
1817cpw 3791 . . . . 5  class  ~P x
1918cpw 3791 . . . 4  class  ~P ~P x
2016, 4, 19crab 2701 . . 3  class  { c  e.  ~P ~P x  |  ( x  e.  c  /\  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) }
212, 3, 20cmpt 4258 . 2  class  ( x  e.  _V  |->  { c  e.  ~P ~P x  |  ( x  e.  c  /\  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
221, 21wceq 1652 1  wff Moore  =  ( x  e.  _V  |->  { c  e.  ~P ~P x  |  ( x  e.  c  /\  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
Colors of variables: wff set class
This definition is referenced by:  ismre  13805  fnmre  13806
  Copyright terms: Public domain W3C validator