P. 138 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 13701-13800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imasvsca 13701*	The scalar multiplication operation of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- G = (Scalar ` R )   &    |- K = ( Base ` G )   &    |- .x. = ( .s ` R )   &    |- .xb = ( .s ` U )   =>    |- ( ph -> .xb = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
Theorem	imastset 13702	The topology of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- J = ( TopOpen ` R )   &    |- O = (TopSet ` U )   =>    |- ( ph -> O = ( J qTop F ) )
Theorem	imasle 13703	The ordering of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- N = ( le ` R )   &    |- .<_ = ( le ` U )   =>    |- ( ph -> .<_ = ( ( F o. N ) o. `' F ) )
Theorem	f1ocpbllem 13704	Lemma for f1ocpbl 13705. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) <-> ( A = C /\ B = D ) ) )
Theorem	f1ocpbl 13705	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( 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	f1ovscpbl 13706	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( F ` B ) = ( F ` C ) -> ( F ` ( A .+ B ) ) = ( F ` ( A .+ C ) ) ) )
Theorem	f1olecpbl 13707	An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( 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	imasaddfnlem 13708*	The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasaddvallem 13709*	The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( 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 ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasaddflem 13710*	The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	imasaddfn 13711*	The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasaddval 13712*	The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasaddf 13713*	The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	imasmulfn 13714*	The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasmulval 13715*	The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasmulf 13716*	The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	imasvscafn 13717*	The image structure's scalar multiplication is a 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 )   &    |- G = (Scalar ` R )   &    |- K = ( Base ` G )   &    |- .x. = ( .s ` R )   &    |- .xb = ( .s ` U )   &    |- ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )   =>    |- ( ph -> .xb Fn ( K X. B ) )
Theorem	imasvscaval 13718*	The value of an image structure's scalar multiplication. (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 )   &    |- G = (Scalar ` R )   &    |- K = ( Base ` G )   &    |- .x. = ( .s ` R )   &    |- .xb = ( .s ` U )   &    |- ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )   =>    |- ( ( ph /\ X e. K /\ Y e. V ) -> ( X .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasvscaf 13719*	The image structure's scalar multiplication is closed in the base set. (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 )   &    |- G = (Scalar ` R )   &    |- K = ( Base ` G )   &    |- .x. = ( .s ` R )   &    |- .xb = ( .s ` U )   &    |- ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ( ph /\ ( p e. K /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( K X. B ) --> B )
Theorem	imasless 13720	The order relation defined on an image set is a subset of the base set. (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 )   =>    |- ( ph -> .<_ C_ ( B X. B ) )
Theorem	imasleval 13721*	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	divsval 13722*	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	divslem 13723*	The function in divsval 13722 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	divsin 13724	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	divsbas 13725	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	divssca 13726	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 13727*	Value of the function in divsval 13722. (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 13728*	Lemma for ercpbl 13729. (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 13729*	Translate the function compatiblity 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 13730*	Translate the relation compatiblity 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	divsaddvallem 13731*	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	divsaddflem 13732*	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	divsaddval 13733*	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	divsaddf 13734*	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	divsmulval 13735*	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	divsmulf 13736*	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 13737	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 13738	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 13739	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 13740	The pair function maps 0 to A. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( A e. V -> ( `' ( { A } +c { B } ) ` (/) ) = A )
Theorem	xpsc1 13741	The pair function maps 1 to B. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( B e. V -> ( `' ( { A } +c { B } ) ` 1o ) = B )
Theorem	xpscfv 13742	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 13743*	Elementhood in the target space of the function F appearing in xpsval 13752. (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 13744	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 13745*	Elementhood in the target space of the function F appearing in xpsval 13752. (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 13746	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 13747*	The value of the function appearing in xpsval 13752. (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 13748*	The function appearing in xpsval 13752 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 13749*	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 13750*	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 13751*	The function appearing in xpsval 13752 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 13752*	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 13753*	The indexed structure product that appears in xpsval 13752 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 13754	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 13755*	Lemma for xpsadd 13756 and xpsmul 13757. (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 13756	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 13757	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 13758	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 13759	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 13760	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 13761	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 13762	The class of Moore systems.
class Moore
Syntax	cmrc 13763	The class function generating Moore closures.
class mrCls
Syntax	cmri 13764	mrInd is a class function which takes a Moore system to its set of independent sets.
class mrInd
Syntax	cacs 13765	The class of algebraic closure (Moore) systems.
class ACS
Definition	df-mre 13766*	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 17097) and vector spaces (lssmre 15997) 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 13770, mresspw 13772, mre1cl 13774 and mreintcl 13775 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 13780); as such the disjoint union of all Moore collections is sometimes considered as U. ran Moore, justified by mreunirn 13781. (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 13767*	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 17098) and linear span (mrclsp 16020). A Moore closure operation N is (1) extensive, i.e., x C_ ( N ` x ) for all subsets x of the base set (mrcssid 13797), (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 13796), and (3) idempotent, i.e., ( N ` ( N ` x ) ) = ( N ` x ) for all subsets x of the base set (mrcidm 13799.) 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 13768*	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 13769*	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 7554 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 13770*	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 13771	The Moore collection generator is a well-behaved function. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- Moore Fn _V
Theorem	mresspw 13772	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 13773	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 13774	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 13775	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 13776*	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 13777	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 13778*	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 13779	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 13780	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 13781	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 13782*	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 13783*	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 13784	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 13785	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 13786*	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 13787	Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- mrCls Fn U. ran Moore
Theorem	mrcfval 13788*	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 13789	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 13790*	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 13791	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 13792	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 13793	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 13794	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 13795	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 13796	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 13797	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 13798	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 13799	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 13800	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 )