P. 163 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16201-16300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imasleval 16201*	The value of the image structure's ordering when the order is compatible with the mapping function. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- .<_ = ( le ` U )   &    |- N = ( le ` R )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( c e. V /\ d e. V ) ) -> ( ( ( F ` a ) = ( F ` c ) /\ ( F ` b ) = ( F ` d ) ) -> ( a N b <-> c N d ) ) )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .<_ ( F ` Y ) <-> X N Y ) )
Theorem	qusval 16202*	Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> U = ( F "s R ) )
Theorem	quslem 16203*	The function in qusval 16202 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> F : V -onto-> ( V /. .~ ) )
Theorem	qusin 16204	Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( .~ " V ) C_ V )   =>    |- ( ph -> U = ( R /.s ( .~ i^i ( V X. V ) ) ) )
Theorem	qusbas 16205	Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> ( V /. .~ ) = ( Base ` U ) )
Theorem	quss 16206	The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   &    |- K = (Scalar ` R )   =>    |- ( ph -> K = (Scalar ` U ) )
Theorem	divsfval 16207*	Value of the function in qusval 16202. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. _V )   &    |- F = ( x e. V |-> [ x ] .~ )   =>    |- ( ph -> ( F ` A ) = [ A ] .~ )
Theorem	ercpbllem 16208*	Lemma for ercpbl 16209. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. _V )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( ( F ` A ) = ( F ` B ) <-> A .~ B ) )
Theorem	ercpbl 16209*	Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. _V )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a .+ b ) e. V )   &    |- ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) ) )
Theorem	erlecpbl 16210*	Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. _V )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A N B <-> C N D ) ) )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( A N B <-> C N D ) ) )
Theorem	qusaddvallem 16211*	Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	qusaddflem 16212*	The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   =>    |- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )
Theorem	qusaddval 16213*	The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	qusaddf 16214*	The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )
Theorem	qusmulval 16215*	The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	qusmulf 16216*	The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )
Theorem	xpsc 16217	A short expression for the pair function mapping 0 to A and 1 to B. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- `' ( { A } +c { B } ) = ( ( { (/) } X. { A } ) u. ( { 1o } X. { B } ) )
Theorem	xpscg 16218	A short expression for the pair function mapping 0 to A and 1 to B. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( ( A e. V /\ B e. W ) -> `' ( { A } +c { B } ) = { <. (/) , A >. , <. 1o , B >. } )
Theorem	xpscfn 16219	The pair function is a function on 2o = { (/) , 1o }. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( ( A e. V /\ B e. W ) -> `' ( { A } +c { B } ) Fn 2o )
Theorem	xpsc0 16220	The pair function maps 0 to A. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( A e. V -> ( `' ( { A } +c { B } ) ` (/) ) = A )
Theorem	xpsc1 16221	The pair function maps 1 to B. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( B e. V -> ( `' ( { A } +c { B } ) ` 1o ) = B )
Theorem	xpscfv 16222	The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( ( A e. V /\ B e. W /\ C e. 2o ) -> ( `' ( { A } +c { B } ) ` C ) = if ( C = (/) , A , B ) )
Theorem	xpsfrnel 16223*	Elementhood in the target space of the function F appearing in xpsval 16232. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( G e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( G Fn 2o /\ ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) )
Theorem	xpsfeq 16224	A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- ( G Fn 2o -> `' ( { ( G ` (/) ) } +c { ( G ` 1o ) } ) = G )
Theorem	xpsfrnel2 16225*	Elementhood in the target space of the function F appearing in xpsval 16232. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- ( `' ( { X } +c { Y } ) e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( X e. A /\ Y e. B ) )
Theorem	xpscf 16226	Equivalent condition for the pair function to be a proper function on A. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( `' ( { X } +c { Y } ) : 2o --> A <-> ( X e. A /\ Y e. A ) )
Theorem	xpsfval 16227*	The value of the function appearing in xpsval 16232. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> `' ( { x } +c { y } ) )   =>    |- ( ( X e. A /\ Y e. B ) -> ( X F Y ) = `' ( { X } +c { Y } ) )
Theorem	xpsff1o 16228*	The function appearing in xpsval 16232 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o }. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> `' ( { x } +c { y } ) )   =>    |- F : ( A X. B ) -1-1-onto-> X_ k e. 2o if ( k = (/) , A , B )
Theorem	xpsfrn 16229*	A short expression for the indexed cartesian product on two indexes. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> `' ( { x } +c { y } ) )   =>    |- ran F = X_ k e. 2o if ( k = (/) , A , B )
Theorem	xpsfrn2 16230*	A short expression for the indexed cartesian product on two indexes. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> `' ( { x } +c { y } ) )   =>    |- ( ( A e. V /\ B e. W ) -> ran F = X_ k e. 2o ( `' ( { A } +c { B } ) ` k ) )
Theorem	xpsff1o2 16231*	The function appearing in xpsval 16232 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o }. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- F = ( x e. A , y e. B |-> `' ( { x } +c { y } ) )   =>    |- F : ( A X. B ) -1-1-onto-> ran F
Theorem	xpsval 16232*	Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- F = ( x e. X , y e. Y |-> `' ( { x } +c { y } ) )   &    |- G = (Scalar ` R )   &    |- U = ( G X_s `' ( { R } +c { S } ) )   =>    |- ( ph -> T = ( `' F "s U ) )
Theorem	xpslem 16233*	The indexed structure product that appears in xpsval 16232 has the same base as the target of the function F. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- F = ( x e. X , y e. Y |-> `' ( { x } +c { y } ) )   &    |- G = (Scalar ` R )   &    |- U = ( G X_s `' ( { R } +c { S } ) )   =>    |- ( ph -> ran F = ( Base ` U ) )
Theorem	xpsbas 16234	The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   =>    |- ( ph -> ( X X. Y ) = ( Base ` T ) )
Theorem	xpsaddlem 16235*	Lemma for xpsadd 16236 and xpsmul 16237. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> ( A .x. C ) e. X )   &    |- ( ph -> ( B .X. D ) e. Y )   &    |- .x. = ( E ` R )   &    |- .X. = ( E ` S )   &    |- .xb = ( E ` T )   &    |- F = ( x e. X , y e. Y |-> `' ( { x } +c { y } ) )   &    |- U = ( (Scalar ` R ) X_s `' ( { R } +c { S } ) )   &    |- ( ( ph /\ `' ( { A } +c { B } ) e. ran F /\ `' ( { C } +c { D } ) e. ran F ) -> ( ( `' F ` `' ( { A } +c { B } ) ) .xb ( `' F ` `' ( { C } +c { D } ) ) ) = ( `' F ` ( `' ( { A } +c { B } ) ( E ` U ) `' ( { C } +c { D } ) ) ) )   &    |- ( ( `' ( { R } +c { S } ) Fn 2o /\ `' ( { A } +c { B } ) e. ( Base ` U ) /\ `' ( { C } +c { D } ) e. ( Base ` U ) ) -> ( `' ( { A } +c { B } ) ( E ` U ) `' ( { C } +c { D } ) ) = ( k e. 2o |-> ( ( `' ( { A } +c { B } ) ` k ) ( E ` ( `' ( { R } +c { S } ) ` k ) ) ( `' ( { C } +c { D } ) ` k ) ) ) )   =>    |- ( ph -> ( <. A , B >. .xb <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. )
Theorem	xpsadd 16236	Value of the addition operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> ( A .x. C ) e. X )   &    |- ( ph -> ( B .X. D ) e. Y )   &    |- .x. = ( +g ` R )   &    |- .X. = ( +g ` S )   &    |- .xb = ( +g ` T )   =>    |- ( ph -> ( <. A , B >. .xb <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. )
Theorem	xpsmul 16237	Value of the multiplication operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> ( A .x. C ) e. X )   &    |- ( ph -> ( B .X. D ) e. Y )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   &    |- .xb = ( .r ` T )   =>    |- ( ph -> ( <. A , B >. .xb <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. )
Theorem	xpssca 16238	Value of the scalar field of a binary structure product. For concreteness, we choose the scalar field to match the left argument, but in most cases where this slot is meaningful both factors will have the same scalar field, so that it doesn't matter which factor is chosen. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- T = ( R X.s S )   &    |- G = (Scalar ` R )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   =>    |- ( ph -> G = (Scalar ` T ) )
Theorem	xpsvsca 16239	Value of the scalar multiplication function in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- T = ( R X.s S )   &    |- G = (Scalar ` R )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- K = ( Base ` G )   &    |- .x. = ( .s ` R )   &    |- .X. = ( .s ` S )   &    |- .xb = ( .s ` T )   &    |- ( ph -> A e. K )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. Y )   &    |- ( ph -> ( A .x. B ) e. X )   &    |- ( ph -> ( A .X. C ) e. Y )   =>    |- ( ph -> ( A .xb <. B , C >. ) = <. ( A .x. B ) , ( A .X. C ) >. )
Theorem	xpsless 16240	Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- .<_ = ( le ` T )   =>    |- ( ph -> .<_ C_ ( ( X X. Y ) X. ( X X. Y ) ) )
Theorem	xpsle 16241	Value of the ordering in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- .<_ = ( le ` T )   &    |- M = ( le ` R )   &    |- N = ( le ` S )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> ( <. A , B >. .<_ <. C , D >. <-> ( A M C /\ B N D ) ) )
7.2  Moore spaces
Syntax	cmre 16242	The class of Moore systems.
class Moore
Syntax	cmrc 16243	The class function generating Moore closures.
class mrCls
Syntax	cmri 16244	mrInd is a class function which takes a Moore system to its set of independent sets.
class mrInd
Syntax	cacs 16245	The class of algebraic closure (Moore) systems.
class ACS
Definition	df-mre 16246*	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.)
|- Moore = ( x e. _V |-> { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )
Definition	df-mrc 16247*	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.)
|- mrCls = ( c e. U. ran Moore |-> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) )
Definition	df-mri 16248*	In a Moore system, a set is independent if no element of the set is in the closure of the set with the element removed (Section 0.6 in [Gratzer] p. 27; Definition 4.1.1 in [FaureFrolicher] p. 83.) mrInd is a class function which takes a Moore system to its set of independent sets. (Contributed by David Moews, 1-May-2017.)
|- mrInd = ( c e. U. ran Moore |-> { s e. ~P U. c | A. x e. s -. x e. ( (mrCls ` c ) ` ( s \ { x } ) ) } )
Definition	df-acs 16249*	An important subclass of Moore systems are those which can be interpreted as closure under some collection of operators of finite arity (the collection itself is not required to be finite). These are termed algebraic closure systems; similar to definition (A) of an algebraic closure system in [Schechter] p. 84, but to avoid the complexity of an arbitrary mixed collection of functions of various arities (especially if the axiom of infinity omex 8540 is to be avoided), we consider a single function defined on finite sets instead. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ACS = ( x e. _V |-> { c e. (Moore ` x ) | E. f ( f : ~P x --> ~P x /\ A. s e. ~P x ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) } )
Theorem	ismre 16250*	Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( C e. (Moore ` X ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) )
Theorem	fnmre 16251	The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon 20728 for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- Moore Fn _V
Theorem	mresspw 16252	A Moore collection is a subset of the power of the base set; each closed subset of the system is actually a subset of the base. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( C e. (Moore ` X ) -> C C_ ~P X )
Theorem	mress 16253	A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- ( ( C e. (Moore ` X ) /\ S e. C ) -> S C_ X )
Theorem	mre1cl 16254	In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( C e. (Moore ` X ) -> X e. C )
Theorem	mreintcl 16255	A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( ( C e. (Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> |^| S e. C )
Theorem	mreiincl 16256*	A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ( C e. (Moore ` X ) /\ I =/= (/) /\ A. y e. I S e. C ) -> |^|_ y e. I S e. C )
Theorem	mrerintcl 16257	The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ( C e. (Moore ` X ) /\ S C_ C ) -> ( X i^i |^| S ) e. C )
Theorem	mreriincl 16258*	The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ( C e. (Moore ` X ) /\ A. y e. I S e. C ) -> ( X i^i |^|_ y e. I S ) e. C )
Theorem	mreincl 16259	Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( ( C e. (Moore ` X ) /\ A e. C /\ B e. C ) -> ( A i^i B ) e. C )
Theorem	mreuni 16260	Since the entire base set of a Moore collection is the greatest element of it, the base set can be recovered from a Moore collection by set union. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( C e. (Moore ` X ) -> U. C = X )
Theorem	mreunirn 16261	Two ways to express the notion of being a Moore collection on an unspecified base. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( C e. U. ran Moore <-> C e. (Moore ` U. C ) )
Theorem	ismred 16262*	Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( ph -> C C_ ~P X )   &    |- ( ph -> X e. C )   &    |- ( ( ph /\ s C_ C /\ s =/= (/) ) -> |^| s e. C )   =>    |- ( ph -> C e. (Moore ` X ) )
Theorem	ismred2 16263*	Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ph -> C C_ ~P X )   &    |- ( ( ph /\ s C_ C ) -> ( X i^i |^| s ) e. C )   =>    |- ( ph -> C e. (Moore ` X ) )
Theorem	mremre 16264	The Moore collections of subsets of a space, viewed as a kind of subset of the power set, form a Moore collection in their own right on the power set. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( X e. V -> (Moore ` X ) e. (Moore ` ~P X ) )
Theorem	submre 16265	The subcollection of a closed set system below a given closed set is itself a closed set system. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- ( ( C e. (Moore ` X ) /\ A e. C ) -> ( C i^i ~P A ) e. (Moore ` A ) )
7.2.1  Moore closures
Theorem	mrcflem 16266*	The domain and range of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- ( C e. (Moore ` X ) -> ( x e. ~P X |-> |^| { s e. C | x C_ s } ) : ~P X --> C )
Theorem	fnmrc 16267	Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- mrCls Fn U. ran Moore
Theorem	mrcfval 16268*	Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (Moore ` X ) -> F = ( x e. ~P X |-> |^| { s e. C | x C_ s } ) )
Theorem	mrcf 16269	The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (Moore ` X ) -> F : ~P X --> C )
Theorem	mrcval 16270*	Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Fan Zheng, 6-Jun-2016.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ X ) -> ( F ` U ) = |^| { s e. C | U C_ s } )
Theorem	mrccl 16271	The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ X ) -> ( F ` U ) e. C )
Theorem	mrcsncl 16272	The Moore closure of a singleton is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U e. X ) -> ( F ` { U } ) e. C )
Theorem	mrcid 16273	The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U e. C ) -> ( F ` U ) = U )
Theorem	mrcssv 16274	The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (Moore ` X ) -> ( F ` U ) C_ X )
Theorem	mrcidb 16275	A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (Moore ` X ) -> ( U e. C <-> ( F ` U ) = U ) )
Theorem	mrcss 16276	Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ V /\ V C_ X ) -> ( F ` U ) C_ ( F ` V ) )
Theorem	mrcssid 16277	The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ X ) -> U C_ ( F ` U ) )
Theorem	mrcidb2 16278	A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ X ) -> ( U e. C <-> ( F ` U ) C_ U ) )
Theorem	mrcidm 16279	The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ X ) -> ( F ` ( F ` U ) ) = ( F ` U ) )
Theorem	mrcsscl 16280	The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ V /\ V e. C ) -> ( F ` U ) C_ V )
Theorem	mrcuni 16281	Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ ~P X ) -> ( F ` U. U ) = ( F ` U. ( F " U ) ) )
Theorem	mrcun 16282	Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ X /\ V C_ X ) -> ( F ` ( U u. V ) ) = ( F ` ( ( F ` U ) u. ( F ` V ) ) ) )
Theorem	mrcssvd 16283	The Moore closure of a set is a subset of the base. Deduction form of mrcssv 16274. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   =>    |- ( ph -> ( N ` B ) C_ X )
Theorem	mrcssd 16284	Moore closure preserves subset ordering. Deduction form of mrcss 16276. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- ( ph -> U C_ V )   &    |- ( ph -> V C_ X )   =>    |- ( ph -> ( N ` U ) C_ ( N ` V ) )
Theorem	mrcssidd 16285	A set is contained in its Moore closure. Deduction form of mrcssid 16277. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- ( ph -> U C_ X )   =>    |- ( ph -> U C_ ( N ` U ) )
Theorem	mrcidmd 16286	Moore closure is idempotent. Deduction form of mrcidm 16279. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- ( ph -> U C_ X )   =>    |- ( ph -> ( N ` ( N ` U ) ) = ( N ` U ) )
Theorem	mressmrcd 16287	In a Moore system, if a set is between another set and its closure, the two sets have the same closure. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- ( ph -> S C_ ( N ` T ) )   &    |- ( ph -> T C_ S )   =>    |- ( ph -> ( N ` S ) = ( N ` T ) )
Theorem	submrc 16288	In a closure system which is cut off above some level, closures below that level act as normal. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- F = (mrCls ` C )   &    |- G = (mrCls ` ( C i^i ~P D ) )   =>    |- ( ( C e. (Moore ` X ) /\ D e. C /\ U C_ D ) -> ( G ` U ) = ( F ` U ) )
Theorem	mrieqvlemd 16289	In a Moore system, if Y is a member of S, ( S \ { Y } ) and S have the same closure if and only if Y is in the closure of ( S \ { Y } ). Used in the proof of mrieqvd 16298 and mrieqv2d 16299. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- ( ph -> S C_ X )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> ( Y e. ( N ` ( S \ { Y } ) ) <-> ( N ` ( S \ { Y } ) ) = ( N ` S ) ) )
7.2.2  Independent sets in a Moore system
Theorem	mrisval 16290*	Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.)
|- N = (mrCls ` A )   &    |- I = (mrInd ` A )   =>    |- ( A e. (Moore ` X ) -> I = { s e. ~P X | A. x e. s -. x e. ( N ` ( s \ { x } ) ) } )
Theorem	ismri 16291*	Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017.)
|- N = (mrCls ` A )   &    |- I = (mrInd ` A )   =>    |- ( A e. (Moore ` X ) -> ( S e. I <-> ( S C_ X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) ) )
Theorem	ismri2 16292*	Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017.)
|- N = (mrCls ` A )   &    |- I = (mrInd ` A )   =>    |- ( ( A e. (Moore ` X ) /\ S C_ X ) -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )
Theorem	ismri2d 16293*	Criterion for a subset of the base set in a Moore system to be independent. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A e. (Moore ` X ) )   &    |- ( ph -> S C_ X )   =>    |- ( ph -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )
Theorem	ismri2dd 16294*	Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017.)
|- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A e. (Moore ` X ) )   &    |- ( ph -> S C_ X )   &    |- ( ph -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) )   =>    |- ( ph -> S e. I )
Theorem	mriss 16295	An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017.)
|- I = (mrInd ` A )   =>    |- ( ( A e. (Moore ` X ) /\ S e. I ) -> S C_ X )
Theorem	mrissd 16296	An independent set of a Moore system is a subset of the base set. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- I = (mrInd ` A )   &    |- ( ph -> A e. (Moore ` X ) )   &    |- ( ph -> S e. I )   =>    |- ( ph -> S C_ X )
Theorem	ismri2dad 16297	Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A e. (Moore ` X ) )   &    |- ( ph -> S e. I )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> -. Y e. ( N ` ( S \ { Y } ) ) )
Theorem	mrieqvd 16298*	In a Moore system, a set is independent if and only if, for all elements of the set, the closure of the set with the element removed is unequal to the closure of the original set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> S C_ X )   =>    |- ( ph -> ( S e. I <-> A. x e. S ( N ` ( S \ { x } ) ) =/= ( N ` S ) ) )
Theorem	mrieqv2d 16299*	In a Moore system, a set is independent if and only if all its proper subsets have closure properly contained in the closure of the set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> S C_ X )   =>    |- ( ph -> ( S e. I <-> A. s ( s C. S -> ( N ` s ) C. ( N ` S ) ) ) )
Theorem	mrissmrcd 16300	In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd 16287, and so are equal by mrieqv2d 16299.) (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> S C_ ( N ` T ) )   &    |- ( ph -> T C_ S )   &    |- ( ph -> S e. I )   =>    |- ( ph -> S = T )