| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-mre | Structured version Visualization version GIF version | ||
| 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 23086) and vector spaces (lssmre 20964)
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 17633, mresspw 17635, mre1cl 17637 and mreintcl 17638 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17643); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 17644. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
| Ref | Expression |
|---|---|
| df-mre | ⊢ Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cmre 17625 | . 2 class Moore | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | cvv 3480 | . . 3 class V | |
| 4 | vc | . . . . . 6 setvar 𝑐 | |
| 5 | 2, 4 | wel 2109 | . . . . 5 wff 𝑥 ∈ 𝑐 |
| 6 | vs | . . . . . . . . 9 setvar 𝑠 | |
| 7 | 6 | cv 1539 | . . . . . . . 8 class 𝑠 |
| 8 | c0 4333 | . . . . . . . 8 class ∅ | |
| 9 | 7, 8 | wne 2940 | . . . . . . 7 wff 𝑠 ≠ ∅ |
| 10 | 7 | cint 4946 | . . . . . . . 8 class ∩ 𝑠 |
| 11 | 4 | cv 1539 | . . . . . . . 8 class 𝑐 |
| 12 | 10, 11 | wcel 2108 | . . . . . . 7 wff ∩ 𝑠 ∈ 𝑐 |
| 13 | 9, 12 | wi 4 | . . . . . 6 wff (𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐) |
| 14 | 11 | cpw 4600 | . . . . . 6 class 𝒫 𝑐 |
| 15 | 13, 6, 14 | wral 3061 | . . . . 5 wff ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐) |
| 16 | 5, 15 | wa 395 | . . . 4 wff (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)) |
| 17 | 2 | cv 1539 | . . . . . 6 class 𝑥 |
| 18 | 17 | cpw 4600 | . . . . 5 class 𝒫 𝑥 |
| 19 | 18 | cpw 4600 | . . . 4 class 𝒫 𝒫 𝑥 |
| 20 | 16, 4, 19 | crab 3436 | . . 3 class {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))} |
| 21 | 2, 3, 20 | cmpt 5225 | . 2 class (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}) |
| 22 | 1, 21 | wceq 1540 | 1 wff Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: ismre 17633 fnmre 17634 |
| Copyright terms: Public domain | W3C validator |