MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mrc Structured version   Visualization version   GIF version

Definition df-mrc 16070
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 20693) and linear span (mrclsp 18810).

A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁𝑥) for all subsets 𝑥 of the base set (mrcssid 16100), (2) isotone, i.e., 𝑥𝑦 implies that (𝑁𝑥) ⊆ (𝑁𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 16099), and (3) idempotent, i.e., (𝑁‘(𝑁𝑥)) = (𝑁𝑥) for all subsets 𝑥 of the base set (mrcidm 16102.) 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
StepHypRef Expression
1 cmrc 16066 . 2 class mrCls
2 vc . . 3 setvar 𝑐
3 cmre 16065 . . . . 5 class Moore
43crn 5039 . . . 4 class ran Moore
54cuni 4372 . . 3 class ran Moore
6 vx . . . 4 setvar 𝑥
72cv 1474 . . . . . 6 class 𝑐
87cuni 4372 . . . . 5 class 𝑐
98cpw 4108 . . . 4 class 𝒫 𝑐
106cv 1474 . . . . . . 7 class 𝑥
11 vs . . . . . . . 8 setvar 𝑠
1211cv 1474 . . . . . . 7 class 𝑠
1310, 12wss 3540 . . . . . 6 wff 𝑥𝑠
1413, 11, 7crab 2900 . . . . 5 class {𝑠𝑐𝑥𝑠}
1514cint 4410 . . . 4 class {𝑠𝑐𝑥𝑠}
166, 9, 15cmpt 4643 . . 3 class (𝑥 ∈ 𝒫 𝑐 {𝑠𝑐𝑥𝑠})
172, 5, 16cmpt 4643 . 2 class (𝑐 ran Moore ↦ (𝑥 ∈ 𝒫 𝑐 {𝑠𝑐𝑥𝑠}))
181, 17wceq 1475 1 wff mrCls = (𝑐 ran Moore ↦ (𝑥 ∈ 𝒫 𝑐 {𝑠𝑐𝑥𝑠}))
Colors of variables: wff setvar class
This definition is referenced by:  fnmrc  16090  mrcfval  16091
  Copyright terms: Public domain W3C validator