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	$$setvarc$$
2		cmre	$$class\mathrm{Moore}$$
3	2	crn	$$class\mathrm{ran}\mathrm{Moore}$$
4	3	cuni	$$class\bigcup \mathrm{ran}\mathrm{Moore}$$
5		vx	$$setvarx$$
6	1	cv	$$setvarc$$
7	6	cuni	$$class\bigcup c$$
8	7	cpw	$$class𝒫\bigcup c$$
9		vs	$$setvars$$
10	5	cv	$$setvarx$$
11	9	cv	$$setvars$$
12	10 11	wss	$$wffx\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)$$