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

Definition df-mre 13766
 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 17097) and vector spaces (lssmre 15997) 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 13770, mresspw 13772, mre1cl 13774 and mreintcl 13775 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 13780); as such the disjoint union of all Moore collections is sometimes considered as Moore, justified by mreunirn 13781. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.)
Assertion
Ref Expression
df-mre Moore
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-mre
StepHypRef Expression
1 cmre 13762 . 2 Moore
2 vx . . 3
3 cvv 2916 . . 3
4 vc . . . . . 6
52, 4wel 1722 . . . . 5
6 vs . . . . . . . . 9
76cv 1648 . . . . . . . 8
8 c0 3588 . . . . . . . 8
97, 8wne 2567 . . . . . . 7
107cint 4010 . . . . . . . 8
114cv 1648 . . . . . . . 8
1210, 11wcel 1721 . . . . . . 7
139, 12wi 4 . . . . . 6
1411cpw 3759 . . . . . 6
1513, 6, 14wral 2666 . . . . 5
165, 15wa 359 . . . 4
172cv 1648 . . . . . 6
1817cpw 3759 . . . . 5
1918cpw 3759 . . . 4
2016, 4, 19crab 2670 . . 3
212, 3, 20cmpt 4226 . 2
221, 21wceq 1649 1 Moore
 Colors of variables: wff set class This definition is referenced by:  ismre  13770  fnmre  13771
 Copyright terms: Public domain W3C validator