Definition df-mrc 17305

Description: Define the Moore closure of a generating set, which is the smallest closed set containing all generating elements. Definition of Moore closure in [Schechter] p. 79. This generalizes topological closure (mrccls 22239) and linear span (mrclsp 20260).

A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcssid 17335), (2) isotone, i.e., 𝑥 ⊆ 𝑦 implies that (𝑁‘𝑥) ⊆ (𝑁‘𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 17334), and (3) idempotent, i.e., (𝑁‘(𝑁‘𝑥)) = (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcidm 17337.) Operators satisfying these three properties are in bijective correspondence with Moore collections, so these properties may be used to give an alternate characterization of a Moore collection by providing a closure operation 𝑁 on the set of subsets of a given base set which satisfies (1), (2), and (3); the closed sets can be recovered as those sets which equal their closures (Section 4.5 in [Schechter] p. 82.) (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by David Moews, 1-May-2017.)

Assertion

Ref	Expression
df-mrc	⊢ mrCls = (𝑐 ∈ ∪ ran Moore ↦ (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}))

Distinct variable group:   𝑠,𝑐,𝑥

Detailed syntax breakdown of Definition df-mrc

Step	Hyp	Ref	Expression
1		cmrc 17301	. 2 class mrCls
2		vc	. . 3 setvar 𝑐
3		cmre 17300	. . . . 5 class Moore
4	3	crn 5591	. . . 4 class ran Moore
5	4	cuni 4840	. . 3 class ∪ ran Moore
6		vx	. . . 4 setvar 𝑥
7	2	cv 1538	. . . . . 6 class 𝑐
8	7	cuni 4840	. . . . 5 class ∪ 𝑐
9	8	cpw 4534	. . . 4 class 𝒫 ∪ 𝑐
10	6	cv 1538	. . . . . . 7 class 𝑥
11		vs	. . . . . . . 8 setvar 𝑠
12	11	cv 1538	. . . . . . 7 class 𝑠
13	10, 12	wss 3888	. . . . . 6 wff 𝑥 ⊆ 𝑠
14	13, 11, 7	crab 3069	. . . . 5 class {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}
15	14	cint 4880	. . . 4 class ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}
16	6, 9, 15	cmpt 5158	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠})
17	2, 5, 16	cmpt 5158	. 2 class (𝑐 ∈ ∪ ran Moore ↦ (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}))
18	1, 17	wceq 1539	1 wff mrCls = (𝑐 ∈ ∪ ran Moore ↦ (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}))

This definition is referenced by:  fnmrc  17325  mrcfval  17326