Definition df-mre 17560

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 22976) and vector spaces (lssmre 20844) 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 17564, mresspw 17566, mre1cl 17568 and mreintcl 17569 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17574); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 17575. (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 17556	. 2 class Moore
2		vx	. . 3 setvar 𝑥
3		cvv 3470	. . 3 class V
4		vc	. . . . . 6 setvar 𝑐
5	2, 4	wel 2100	. . . . 5 wff 𝑥 ∈ 𝑐
6		vs	. . . . . . . . 9 setvar 𝑠
7	6	cv 1533	. . . . . . . 8 class 𝑠
8		c0 4319	. . . . . . . 8 class ∅
9	7, 8	wne 2936	. . . . . . 7 wff 𝑠 ≠ ∅
10	7	cint 4945	. . . . . . . 8 class ∩ 𝑠
11	4	cv 1533	. . . . . . . 8 class 𝑐
12	10, 11	wcel 2099	. . . . . . 7 wff ∩ 𝑠 ∈ 𝑐
13	9, 12	wi 4	. . . . . 6 wff (𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)
14	11	cpw 4599	. . . . . 6 class 𝒫 𝑐
15	13, 6, 14	wral 3057	. . . . 5 wff ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐)
16	5, 15	wa 395	. . . 4 wff (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))
17	2	cv 1533	. . . . . 6 class 𝑥
18	17	cpw 4599	. . . . 5 class 𝒫 𝑥
19	18	cpw 4599	. . . 4 class 𝒫 𝒫 𝑥
20	16, 4, 19	crab 3428	. . 3 class {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}
21	2, 3, 20	cmpt 5226	. 2 class (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})
22	1, 21	wceq 1534	1 wff Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})

This definition is referenced by:  ismre  17564  fnmre  17565

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »