P. 151 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mrcun 15001	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 15002	The Moore closure of a set is a subset of the base. Deduction form of mrcssv 14993. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   =>    |- ( ph -> ( N ` B ) C_ X )
Theorem	mrcssd 15003	Moore closure preserves subset ordering. Deduction form of mrcss 14995. (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 15004	A set is contained in its Moore closure. Deduction form of mrcssid 14996. (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 15005	Moore closure is idempotent. Deduction form of mrcidm 14998. (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 15006	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 15007	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 15008	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 15017 and mrieqv2d 15018. 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 15009*	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 15010*	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 15011*	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 15012*	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 15013*	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 15014	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 15015	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 15016	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 15017*	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 15018*	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 15019	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 15006, and so are equal by mrieqv2d 15018.) (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 )
Theorem	mrissmrid 15020	In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> S e. I )   &    |- ( ph -> T C_ S )   =>    |- ( ph -> T e. I )
Theorem	mreexd 15021*	In a Moore system, the closure operator is said to have the exchange property if, for all elements y and z of the base set and subsets S of the base set such that z is in the closure of ( S u. { y } ) but not in the closure of S, y is in the closure of ( S u. { z } ) (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.)
|- ( ph -> X e. V )   &    |- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )   &    |- ( ph -> S C_ X )   &    |- ( ph -> Y e. X )   &    |- ( ph -> Z e. ( N ` ( S u. { Y } ) ) )   &    |- ( ph -> -. Z e. ( N ` S ) )   =>    |- ( ph -> Y e. ( N ` ( S u. { Z } ) ) )
Theorem	mreexmrid 15022*	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.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )   &    |- ( ph -> S e. I )   &    |- ( ph -> Y e. X )   &    |- ( ph -> -. Y e. ( N ` S ) )   =>    |- ( ph -> ( S u. { Y } ) e. I )
Theorem	mreexexlemd 15023*	This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 15027. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> X e. J )   &    |- ( ph -> F C_ ( X \ H ) )   &    |- ( ph -> G C_ ( X \ H ) )   &    |- ( ph -> F C_ ( N ` ( G u. H ) ) )   &    |- ( ph -> ( F u. H ) e. I )   &    |- ( ph -> ( F ~~ K \/ G ~~ K ) )   &    |- ( ph -> A. t A. u e. ~P ( X \ t ) A. v e. ~P ( X \ t ) ( ( ( u ~~ K \/ v ~~ K ) /\ u C_ ( N ` ( v u. t ) ) /\ ( u u. t ) e. I ) -> E. i e. ~P v ( u ~~ i /\ ( i u. t ) e. I ) ) )   =>    |- ( ph -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
Theorem	mreexexlem2d 15024*	Used in mreexexlem4d 15026 to prove the induction step in mreexexd 15027. See the proof of Proposition 4.2.1 in [FaureFrolicher] p. 86 to 87. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )   &    |- ( ph -> F C_ ( X \ H ) )   &    |- ( ph -> G C_ ( X \ H ) )   &    |- ( ph -> F C_ ( N ` ( G u. H ) ) )   &    |- ( ph -> ( F u. H ) e. I )   &    |- ( ph -> Y e. F )   =>    |- ( ph -> E. g e. G ( -. g e. ( F \ { Y } ) /\ ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) )
Theorem	mreexexlem3d 15025*	Base case of the induction in mreexexd 15027. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )   &    |- ( ph -> F C_ ( X \ H ) )   &    |- ( ph -> G C_ ( X \ H ) )   &    |- ( ph -> F C_ ( N ` ( G u. H ) ) )   &    |- ( ph -> ( F u. H ) e. I )   &    |- ( ph -> ( F = (/) \/ G = (/) ) )   =>    |- ( ph -> E. i e. ~P G ( F ~~ i /\ ( i u. H ) e. I ) )
Theorem	mreexexlem4d 15026*	Induction step of the induction in mreexexd 15027. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )   &    |- ( ph -> F C_ ( X \ H ) )   &    |- ( ph -> G C_ ( X \ H ) )   &    |- ( ph -> F C_ ( N ` ( G u. H ) ) )   &    |- ( ph -> ( F u. H ) e. I )   &    |- ( ph -> L e. om )   &    |- ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ L \/ g ~~ L ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) )   &    |- ( ph -> ( F ~~ suc L \/ G ~~ suc L ) )   =>    |- ( ph -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
Theorem	mreexexd 15027*	Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if F and G are disjoint from H, ( F u. H ) is independent, F is contained in the closure of ( G u. H ), and either F or G is finite, then there is a subset q of G equinumerous to F such that ( q u. H ) is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either ( A \ B ) or ( B \ A ) is finite. The theorem is proven by induction using mreexexlem3d 15025 for the base case and mreexexlem4d 15026 for the induction step. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )   &    |- ( ph -> F C_ ( X \ H ) )   &    |- ( ph -> G C_ ( X \ H ) )   &    |- ( ph -> F C_ ( N ` ( G u. H ) ) )   &    |- ( ph -> ( F u. H ) e. I )   &    |- ( ph -> ( F e. Fin \/ G e. Fin ) )   =>    |- ( ph -> E. q e. ~P G ( F ~~ q /\ ( q u. H ) e. I ) )
Theorem	mreexdomd 15028*	In a Moore system whose closure operator has the exchange property, if S is independent and contained in the closure of T, and either S or T is finite, then T dominates S. This is an immediate consequence of mreexexd 15027. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )   &    |- ( ph -> S C_ ( N ` T ) )   &    |- ( ph -> T C_ X )   &    |- ( ph -> ( S e. Fin \/ T e. Fin ) )   &    |- ( ph -> S e. I )   =>    |- ( ph -> S ~<_ T )
Theorem	mreexfidimd 15029*	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 15028 twice. This implies a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (Moore ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )   &    |- ( ph -> S e. I )   &    |- ( ph -> T e. I )   &    |- ( ph -> S e. Fin )   &    |- ( ph -> ( N ` S ) = ( N ` T ) )   =>    |- ( ph -> S ~~ T )
7.2.3  Algebraic closure systems
Theorem	isacs 15030*	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.)
|- ( C e. (ACS ` X ) <-> ( 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	acsmre 15031	Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ( C e. (ACS ` X ) -> C e. (Moore ` X ) )
Theorem	isacs2 15032*	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.)
|- F = (mrCls ` C )   =>    |- ( C e. (ACS ` X ) <-> ( C e. (Moore ` X ) /\ A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )
Theorem	acsfiel 15033*	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.)
|- F = (mrCls ` C )   =>    |- ( C e. (ACS ` X ) -> ( S e. C <-> ( S C_ X /\ A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) ) )
Theorem	acsfiel2 15034*	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.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (ACS ` X ) /\ S C_ X ) -> ( S e. C <-> A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) )
Theorem	acsmred 15035	An algebraic closure system is also a Moore system. Deduction form of acsmre 15031. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   =>    |- ( ph -> A e. (Moore ` X ) )
Theorem	isacs1i 15036*	A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. (ACS ` X ) )
Theorem	mreacs 15037	Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( X e. V -> (ACS ` X ) e. (Moore ` ~P X ) )
Theorem	acsfn 15038*	Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> { a e. ~P X | ( T C_ a -> K e. a ) } e. (ACS ` X ) )
Theorem	acsfn0 15039*	Algebraicity of a point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ( X e. V /\ K e. X ) -> { a e. ~P X | K e. a } e. (ACS ` X ) )
Theorem	acsfn1 15040*	Algebraicity of a one-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ( X e. V /\ A. b e. X E e. X ) -> { a e. ~P X | A. b e. a E e. a } e. (ACS ` X ) )
Theorem	acsfn1c 15041*	Algebraicity of a one-argument closure condition with additional constant. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ( X e. V /\ A. b e. K A. c e. X E e. X ) -> { a e. ~P X | A. b e. K A. c e. a E e. a } e. (ACS ` X ) )
Theorem	acsfn2 15042*	Algebraicity of a two-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ( X e. V /\ A. b e. X A. c e. X E e. X ) -> { a e. ~P X | A. b e. a A. c e. a E e. a } e. (ACS ` X ) )
PART 8  BASIC CATEGORY THEORY
8.1  Categories
8.1.1  Categories
Syntax	ccat 15043	Extend class notation with the class of categories.
class Cat
Syntax	ccid 15044	Extend class notation with the identity arrow of a category.
class Id
Syntax	chomf 15045	Extend class notation to include functionalized Hom-set extractor.
class Hom f
Syntax	ccomf 15046	Extend class notation to include functionalized composition operation.
class compf
Definition	df-cat 15047*	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 to 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. (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)
|- Cat = { c | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. (comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) }
Definition	df-cid 15048*	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.)
|- Id = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ (comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) )
Definition	df-homf 15049*	Define the functionalized Hom-set operator, which is exactly like Hom but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- Hom f = ( c e. _V |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( x ( Hom ` c ) y ) ) )
Definition	df-comf 15050*	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 = ( c e. _V |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) , y e. ( Base ` c ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x (comp ` c ) y ) f ) ) ) )
Theorem	iscat 15051*	The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   =>    |- ( C e. V -> ( C e. Cat <-> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )
Theorem	iscatd 15052*	Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- ( ph -> B = ( Base ` C ) )   &    |- ( ph -> H = ( Hom ` C ) )   &    |- ( ph -> .x. = (comp ` C ) )   &    |- ( ph -> C e. V )   &    |- ( ( ph /\ x e. B ) -> .1. e. ( x H x ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( y H x ) ) ) -> ( .1. ( <. y , x >. .x. x ) f ) = f )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( x H y ) ) ) -> ( f ( <. x , x >. .x. y ) .1. ) = f )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )   &    |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )   =>    |- ( ph -> C e. Cat )
Theorem	catidex 15053*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> E. g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) )
Theorem	catideu 15054*	Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> E! g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) )
Theorem	cidfval 15055*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> C e. Cat )   &    |- .1. = ( Id ` C )   =>    |- ( ph -> .1. = ( x e. B |-> ( iota_ g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) ) ) )
Theorem	cidval 15056*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> C e. Cat )   &    |- .1. = ( Id ` C )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( .1. ` X ) = ( iota_ g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) )
Theorem	cidffn 15057	The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- Id Fn Cat
Theorem	cidfn 15058	The identity arrow operator is a function from objects to arrows. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- B = ( Base ` C )   &    |- .1. = ( Id ` C )   =>    |- ( C e. Cat -> .1. Fn B )
Theorem	catidd 15059*	Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> B = ( Base ` C ) )   &    |- ( ph -> H = ( Hom ` C ) )   &    |- ( ph -> .x. = (comp ` C ) )   &    |- ( ph -> C e. Cat )   &    |- ( ( ph /\ x e. B ) -> .1. e. ( x H x ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( y H x ) ) ) -> ( .1. ( <. y , x >. .x. x ) f ) = f )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( x H y ) ) ) -> ( f ( <. x , x >. .x. y ) .1. ) = f )   =>    |- ( ph -> ( Id ` C ) = ( x e. B |-> .1. ) )
Theorem	iscatd2 15060*	Version of iscatd 15052 with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> B = ( Base ` C ) )   &    |- ( ph -> H = ( Hom ` C ) )   &    |- ( ph -> .x. = (comp ` C ) )   &    |- ( ph -> C e. V )   &    |- ( ps <-> ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )   &    |- ( ( ph /\ y e. B ) -> .1. e. ( y H y ) )   &    |- ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )   &    |- ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )   &    |- ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )   &    |- ( ( ph /\ ps ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )   =>    |- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. B |-> .1. ) ) )
Theorem	catidcl 15061	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( .1. ` X ) e. ( X H X ) )
Theorem	catlid 15062	Left identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- .x. = (comp ` C )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( ( .1. ` Y ) ( <. X , Y >. .x. Y ) F ) = F )
Theorem	catrid 15063	Right identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- .x. = (comp ` C )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( F ( <. X , X >. .x. Y ) ( .1. ` X ) ) = F )
Theorem	catcocl 15064	Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) )
Theorem	catass 15065	Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   &    |- ( ph -> W e. B )   &    |- ( ph -> K e. ( Z H W ) )   =>    |- ( ph -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) )
Theorem	0catg 15066	Any structure with an empty set of objects is a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. Cat )
Theorem	0cat 15067	The empty set is a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- (/) e. Cat
Theorem	homffval 15068*	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- F = ( Hom f ` C )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   =>    |- F = ( x e. B , y e. B |-> ( x H y ) )
Theorem	homfval 15069	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- F = ( Hom f ` C )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X F Y ) = ( X H Y ) )
Theorem	homffn 15070	The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- F = ( Hom f ` C )   &    |- B = ( Base ` C )   =>    |- F Fn ( B X. B )
Theorem	homfeq 15071*	Condition for two categories with the same base to have the same hom-sets. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> B = ( Base ` C ) )   &    |- ( ph -> B = ( Base ` D ) )   =>    |- ( ph -> ( ( Hom f ` C ) = ( Hom f ` D ) <-> A. x e. B A. y e. B ( x H y ) = ( x J y ) ) )
Theorem	homfeqd 15072	If two structures have the same Hom slot, they have the same Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ( Base ` C ) = ( Base ` D ) )   &    |- ( ph -> ( Hom ` C ) = ( Hom ` D ) )   =>    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )
Theorem	homfeqbas 15073	Deduce equality of base sets from equality of Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   =>    |- ( ph -> ( Base ` C ) = ( Base ` D ) )
Theorem	homfeqval 15074	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X J Y ) )
Theorem	comfffval 15075*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- O = (compf ` C )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   =>    |- O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) )
Theorem	comffval 15076*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- O = (compf ` C )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( <. X , Y >. O Z ) = ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) )
Theorem	comfval 15077	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- O = (compf ` C )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. O Z ) F ) = ( G ( <. X , Y >. .x. Z ) F ) )
Theorem	comfffval2 15078*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- O = (compf ` C )   &    |- B = ( Base ` C )   &    |- H = ( Hom f ` C )   &    |- .x. = (comp ` C )   =>    |- O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) )
Theorem	comffval2 15079*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- O = (compf ` C )   &    |- B = ( Base ` C )   &    |- H = ( Hom f ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( <. X , Y >. O Z ) = ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) )
Theorem	comfval2 15080	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- O = (compf ` C )   &    |- B = ( Base ` C )   &    |- H = ( Hom f ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. O Z ) F ) = ( G ( <. X , Y >. .x. Z ) F ) )
Theorem	comfffn 15081	The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- O = (compf ` C )   &    |- B = ( Base ` C )   =>    |- O Fn ( ( B X. B ) X. B )
Theorem	comffn 15082	The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- O = (compf ` C )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( <. X , Y >. O Z ) Fn ( ( Y H Z ) X. ( X H Y ) ) )
Theorem	comfeq 15083*	Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- .x. = (comp ` C )   &    |- .xb = (comp ` D )   &    |- H = ( Hom ` C )   &    |- ( ph -> B = ( Base ` C ) )   &    |- ( ph -> B = ( Base ` D ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   =>    |- ( ph -> ( (compf ` C ) = (compf ` D ) <-> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) ) )
Theorem	comfeqd 15084	Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> (comp ` C ) = (comp ` D ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   =>    |- ( ph -> (compf ` C ) = (compf ` D ) )
Theorem	comfeqval 15085	Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- .xb = (comp ` D )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G ( <. X , Y >. .xb Z ) F ) )
Theorem	catpropd 15086	Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. W )   =>    |- ( ph -> ( C e. Cat <-> D e. Cat ) )
Theorem	cidpropd 15087	Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. W )   =>    |- ( ph -> ( Id ` C ) = ( Id ` D ) )
8.1.2  Opposite category
Syntax	coppc 15088	The opposite category operation.
class oppCat
Definition	df-oppc 15089*	Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- oppCat = ( f e. _V |-> ( ( f sSet <. ( Hom ` ndx ) , tpos ( Hom ` f ) >. ) sSet <. (comp ` ndx ) , ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. (comp ` f ) ( 1st ` u ) ) ) >. ) )
Theorem	oppcval 15090*	Value of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- O = (oppCat ` C )   =>    |- ( C e. V -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. (comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
Theorem	oppchomfval 15091	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- H = ( Hom ` C )   &    |- O = (oppCat ` C )   =>    |- tpos H = ( Hom ` O )
Theorem	oppchom 15092	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- H = ( Hom ` C )   &    |- O = (oppCat ` C )   =>    |- ( X ( Hom ` O ) Y ) = ( Y H X )
Theorem	oppccofval 15093	Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- .x. = (comp ` C )   &    |- O = (oppCat ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( <. X , Y >. (comp ` O ) Z ) = tpos ( <. Z , Y >. .x. X ) )
Theorem	oppcco 15094	Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- .x. = (comp ` C )   &    |- O = (oppCat ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( G ( <. X , Y >. (comp ` O ) Z ) F ) = ( F ( <. Z , Y >. .x. X ) G ) )
Theorem	oppcbas 15095	Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- O = (oppCat ` C )   &    |- B = ( Base ` C )   =>    |- B = ( Base ` O )
Theorem	oppccatid 15096	Lemma for oppccat 15099. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- O = (oppCat ` C )   =>    |- ( C e. Cat -> ( O e. Cat /\ ( Id ` O ) = ( Id ` C ) ) )
Theorem	oppchomf 15097	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- O = (oppCat ` C )   &    |- H = ( Hom f ` C )   =>    |- tpos H = ( Hom f ` O )
Theorem	oppcid 15098	Identity function of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- O = (oppCat ` C )   &    |- B = ( Id ` C )   =>    |- ( C e. Cat -> ( Id ` O ) = B )
Theorem	oppccat 15099	An opposite category is a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- O = (oppCat ` C )   =>    |- ( C e. Cat -> O e. Cat )
Theorem	2oppcbas 15100	The double opposite category has the same objects as the original category. Intended for use with property lemmas such as monpropd 15114. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- O = (oppCat ` C )   &    |- B = ( Base ` C )   =>    |- B = ( Base ` (oppCat ` O ) )