Definition df-mre 17547

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 22965) and vector spaces (lssmre 20872) 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 17551, mresspw 17553, mre1cl 17555 and mreintcl 17556 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17561); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 17562. (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

Step	Hyp	Ref	Expression
1		cmre 17543	. 2 class Moore
2		vx	. . 3 setvar 𝑥
3		cvv 3447	. . 3 class V
4		vc	. . . . . 6 setvar 𝑐
5	2, 4	wel 2110	. . . . 5 wff 𝑥 ∈ 𝑐
6		vs	. . . . . . . . 9 setvar 𝑠
7	6	cv 1539	. . . . . . . 8 class 𝑠
8		c0 4296	. . . . . . . 8 class ∅
9	7, 8	wne 2925	. . . . . . 7 wff 𝑠 ≠ ∅
10	7	cint 4910	. . . . . . . 8 class ∩ 𝑠
11	4	cv 1539	. . . . . . . 8 class 𝑐
12	10, 11	wcel 2109	. . . . . . 7 wff ∩ 𝑠 ∈ 𝑐
13	9, 12	wi 4	. . . . . 6 wff (𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)
14	11	cpw 4563	. . . . . 6 class 𝒫 𝑐
15	13, 6, 14	wral 3044	. . . . 5 wff ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)
16	5, 15	wa 395	. . . 4 wff (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))
17	2	cv 1539	. . . . . 6 class 𝑥
18	17	cpw 4563	. . . . 5 class 𝒫 𝑥
19	18	cpw 4563	. . . 4 class 𝒫 𝒫 𝑥
20	16, 4, 19	crab 3405	. . 3 class {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}
21	2, 3, 20	cmpt 5188	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})
22	1, 21	wceq 1540	1 wff Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})

This definition is referenced by:  ismre  17551  fnmre  17552