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

Definition df-mre 13361
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 16647) and vector spaces (lssmre 15558) to the most general setting in which such concepts make sense. Definition of Moore collection of sets in [Schechter] p. 78.

See ismre 13364, mresspw 13366, mre1cl 13368 and mreintcl 13369 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 13374); as such the disjoint union of all Moore collections is sometimes considered as  U. ran Moore, justified by mreunirn 13375. (Contributed by Stefan O'Rear, 30-Jan-2015.)

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 13358 . 2  class Moore
2 vx . . 3  set  x
3 cvv 2727 . . 3  class  _V
4 vc . . . . . 6  set  c
52, 4wel 1622 . . . . 5  wff  x  e.  c
6 vs . . . . . . . . 9  set  s
76cv 1618 . . . . . . . 8  class  s
8 c0 3362 . . . . . . . 8  class  (/)
97, 8wne 2412 . . . . . . 7  wff  s  =/=  (/)
107cint 3760 . . . . . . . 8  class  |^| s
114cv 1618 . . . . . . . 8  class  c
1210, 11wcel 1621 . . . . . . 7  wff  |^| s  e.  c
139, 12wi 6 . . . . . 6  wff  ( s  =/=  (/)  ->  |^| s  e.  c )
1411cpw 3530 . . . . . 6  class  ~P c
1513, 6, 14wral 2509 . . . . 5  wff  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c )
165, 15wa 360 . . . 4  wff  ( x  e.  c  /\  A. s  e.  ~P  c
( s  =/=  (/)  ->  |^| s  e.  c ) )
172cv 1618 . . . . . 6  class  x
1817cpw 3530 . . . . 5  class  ~P x
1918cpw 3530 . . . 4  class  ~P ~P x
2016, 4, 19crab 2512 . . 3  class  { c  e.  ~P ~P x  |  ( x  e.  c  /\  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) }
212, 3, 20cmpt 3974 . 2  class  ( x  e.  _V  |->  { c  e.  ~P ~P x  |  ( x  e.  c  /\  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
221, 21wceq 1619 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  13364  fnmre  13365
  Copyright terms: Public domain W3C validator