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

Definition df-mre 16069
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 20692) and vector spaces (lssmre 18787) 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 16073, mresspw 16075, mre1cl 16077 and mreintcl 16078 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 16083); as such the disjoint union of all Moore collections is sometimes considered as ran Moore, justified by mreunirn 16084. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.)

Assertion
Ref Expression
df-mre Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → 𝑠𝑐))})
Distinct variable group:   𝑠,𝑐,𝑥

Detailed syntax breakdown of Definition df-mre
StepHypRef Expression
1 cmre 16065 . 2 class Moore
2 vx . . 3 setvar 𝑥
3 cvv 3173 . . 3 class V
4 vc . . . . . 6 setvar 𝑐
52, 4wel 1978 . . . . 5 wff 𝑥𝑐
6 vs . . . . . . . . 9 setvar 𝑠
76cv 1474 . . . . . . . 8 class 𝑠
8 c0 3874 . . . . . . . 8 class
97, 8wne 2780 . . . . . . 7 wff 𝑠 ≠ ∅
107cint 4410 . . . . . . . 8 class 𝑠
114cv 1474 . . . . . . . 8 class 𝑐
1210, 11wcel 1977 . . . . . . 7 wff 𝑠𝑐
139, 12wi 4 . . . . . 6 wff (𝑠 ≠ ∅ → 𝑠𝑐)
1411cpw 4108 . . . . . 6 class 𝒫 𝑐
1513, 6, 14wral 2896 . . . . 5 wff 𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → 𝑠𝑐)
165, 15wa 383 . . . 4 wff (𝑥𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → 𝑠𝑐))
172cv 1474 . . . . . 6 class 𝑥
1817cpw 4108 . . . . 5 class 𝒫 𝑥
1918cpw 4108 . . . 4 class 𝒫 𝒫 𝑥
2016, 4, 19crab 2900 . . 3 class {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → 𝑠𝑐))}
212, 3, 20cmpt 4643 . 2 class (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → 𝑠𝑐))})
221, 21wceq 1475 1 wff Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → 𝑠𝑐))})
Colors of variables: wff setvar class
This definition is referenced by:  ismre  16073  fnmre  16074
  Copyright terms: Public domain W3C validator