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 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.) |
Ref | Expression |
---|---|
df-mre | ⊢ Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmre 16065 | . 2 class Moore | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cvv 3173 | . . 3 class V | |
4 | vc | . . . . . 6 setvar 𝑐 | |
5 | 2, 4 | wel 1978 | . . . . 5 wff 𝑥 ∈ 𝑐 |
6 | vs | . . . . . . . . 9 setvar 𝑠 | |
7 | 6 | cv 1474 | . . . . . . . 8 class 𝑠 |
8 | c0 3874 | . . . . . . . 8 class ∅ | |
9 | 7, 8 | wne 2780 | . . . . . . 7 wff 𝑠 ≠ ∅ |
10 | 7 | cint 4410 | . . . . . . . 8 class ∩ 𝑠 |
11 | 4 | cv 1474 | . . . . . . . 8 class 𝑐 |
12 | 10, 11 | wcel 1977 | . . . . . . 7 wff ∩ 𝑠 ∈ 𝑐 |
13 | 9, 12 | wi 4 | . . . . . 6 wff (𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐) |
14 | 11 | cpw 4108 | . . . . . 6 class 𝒫 𝑐 |
15 | 13, 6, 14 | wral 2896 | . . . . 5 wff ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐) |
16 | 5, 15 | wa 383 | . . . 4 wff (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)) |
17 | 2 | cv 1474 | . . . . . 6 class 𝑥 |
18 | 17 | cpw 4108 | . . . . 5 class 𝒫 𝑥 |
19 | 18 | cpw 4108 | . . . 4 class 𝒫 𝒫 𝑥 |
20 | 16, 4, 19 | crab 2900 | . . 3 class {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))} |
21 | 2, 3, 20 | cmpt 4643 | . 2 class (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}) |
22 | 1, 21 | wceq 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 |