# Metamath Proof Explorer

## Definition df-mrc

Description: Define theMoore 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 ) and linear span ( mrclsp ).

A Moore closure operation N is (1) extensive, i.e., x C_ ( Nx ) for all subsets x of the base set ( mrcssid ), (2) isotone, i.e., x C_ y implies that ( Nx ) C_ ( Ny ) for all subsets x and y of the base set ( mrcss ), and (3) idempotent, i.e., ( N( Nx ) ) = ( Nx ) for all subsets x of the base set ( mrcidm .) 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 N 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)

Ref Expression
Assertion df-mrc ${⊢}\mathrm{mrCls}=\left({c}\in \bigcup \mathrm{ran}\mathrm{Moore}⟼\left({x}\in 𝒫\bigcup {c}⟼\bigcap \left\{{s}\in {c}|{x}\subseteq {s}\right\}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmrc ${class}\mathrm{mrCls}$
1 vc ${setvar}{c}$
2 cmre ${class}\mathrm{Moore}$
3 2 crn ${class}\mathrm{ran}\mathrm{Moore}$
4 3 cuni ${class}\bigcup \mathrm{ran}\mathrm{Moore}$
5 vx ${setvar}{x}$
6 1 cv ${setvar}{c}$
7 6 cuni ${class}\bigcup {c}$
8 7 cpw ${class}𝒫\bigcup {c}$
9 vs ${setvar}{s}$
10 5 cv ${setvar}{x}$
11 9 cv ${setvar}{s}$
12 10 11 wss ${wff}{x}\subseteq {s}$
13 12 9 6 crab ${class}\left\{{s}\in {c}|{x}\subseteq {s}\right\}$
14 13 cint ${class}\bigcap \left\{{s}\in {c}|{x}\subseteq {s}\right\}$
15 5 8 14 cmpt ${class}\left({x}\in 𝒫\bigcup {c}⟼\bigcap \left\{{s}\in {c}|{x}\subseteq {s}\right\}\right)$
16 1 4 15 cmpt ${class}\left({c}\in \bigcup \mathrm{ran}\mathrm{Moore}⟼\left({x}\in 𝒫\bigcup {c}⟼\bigcap \left\{{s}\in {c}|{x}\subseteq {s}\right\}\right)\right)$
17 0 16 wceq ${wff}\mathrm{mrCls}=\left({c}\in \bigcup \mathrm{ran}\mathrm{Moore}⟼\left({x}\in 𝒫\bigcup {c}⟼\bigcap \left\{{s}\in {c}|{x}\subseteq {s}\right\}\right)\right)$