Definition df-mre

Description: Define aMoore collection, which is a family of subsets of a base set which preserve arbitrary intersection. Elements of a Moore collection are termedclosed; Moore collections generalize the notion of closedness from topologies ( cldmre ) and vector spaces ( lssmre ) to the most general setting in which such concepts make sense. Definition of Moore collection of sets in Schechter p. 78. A Moore collection may also be called aclosure system (Section 0.6 in Gratzer p. 23.) The nameMoore collection is after Eliakim Hastings Moore, who discussed these systems in Part I of Moore p. 53 to 76.

See ismre , mresspw , mre1cl and mreintcl for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set ( mreuni ); as such the disjoint union of all Moore collections is sometimes considered as U. ran Moore , justified by mreunirn . (Contributed by Stefan O'Rear, 30-Jan-2015) (Revised by David Moews, 1-May-2017)

	Ref	Expression
Assertion	df-mre	|- Moore = ( x e. _V |-> { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmre	|- Moore
1		vx	|- x
2		cvv	|- _V
3		vc	|- c
4	1	cv	|- x
5	4	cpw	|- ~P x
6	5	cpw	|- ~P ~P x
7	3	cv	|- c
8	4 7	wcel	|- x e. c
9		vs	|- s
10	7	cpw	|- ~P c
11	9	cv	|- s
12		c0	|- (/)
13	11 12	wne	|- s =/= (/)
14	11	cint	|- |^| s
15	14 7	wcel	|- |^| s e. c
16	13 15	wi	|- ( s =/= (/) -> |^| s e. c )
17	16 9 10	wral	|- A. s e. ~P c ( s =/= (/) -> |^| s e. c )
18	8 17	wa	|- ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) )
19	18 3 6	crab	|- { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) }
20	1 2 19	cmpt	|- ( x e. _V |-> { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )
21	0 20	wceq	|- Moore = ( x e. _V |-> { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )