Home | Metamath
Proof Explorer Theorem List (p. 164 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mrissmrid 16301 | In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
Theorem | mreexd 16302* | In a Moore system, the closure operator is said to have the exchange property if, for all elements and of the base set and subsets of the base set such that is in the closure of but not in the closure of , is in the closure of (Definition 3.1.9 in [FaureFrolicher] p. 57 to 58.) This theorem allows us to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017.) |
Theorem | mreexmrid 16303* | In a Moore system whose closure operator has the exchange property, if a set is independent and an element is not in its closure, then adding the element to the set gives another independent set. Lemma 4.1.5 in [FaureFrolicher] p. 84. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
Theorem | mreexexlemd 16304* | This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 16308. (Contributed by David Moews, 1-May-2017.) |
Theorem | mreexexlem2d 16305* | Used in mreexexlem4d 16307 to prove the induction step in mreexexd 16308. See the proof of Proposition 4.2.1 in [FaureFrolicher] p. 86 to 87. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
Theorem | mreexexlem3d 16306* | Base case of the induction in mreexexd 16308. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
Theorem | mreexexlem4d 16307* | Induction step of the induction in mreexexd 16308. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
Theorem | mreexexd 16308* | Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if and are disjoint from , is independent, is contained in the closure of , and either or is finite, then there is a subset of equinumerous to such that is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either or is finite. The theorem is proven by induction using mreexexlem3d 16306 for the base case and mreexexlem4d 16307 for the induction step. (Contributed by David Moews, 1-May-2017.) Removed dependencies on ax-rep 4771 and ax-ac2 9285. (Revised by Brendan Leahy, 2-Jun-2021.) |
Moore mrCls mrInd | ||
Theorem | mreexexdOLD 16309* | Obsolete proof of mreexexd 16308 as of 2-Jun-2021. Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if and are disjoint from , is independent, is contained in the closure of , and either or is finite, then there is a subset of equinumerous to such that is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either or is finite. The theorem is proven by induction using mreexexlem3d 16306 for the base case and mreexexlem4d 16307 for the induction step. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Moore mrCls mrInd | ||
Theorem | mreexdomd 16310* | In a Moore system whose closure operator has the exchange property, if is independent and contained in the closure of , and either or is finite, then dominates . This is an immediate consequence of mreexexd 16308. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
Theorem | mreexfidimd 16311* | In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd 16310 twice. This implies a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
Theorem | isacs 16312* | A set is an algebraic closure system iff it is specified by some function of the finite subsets, such that a set is closed iff it does not expand under the operation. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
ACS Moore | ||
Theorem | acsmre 16313 | Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
ACS Moore | ||
Theorem | isacs2 16314* | In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
mrCls ACS Moore | ||
Theorem | acsfiel 16315* | A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
mrCls ACS | ||
Theorem | acsfiel2 16316* | A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
mrCls ACS | ||
Theorem | acsmred 16317 | An algebraic closure system is also a Moore system. Deduction form of acsmre 16313. (Contributed by David Moews, 1-May-2017.) |
ACS Moore | ||
Theorem | isacs1i 16318* | A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
ACS | ||
Theorem | mreacs 16319 | Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
ACS Moore | ||
Theorem | acsfn 16320* | Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
ACS | ||
Theorem | acsfn0 16321* | Algebraicity of a point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
ACS | ||
Theorem | acsfn1 16322* | Algebraicity of a one-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
ACS | ||
Theorem | acsfn1c 16323* | Algebraicity of a one-argument closure condition with additional constant. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
ACS | ||
Theorem | acsfn2 16324* | Algebraicity of a two-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
ACS | ||
Syntax | ccat 16325 | Extend class notation with the class of categories. |
Syntax | ccid 16326 | Extend class notation with the identity arrow of a category. |
Syntax | chomf 16327 | Extend class notation to include functionalized Hom-set extractor. |
f | ||
Syntax | ccomf 16328 | Extend class notation to include functionalized composition operation. |
compf | ||
Definition | df-cat 16329* | A category is an abstraction of a structure (a group, a topology, an order...) Category theory consists in finding new formulation of the concepts associated with those structures (product, substructure...) using morphisms instead of the belonging relation. That trick has the interesting property that heterogeneous structures like topologies or groups for instance become comparable. Definition in [Lang] p. 53. In contrast to definition 3.1 of [Adamek] p. 21, where "A category is a quadruple A = (O, hom, id, o)", a category is defined as an extensible structure consisting of three slots: the objects "O" (), the morphisms "hom" ( ) and the composition law "o" (comp). The identities "id" are defined by their properties related to morphisms and their composition, see condition 3.1(b) in [Adamek] p. 21 and df-cid 16330. (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Definition | df-cid 16330* | Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017.) |
comp | ||
Definition | df-homf 16331* | Define the functionalized Hom-set operator, which is exactly like but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017.) |
f | ||
Definition | df-comf 16332* | Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017.) |
compf comp | ||
Theorem | iscat 16333* | The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Theorem | iscatd 16334* | Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Theorem | catidex 16335* | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Theorem | catideu 16336* | Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Theorem | cidfval 16337* | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 3-Jan-2017.) |
comp | ||
Theorem | cidval 16338* | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Theorem | cidffn 16339 | The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017.) |
Theorem | cidfn 16340 | The identity arrow operator is a function from objects to arrows. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | catidd 16341* | Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
comp | ||
Theorem | iscatd2 16342* | Version of iscatd 16334 with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017.) |
comp | ||
Theorem | catidcl 16343 | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | catlid 16344 | Left identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Theorem | catrid 16345 | Right identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Theorem | catcocl 16346 | Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Theorem | catass 16347 | Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp | ||
Theorem | 0catg 16348 | Any structure with an empty set of objects is a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | 0cat 16349 | The empty set is a category, the empty category, see example 3.3(4.c) in [Adamek] p. 24. (Contributed by Mario Carneiro, 3-Jan-2017.) |
Theorem | homffval 16350* | Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
f | ||
Theorem | fnhomeqhomf 16351 | If the Hom-set operation is a function it is equal to the corresponding functionalized Hom-set operation. (Contributed by AV, 1-Mar-2020.) |
f | ||
Theorem | homfval 16352 | Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
f | ||
Theorem | homffn 16353 | The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
f | ||
Theorem | homfeq 16354* | Condition for two categories with the same base to have the same hom-sets. (Contributed by Mario Carneiro, 6-Jan-2017.) |
f f | ||
Theorem | homfeqd 16355 | If two structures have the same slot, they have the same Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.) |
f f | ||
Theorem | homfeqbas 16356 | Deduce equality of base sets from equality of Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.) |
f f | ||
Theorem | homfeqval 16357 | Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
f f | ||
Theorem | comfffval 16358* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
compf comp | ||
Theorem | comffval 16359* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
compf comp | ||
Theorem | comfval 16360 | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
compf comp | ||
Theorem | comfffval2 16361* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
compf f comp | ||
Theorem | comffval2 16362* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
compf f comp | ||
Theorem | comfval2 16363 | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
compf f comp | ||
Theorem | comfffn 16364 | The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
compf | ||
Theorem | comffn 16365 | The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
compf | ||
Theorem | comfeq 16366* | Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
comp comp f f compf compf | ||
Theorem | comfeqd 16367 | Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
comp comp f f compf compf | ||
Theorem | comfeqval 16368 | Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017.) |
comp comp f f compf compf | ||
Theorem | catpropd 16369 | Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017.) |
f f compf compf | ||
Theorem | cidpropd 16370 | Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017.) |
f f compf compf | ||
Syntax | coppc 16371 | The opposite category operation. |
oppCat | ||
Definition | df-oppc 16372* | Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. Definition 3.5 of [Adamek] p. 25. (Contributed by Mario Carneiro, 2-Jan-2017.) |
oppCat sSet tpos sSet comp tpos comp | ||
Theorem | oppcval 16373* | Value of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp oppCat sSet tpos sSet comp tpos | ||
Theorem | oppchomfval 16374 | Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
oppCat tpos | ||
Theorem | oppchom 16375 | Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
oppCat | ||
Theorem | oppccofval 16376 | Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp oppCat comp tpos | ||
Theorem | oppcco 16377 | Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp oppCat comp | ||
Theorem | oppcbas 16378 | Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
oppCat | ||
Theorem | oppccatid 16379 | Lemma for oppccat 16382. (Contributed by Mario Carneiro, 3-Jan-2017.) |
oppCat | ||
Theorem | oppchomf 16380 | Hom-sets of the opposite category. (Contributed by Mario Carneiro, 17-Jan-2017.) |
oppCat f tpos f | ||
Theorem | oppcid 16381 | Identity function of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
oppCat | ||
Theorem | oppccat 16382 | An opposite category is a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
oppCat | ||
Theorem | 2oppcbas 16383 | The double opposite category has the same objects as the original category. Intended for use with property lemmas such as monpropd 16397. (Contributed by Mario Carneiro, 3-Jan-2017.) |
oppCat oppCat | ||
Theorem | 2oppchomf 16384 | The double opposite category has the same morphisms as the original category. Intended for use with property lemmas such as monpropd 16397. (Contributed by Mario Carneiro, 3-Jan-2017.) |
oppCat f f oppCat | ||
Theorem | 2oppccomf 16385 | The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd 16397. (Contributed by Mario Carneiro, 3-Jan-2017.) |
oppCat compf compfoppCat | ||
Theorem | oppchomfpropd 16386 | If two categories have the same hom-sets, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.) |
f f f oppCat f oppCat | ||
Theorem | oppccomfpropd 16387 | If two categories have the same hom-sets and composition, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.) |
f f compf compf compfoppCat compfoppCat | ||
Syntax | cmon 16388 | Extend class notation with the class of all monomorphisms. |
Mono | ||
Syntax | cepi 16389 | Extend class notation with the class of all epimorphisms. |
Epi | ||
Definition | df-mon 16390* | Function returning the monomorphisms of the category . JFM CAT1 def. 10. (Contributed by FL, 5-Dec-2007.) (Revised by Mario Carneiro, 2-Jan-2017.) |
Mono comp | ||
Definition | df-epi 16391 | Function returning the epimorphisms of the category . JFM CAT1 def. 11. (Contributed by FL, 8-Aug-2008.) (Revised by Mario Carneiro, 2-Jan-2017.) |
Epi tpos MonooppCat | ||
Theorem | monfval 16392* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
comp Mono | ||
Theorem | ismon 16393* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp Mono | ||
Theorem | ismon2 16394* | Write out the monomorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp Mono | ||
Theorem | monhom 16395 | A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp Mono | ||
Theorem | moni 16396 | Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp Mono | ||
Theorem | monpropd 16397 | If two categories have the same set of objects, morphisms, and compositions, then they have the same monomorphisms. (Contributed by Mario Carneiro, 3-Jan-2017.) |
f f compf compf Mono Mono | ||
Theorem | oppcmon 16398 | A monomorphism in the opposite category is an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
oppCat Mono Epi | ||
Theorem | oppcepi 16399 | An epimorphism in the opposite category is a monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
oppCat Epi Mono | ||
Theorem | isepi 16400* | Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
comp Epi |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |