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

Definition df-mre 13587
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 16921) and vector spaces (lssmre 15822) 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 13591, mresspw 13593, mre1cl 13595 and mreintcl 13596 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 13601); as such the disjoint union of all Moore collections is sometimes considered as  U. ran Moore, justified by mreunirn 13602. (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 13583 . 2  class Moore
2 vx . . 3  set  x
3 cvv 2864 . . 3  class  _V
4 vc . . . . . 6  set  c
52, 4wel 1711 . . . . 5  wff  x  e.  c
6 vs . . . . . . . . 9  set  s
76cv 1641 . . . . . . . 8  class  s
8 c0 3531 . . . . . . . 8  class  (/)
97, 8wne 2521 . . . . . . 7  wff  s  =/=  (/)
107cint 3943 . . . . . . . 8  class  |^| s
114cv 1641 . . . . . . . 8  class  c
1210, 11wcel 1710 . . . . . . 7  wff  |^| s  e.  c
139, 12wi 4 . . . . . 6  wff  ( s  =/=  (/)  ->  |^| s  e.  c )
1411cpw 3701 . . . . . 6  class  ~P c
1513, 6, 14wral 2619 . . . . 5  wff  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c )
165, 15wa 358 . . . 4  wff  ( x  e.  c  /\  A. s  e.  ~P  c
( s  =/=  (/)  ->  |^| s  e.  c ) )
172cv 1641 . . . . . 6  class  x
1817cpw 3701 . . . . 5  class  ~P x
1918cpw 3701 . . . 4  class  ~P ~P x
2016, 4, 19crab 2623 . . 3  class  { c  e.  ~P ~P x  |  ( x  e.  c  /\  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) }
212, 3, 20cmpt 4158 . 2  class  ( x  e.  _V  |->  { c  e.  ~P ~P x  |  ( x  e.  c  /\  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
221, 21wceq 1642 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  13591  fnmre  13592
  Copyright terms: Public domain W3C validator