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 = ( 𝑥 ∈ V ↦ { 𝑐 ∈ 𝒫 𝒫 𝑥 ∣ ( 𝑥 ∈ 𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐 ) ) } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cmre | ⊢ Moore | |
| 1 | vx | ⊢ 𝑥 | |
| 2 | cvv | ⊢ V | |
| 3 | vc | ⊢ 𝑐 | |
| 4 | 1 | cv | ⊢ 𝑥 |
| 5 | 4 | cpw | ⊢ 𝒫 𝑥 |
| 6 | 5 | cpw | ⊢ 𝒫 𝒫 𝑥 |
| 7 | 3 | cv | ⊢ 𝑐 |
| 8 | 4 7 | wcel | ⊢ 𝑥 ∈ 𝑐 |
| 9 | vs | ⊢ 𝑠 | |
| 10 | 7 | cpw | ⊢ 𝒫 𝑐 |
| 11 | 9 | cv | ⊢ 𝑠 |
| 12 | c0 | ⊢ ∅ | |
| 13 | 11 12 | wne | ⊢ 𝑠 ≠ ∅ |
| 14 | 11 | cint | ⊢ ∩ 𝑠 |
| 15 | 14 7 | wcel | ⊢ ∩ 𝑠 ∈ 𝑐 |
| 16 | 13 15 | wi | ⊢ ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐 ) |
| 17 | 16 9 10 | wral | ⊢ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐 ) |
| 18 | 8 17 | wa | ⊢ ( 𝑥 ∈ 𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐 ) ) |
| 19 | 18 3 6 | crab | ⊢ { 𝑐 ∈ 𝒫 𝒫 𝑥 ∣ ( 𝑥 ∈ 𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐 ) ) } |
| 20 | 1 2 19 | cmpt | ⊢ ( 𝑥 ∈ V ↦ { 𝑐 ∈ 𝒫 𝒫 𝑥 ∣ ( 𝑥 ∈ 𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐 ) ) } ) |
| 21 | 0 20 | wceq | ⊢ Moore = ( 𝑥 ∈ V ↦ { 𝑐 ∈ 𝒫 𝒫 𝑥 ∣ ( 𝑥 ∈ 𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐 ) ) } ) |