Metamath Proof Explorer

Definition df-mre

Description: Define aMoore collection, which is a family of subsets of a base set which preserve arbitrary intersection. Elements of a Moore collection are termedclosed; Moore collections generalize the notion of closedness from topologies ( cldmre ) and vector spaces ( lssmre ) 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 aclosure system (Section 0.6 in Gratzer p. 23.) The nameMoore collection is after Eliakim Hastings Moore, who discussed these systems in Part I of Moore p. 53 to 76.

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

Ref Expression
Assertion df-mre ⊢Moore=x∈V⟼c∈𝒫𝒫x|x∈c∧∀s∈𝒫cs≠∅→⋂s∈c

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmre classMoore
1 vx setvarx
2 cvv classV
3 vc setvarc
4 1 cv setvarx
5 4 cpw class𝒫x
6 5 cpw class𝒫𝒫x
7 3 cv setvarc
8 4 7 wcel wffx∈c
9 vs setvars
10 7 cpw class𝒫c
11 9 cv setvars
12 c0 class∅
13 11 12 wne wffs≠∅
14 11 cint class⋂s
15 14 7 wcel wff⋂s∈c
16 13 15 wi wffs≠∅→⋂s∈c
17 16 9 10 wral wff∀s∈𝒫cs≠∅→⋂s∈c
18 8 17 wa wffx∈c∧∀s∈𝒫cs≠∅→⋂s∈c
19 18 3 6 crab classc∈𝒫𝒫x|x∈c∧∀s∈𝒫cs≠∅→⋂s∈c
20 1 2 19 cmpt classx∈V⟼c∈𝒫𝒫x|x∈c∧∀s∈𝒫cs≠∅→⋂s∈c
21 0 20 wceq wffMoore=x∈V⟼c∈𝒫𝒫x|x∈c∧∀s∈𝒫cs≠∅→⋂s∈c