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

Definition df-mrc 16929
 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 21792) and linear span (mrclsp 19842). A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcssid 16959), (2) isotone, i.e., 𝑥 ⊆ 𝑦 implies that (𝑁‘𝑥) ⊆ (𝑁‘𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 16958), and (3) idempotent, i.e., (𝑁‘(𝑁‘𝑥)) = (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcidm 16961.) 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 16925 . 2 class mrCls
2 vc . . 3 setvar 𝑐
3 cmre 16924 . . . . 5 class Moore
43crn 5529 . . . 4 class ran Moore
54cuni 4801 . . 3 class ran Moore
6 vx . . . 4 setvar 𝑥
72cv 1537 . . . . . 6 class 𝑐
87cuni 4801 . . . . 5 class 𝑐
98cpw 4497 . . . 4 class 𝒫 𝑐
106cv 1537 . . . . . . 7 class 𝑥
11 vs . . . . . . . 8 setvar 𝑠
1211cv 1537 . . . . . . 7 class 𝑠
1310, 12wss 3860 . . . . . 6 wff 𝑥𝑠
1413, 11, 7crab 3074 . . . . 5 class {𝑠𝑐𝑥𝑠}
1514cint 4841 . . . 4 class {𝑠𝑐𝑥𝑠}
166, 9, 15cmpt 5116 . . 3 class (𝑥 ∈ 𝒫 𝑐 {𝑠𝑐𝑥𝑠})
172, 5, 16cmpt 5116 . 2 class (𝑐 ran Moore ↦ (𝑥 ∈ 𝒫 𝑐 {𝑠𝑐𝑥𝑠}))
181, 17wceq 1538 1 wff mrCls = (𝑐 ran Moore ↦ (𝑥 ∈ 𝒫 𝑐 {𝑠𝑐𝑥𝑠}))
 Colors of variables: wff setvar class This definition is referenced by:  fnmrc  16949  mrcfval  16950
 Copyright terms: Public domain W3C validator