Definition df-mrc 17213

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 22138) and linear span (mrclsp 20166).

A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcssid 17243), (2) isotone, i.e., 𝑥 ⊆ 𝑦 implies that (𝑁‘𝑥) ⊆ (𝑁‘𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 17242), and (3) idempotent, i.e., (𝑁‘(𝑁‘𝑥)) = (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcidm 17245.) 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 17209	. 2 class mrCls
2		vc	. . 3 setvar 𝑐
3		cmre 17208	. . . . 5 class Moore
4	3	crn 5581	. . . 4 class ran Moore
5	4	cuni 4836	. . 3 class ∪ ran Moore
6		vx	. . . 4 setvar 𝑥
7	2	cv 1538	. . . . . 6 class 𝑐
8	7	cuni 4836	. . . . 5 class ∪ 𝑐
9	8	cpw 4530	. . . 4 class 𝒫 ∪ 𝑐
10	6	cv 1538	. . . . . . 7 class 𝑥
11		vs	. . . . . . . 8 setvar 𝑠
12	11	cv 1538	. . . . . . 7 class 𝑠
13	10, 12	wss 3883	. . . . . 6 wff 𝑥 ⊆ 𝑠
14	13, 11, 7	crab 3067	. . . . 5 class {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}
15	14	cint 4876	. . . 4 class ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}
16	6, 9, 15	cmpt 5153	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠})
17	2, 5, 16	cmpt 5153	. 2 class (𝑐 ∈ ∪ ran Moore ↦ (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}))
18	1, 17	wceq 1539	1 wff mrCls = (𝑐 ∈ ∪ ran Moore ↦ (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}))

This definition is referenced by:  fnmrc  17233  mrcfval  17234