Definition df-mrc 16247

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 20883) and linear span (mrclsp 18989).

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

Assertion

Ref	Expression
df-mrc	|- mrCls = ( c e. U. ran Moore |-> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) )

Distinct variable group:   s, c, x

Detailed syntax breakdown of Definition df-mrc

Step	Hyp	Ref	Expression
1		cmrc 16243	. 2 class mrCls
2		vc	. . 3 setvar c
3		cmre 16242	. . . . 5 class Moore
4	3	crn 5115	. . . 4 class ran Moore
5	4	cuni 4436	. . 3 class U. ran Moore
6		vx	. . . 4 setvar x
7	2	cv 1482	. . . . . 6 class c
8	7	cuni 4436	. . . . 5 class U. c
9	8	cpw 4158	. . . 4 class ~P U. c
10	6	cv 1482	. . . . . . 7 class x
11		vs	. . . . . . . 8 setvar s
12	11	cv 1482	. . . . . . 7 class s
13	10, 12	wss 3574	. . . . . 6 wff x C_ s
14	13, 11, 7	crab 2916	. . . . 5 class { s e. c | x C_ s }
15	14	cint 4475	. . . 4 class |^| { s e. c | x C_ s }
16	6, 9, 15	cmpt 4729	. . 3 class ( x e. ~P U. c |-> |^| { s e. c | x C_ s } )
17	2, 5, 16	cmpt 4729	. 2 class ( c e. U. ran Moore |-> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) )
18	1, 17	wceq 1483	1 wff mrCls = ( c e. U. ran Moore |-> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) )

This definition is referenced by:  fnmrc  16267  mrcfval  16268