Definition df-mre 17695

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 23335) and vector spaces (lssmre 21180) 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 17699, mresspw 17701, mre1cl 17703 and mreintcl 17704 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17709); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 17710. (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 17691	. 2 class Moore
2		vx	. . 3 setvar 𝑥
3		cvv 3450	. . 3 class V
4		vc	. . . . . 6 setvar 𝑐
5	2, 4	wel 2146	. . . . 5 wff 𝑥 ∈ 𝑐
6		vs	. . . . . . . . 9 setvar 𝑠
7	6	cv 1569	. . . . . . . 8 class 𝑠
8		c0 4279	. . . . . . . 8 class ∅
9	7, 8	wne 2955	. . . . . . 7 wff 𝑠 ≠ ∅
10	7	cint 4907	. . . . . . . 8 class ∩ 𝑠
11	4	cv 1569	. . . . . . . 8 class 𝑐
12	10, 11	wcel 2145	. . . . . . 7 wff ∩ 𝑠 ∈ 𝑐
13	9, 12	wi 4	. . . . . 6 wff (𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)
14	11	cpw 4557	. . . . . 6 class 𝒫 𝑐
15	13, 6, 14	wral 3076	. . . . 5 wff ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)
16	5, 15	wa 401	. . . 4 wff (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))
17	2	cv 1569	. . . . . 6 class 𝑥
18	17	cpw 4557	. . . . 5 class 𝒫 𝑥
19	18	cpw 4557	. . . 4 class 𝒫 𝒫 𝑥
20	16, 4, 19	crab 3412	. . 3 class {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}
21	2, 3, 20	cmpt 5186	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})
22	1, 21	wceq 1570	1 wff Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})

This definition is used by:  ismre  17699  fnmre  17700