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	|- mrCls = ( c e. U. ran Moore |-> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmrc	|- mrCls
1		vc	|- c
2		cmre	|- Moore
3	2	crn	|- ran Moore
4	3	cuni	|- U. ran Moore
5		vx	|- x
6	1	cv	|- c
7	6	cuni	|- U. c
8	7	cpw	|- ~P U. c
9		vs	|- s
10	5	cv	|- x
11	9	cv	|- s
12	10 11	wss	|- x C_ s
13	12 9 6	crab	|- { s e. c | x C_ s }
14	13	cint	|- |^| { s e. c | x C_ s }
15	5 8 14	cmpt	|- ( x e. ~P U. c |-> |^| { s e. c | x C_ s } )
16	1 4 15	cmpt	|- ( c e. U. ran Moore |-> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) )
17	0 16	wceq	|- mrCls = ( c e. U. ran Moore |-> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) )