Definition df-mre 16246

Description: Define a Moore collection, which is a family of subsets of a base set which preserve arbitrary intersection. Elements of a Moore collection are termed closed; Moore collections generalize the notion of closedness from topologies (cldmre 20882) and vector spaces (lssmre 18966) 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 a closure system (Section 0.6 in [Gratzer] p. 23.) The name Moore collection is after Eliakim Hastings Moore, who discussed these systems in Part I of [Moore] p. 53 to 76.

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

Assertion

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

Distinct variable group:   s, c, x

Detailed syntax breakdown of Definition df-mre

Step	Hyp	Ref	Expression
1		cmre 16242	. 2 class Moore
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vc	. . . . . 6 setvar c
5	2, 4	wel 1991	. . . . 5 wff x e. c
6		vs	. . . . . . . . 9 setvar s
7	6	cv 1482	. . . . . . . 8 class s
8		c0 3915	. . . . . . . 8 class (/)
9	7, 8	wne 2794	. . . . . . 7 wff s =/= (/)
10	7	cint 4475	. . . . . . . 8 class |^| s
11	4	cv 1482	. . . . . . . 8 class c
12	10, 11	wcel 1990	. . . . . . 7 wff |^| s e. c
13	9, 12	wi 4	. . . . . 6 wff ( s =/= (/) -> |^| s e. c )
14	11	cpw 4158	. . . . . 6 class ~P c
15	13, 6, 14	wral 2912	. . . . 5 wff A. s e. ~P c ( s =/= (/) -> |^| s e. c )
16	5, 15	wa 384	. . . 4 wff ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) )
17	2	cv 1482	. . . . . 6 class x
18	17	cpw 4158	. . . . 5 class ~P x
19	18	cpw 4158	. . . 4 class ~P ~P x
20	16, 4, 19	crab 2916	. . 3 class { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) }
21	2, 3, 20	cmpt 4729	. 2 class ( x e. _V |-> { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )
22	1, 21	wceq 1483	1 wff Moore = ( x e. _V |-> { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )

This definition is referenced by:  ismre  16250  fnmre  16251