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

Definition df-mrc 14517
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 18663) and linear span (mrclsp 17050).

A Moore closure operation is (1) extensive, i.e., for all subsets of the base set (mrcssid 14547), (2) isotone, i.e., implies that for all subsets and of the base set (mrcss 14546), and (3) idempotent, i.e., for all subsets of the base set (mrcidm 14549.) 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
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-mrc
StepHypRef Expression
1 cmrc 14513 . 2
2 vc . . 3
3 cmre 14512 . . . . 5
43crn 4836 . . . 4
54cuni 4086 . . 3
6 vx . . . 4
72cv 1368 . . . . . 6
87cuni 4086 . . . . 5
98cpw 3855 . . . 4
106cv 1368 . . . . . . 7
11 vs . . . . . . . 8
1211cv 1368 . . . . . . 7
1310, 12wss 3323 . . . . . 6
1413, 11, 7crab 2714 . . . . 5
1514cint 4123 . . . 4
166, 9, 15cmpt 4345 . . 3
172, 5, 16cmpt 4345 . 2
181, 17wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  fnmrc  14537  mrcfval  14538
  Copyright terms: Public domain W3C validator