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 ∈ 𝒫 c s ≠ ∅ → ⋂ s ∈ c

Detailed syntax breakdown

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