Definition df-mre 16447

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 21093) and vector spaces (lssmre 19169) 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 16451, mresspw 16453, mre1cl 16455 and mreintcl 16456 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 16461); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 16462. (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 16443	. 2 class Moore
2		vx	. . 3 setvar 𝑥
3		cvv 3391	. . 3 class V
4		vc	. . . . . 6 setvar 𝑐
5	2, 4	wel 2157	. . . . 5 wff 𝑥 ∈ 𝑐
6		vs	. . . . . . . . 9 setvar 𝑠
7	6	cv 1636	. . . . . . . 8 class 𝑠
8		c0 4116	. . . . . . . 8 class ∅
9	7, 8	wne 2978	. . . . . . 7 wff 𝑠 ≠ ∅
10	7	cint 4669	. . . . . . . 8 class ∩ 𝑠
11	4	cv 1636	. . . . . . . 8 class 𝑐
12	10, 11	wcel 2156	. . . . . . 7 wff ∩ 𝑠 ∈ 𝑐
13	9, 12	wi 4	. . . . . 6 wff (𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)
14	11	cpw 4351	. . . . . 6 class 𝒫 𝑐
15	13, 6, 14	wral 3096	. . . . 5 wff ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)
16	5, 15	wa 384	. . . 4 wff (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))
17	2	cv 1636	. . . . . 6 class 𝑥
18	17	cpw 4351	. . . . 5 class 𝒫 𝑥
19	18	cpw 4351	. . . 4 class 𝒫 𝒫 𝑥
20	16, 4, 19	crab 3100	. . 3 class {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}
21	2, 3, 20	cmpt 4923	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})
22	1, 21	wceq 1637	1 wff Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})

This definition is referenced by:  ismre  16451  fnmre  16452