:: OPPCAT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let X, Y, Z be non empty set ;
let f be PartFunc of [:X,Y:],Z;
:: original: ~
redefine func ~ f -> PartFunc of [:Y,X:],Z;
coherence
~ f is PartFunc of [:Y,X:],Z
by FUNCT_4:49;
end;

theorem Th1: :: OPPCAT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category holds CatStr(# the Objects of C,the Morphisms of C,the Cod of C,the Dom of C,(~ the Comp of C),the Id of C #) is Category
proof end;

definition
let C be Category;
func C opp -> strict Category equals :: OPPCAT_1:def 1
CatStr(# the Objects of C,the Morphisms of C,the Cod of C,the Dom of C,(~ the Comp of C),the Id of C #);
coherence
CatStr(# the Objects of C,the Morphisms of C,the Cod of C,the Dom of C,(~ the Comp of C),the Id of C #) is strict Category
by Th1;
end;

:: deftheorem defines opp OPPCAT_1:def 1 :
for C being Category holds C opp = CatStr(# the Objects of C,the Morphisms of C,the Cod of C,the Dom of C,(~ the Comp of C),the Id of C #);

theorem Th2: :: OPPCAT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category holds (C opp ) opp = CatStr(# the Objects of C,the Morphisms of C,the Dom of C,the Cod of C,the Comp of C,the Id of C #) by FUNCT_4:54;

definition
let C be Category;
let c be Object of C;
func c opp -> Object of (C opp ) equals :: OPPCAT_1:def 2
c;
coherence
c is Object of (C opp )
;
end;

:: deftheorem defines opp OPPCAT_1:def 2 :
for C being Category
for c being Object of C holds c opp = c;

definition
let C be Category;
let c be Object of (C opp );
func opp c -> Object of C equals :: OPPCAT_1:def 3
c opp ;
coherence
c opp is Object of C
;
end;

:: deftheorem defines opp OPPCAT_1:def 3 :
for C being Category
for c being Object of (C opp ) holds opp c = c opp ;

theorem :: OPPCAT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C holds (c opp ) opp = c ;

theorem :: OPPCAT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C holds opp (c opp ) = c ;

theorem :: OPPCAT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of (C opp ) holds (opp c) opp = c ;

definition
let C be Category;
let f be Morphism of C;
func f opp -> Morphism of (C opp ) equals :: OPPCAT_1:def 4
f;
coherence
f is Morphism of (C opp )
;
end;

:: deftheorem defines opp OPPCAT_1:def 4 :
for C being Category
for f being Morphism of C holds f opp = f;

definition
let C be Category;
let f be Morphism of (C opp );
func opp f -> Morphism of C equals :: OPPCAT_1:def 5
f opp ;
coherence
f opp is Morphism of C
;
end;

:: deftheorem defines opp OPPCAT_1:def 5 :
for C being Category
for f being Morphism of (C opp ) holds opp f = f opp ;

theorem :: OPPCAT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds (f opp ) opp = f ;

theorem :: OPPCAT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds opp (f opp ) = f ;

theorem :: OPPCAT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of (C opp ) holds (opp f) opp = f ;

theorem :: OPPCAT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds
( dom (f opp ) = cod f & cod (f opp ) = dom f ) ;

theorem :: OPPCAT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of (C opp ) holds
( dom (opp f) = cod f & cod (opp f) = dom f ) ;

theorem :: OPPCAT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds
( (dom f) opp = cod (f opp ) & (cod f) opp = dom (f opp ) ) ;

theorem :: OPPCAT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of (C opp ) holds
( opp (dom f) = cod (opp f) & opp (cod f) = dom (opp f) ) ;

theorem Th13: :: OPPCAT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of C
for f being Morphism of C holds
( f in Hom a,b iff f opp in Hom (b opp ),(a opp ) )
proof end;

theorem Th14: :: OPPCAT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of (C opp )
for f being Morphism of (C opp ) holds
( f in Hom a,b iff opp f in Hom (opp b),(opp a) )
proof end;

theorem Th15: :: OPPCAT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom a,b <> {} holds
f opp is Morphism of b opp ,a opp
proof end;

theorem Th16: :: OPPCAT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of (C opp )
for f being Morphism of a,b st Hom a,b <> {} holds
opp f is Morphism of opp b, opp a
proof end;

theorem Th17: :: OPPCAT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f, g being Morphism of C st dom g = cod f holds
(g * f) opp = (f opp ) * (g opp )
proof end;

theorem Th18: :: OPPCAT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f, g being Morphism of C st cod (g opp ) = dom (f opp ) holds
(g * f) opp = (f opp ) * (g opp )
proof end;

theorem Th19: :: OPPCAT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f, g being Morphism of (C opp ) st dom g = cod f holds
opp (g * f) = (opp f) * (opp g)
proof end;

theorem :: OPPCAT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom a,b <> {} & Hom b,c <> {} holds
(g * f) opp = (f opp ) * (g opp )
proof end;

theorem :: OPPCAT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C holds (id a) opp = id (a opp ) ;

theorem :: OPPCAT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of (C opp ) holds opp (id a) = id (opp a) ;

theorem :: OPPCAT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds
( f opp is monic iff f is epi )
proof end;

theorem :: OPPCAT_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds
( f opp is epi iff f is monic )
proof end;

theorem :: OPPCAT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds
( f opp is invertible iff f is invertible )
proof end;

theorem :: OPPCAT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C holds
( c is initial iff c opp is terminal )
proof end;

theorem :: OPPCAT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C holds
( c opp is initial iff c is terminal )
proof end;

definition
let C, B be Category;
let S be Function of the Morphisms of (C opp ),the Morphisms of B;
func /* S -> Function of the Morphisms of C,the Morphisms of B means :Def6: :: OPPCAT_1:def 6
for f being Morphism of C holds it . f = S . (f opp );
existence
ex b1 being Function of the Morphisms of C,the Morphisms of B st
for f being Morphism of C holds b1 . f = S . (f opp )
proof end;
uniqueness
for b1, b2 being Function of the Morphisms of C,the Morphisms of B st ( for f being Morphism of C holds b1 . f = S . (f opp ) ) & ( for f being Morphism of C holds b2 . f = S . (f opp ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines /* OPPCAT_1:def 6 :
for C, B being Category
for S being Function of the Morphisms of (C opp ),the Morphisms of B
for b4 being Function of the Morphisms of C,the Morphisms of B holds
( b4 = /* S iff for f being Morphism of C holds b4 . f = S . (f opp ) );

theorem :: OPPCAT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Function of the Morphisms of (C opp ),the Morphisms of B
for f being Morphism of (C opp ) holds (/* S) . (opp f) = S . f
proof end;

Lm1: for C, B being Category
for S being Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp ))
proof end;

theorem Th29: :: OPPCAT_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Functor of C opp ,B
for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp )
proof end;

theorem :: OPPCAT_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Functor of C opp ,B
for c being Object of (C opp ) holds (Obj (/* S)) . (opp c) = (Obj S) . c
proof end;

Lm2: for C, B being Category
for S being Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
proof end;

Lm3: now
let C, B be Category;
let S be Functor of C opp ,B; :: thesis: for c being Object of C ex d being Object of B st (/* S) . (id c) = id d
let c be Object of C; :: thesis: ex d being Object of B st (/* S) . (id c) = id d
(/* S) . (id c) = id ((Obj (/* S)) . c) by Lm2;
hence ex d being Object of B st (/* S) . (id c) = id d ; :: thesis: verum
end;

Lm4: for C, B being Category
for S being Functor of C opp ,B
for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) )
proof end;

Lm5: now
let C, B be Category;
let S be Functor of C opp ,B; :: thesis: for f being Morphism of C holds
( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )

let f be Morphism of C; :: thesis: ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )
thus (/* S) . (id (dom f)) = id ((Obj (/* S)) . (dom f)) by Lm2
.= id (cod ((/* S) . f)) by Lm4 ; :: thesis: (/* S) . (id (cod f)) = id (dom ((/* S) . f))
thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm2
.= id (dom ((/* S) . f)) by Lm4 ; :: thesis: verum
end;

Lm6: for C, B being Category
for S being Functor of C opp ,B
for f, g being Morphism of C st dom g = cod f holds
(/* S) . (g * f) = ((/* S) . f) * ((/* S) . g)
proof end;

definition
let C, D be Category;
mode Contravariant_Functor of C,D -> Function of the Morphisms of C,the Morphisms of D means :Def7: :: OPPCAT_1:def 7
( ( for c being Object of C ex d being Object of D st it . (id c) = id d ) & ( for f being Morphism of C holds
( it . (id (dom f)) = id (cod (it . f)) & it . (id (cod f)) = id (dom (it . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
it . (g * f) = (it . f) * (it . g) ) );
existence
ex b1 being Function of the Morphisms of C,the Morphisms of D st
( ( for c being Object of C ex d being Object of D st b1 . (id c) = id d ) & ( for f being Morphism of C holds
( b1 . (id (dom f)) = id (cod (b1 . f)) & b1 . (id (cod f)) = id (dom (b1 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b1 . (g * f) = (b1 . f) * (b1 . g) ) )
proof end;
end;

:: deftheorem Def7 defines Contravariant_Functor OPPCAT_1:def 7 :
for C, D being Category
for b3 being Function of the Morphisms of C,the Morphisms of D holds
( b3 is Contravariant_Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b3 . (id c) = id d ) & ( for f being Morphism of C holds
( b3 . (id (dom f)) = id (cod (b3 . f)) & b3 . (id (cod f)) = id (dom (b3 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b3 . (g * f) = (b3 . f) * (b3 . g) ) ) );

theorem Th31: :: OPPCAT_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Contravariant_Functor of C,D
for c being Object of C
for d being Object of D st S . (id c) = id d holds
(Obj S) . c = d
proof end;

theorem Th32: :: OPPCAT_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Contravariant_Functor of C,D
for c being Object of C holds S . (id c) = id ((Obj S) . c)
proof end;

theorem Th33: :: OPPCAT_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Contravariant_Functor of C,D
for f being Morphism of C holds
( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )
proof end;

theorem Th34: :: OPPCAT_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Contravariant_Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
dom (S . f) = cod (S . g)
proof end;

theorem Th35: :: OPPCAT_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Functor of C opp ,B holds /* S is Contravariant_Functor of C,B
proof end;

theorem Th36: :: OPPCAT_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B, D being Category
for S1 being Contravariant_Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D
proof end;

Lm7: for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp ))
proof end;

theorem Th37: :: OPPCAT_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp )
proof end;

theorem :: OPPCAT_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of (C opp ) holds (Obj (/* S)) . (opp c) = (Obj S) . c
proof end;

Lm8: for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
proof end;

Lm9: for C, B being Category
for S being Contravariant_Functor of C opp ,B
for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )
proof end;

theorem :: OPPCAT_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Contravariant_Functor of C opp ,B holds /* S is Functor of C,B
proof end;

definition
let C, B be Category;
let S be Function of the Morphisms of C,the Morphisms of B;
func *' S -> Function of the Morphisms of (C opp ),the Morphisms of B means :Def8: :: OPPCAT_1:def 8
for f being Morphism of (C opp ) holds it . f = S . (opp f);
existence
ex b1 being Function of the Morphisms of (C opp ),the Morphisms of B st
for f being Morphism of (C opp ) holds b1 . f = S . (opp f)
proof end;
uniqueness
for b1, b2 being Function of the Morphisms of (C opp ),the Morphisms of B st ( for f being Morphism of (C opp ) holds b1 . f = S . (opp f) ) & ( for f being Morphism of (C opp ) holds b2 . f = S . (opp f) ) holds
b1 = b2
proof end;
func S *' -> Function of the Morphisms of C,the Morphisms of (B opp ) means :Def9: :: OPPCAT_1:def 9
for f being Morphism of C holds it . f = (S . f) opp ;
existence
ex b1 being Function of the Morphisms of C,the Morphisms of (B opp ) st
for f being Morphism of C holds b1 . f = (S . f) opp
proof end;
uniqueness
for b1, b2 being Function of the Morphisms of C,the Morphisms of (B opp ) st ( for f being Morphism of C holds b1 . f = (S . f) opp ) & ( for f being Morphism of C holds b2 . f = (S . f) opp ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines *' OPPCAT_1:def 8 :
for C, B being Category
for S being Function of the Morphisms of C,the Morphisms of B
for b4 being Function of the Morphisms of (C opp ),the Morphisms of B holds
( b4 = *' S iff for f being Morphism of (C opp ) holds b4 . f = S . (opp f) );

:: deftheorem Def9 defines *' OPPCAT_1:def 9 :
for C, B being Category
for S being Function of the Morphisms of C,the Morphisms of B
for b4 being Function of the Morphisms of C,the Morphisms of (B opp ) holds
( b4 = S *' iff for f being Morphism of C holds b4 . f = (S . f) opp );

theorem :: OPPCAT_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Function of the Morphisms of C,the Morphisms of B
for f being Morphism of C holds (*' S) . (f opp ) = S . f
proof end;

Lm10: for C, B being Category
for S being Functor of C,B
for c being Object of (C opp ) holds (*' S) . (id c) = id ((Obj S) . (opp c))
proof end;

theorem Th41: :: OPPCAT_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Functor of C,B
for c being Object of (C opp ) holds (Obj (*' S)) . c = (Obj S) . (opp c)
proof end;

theorem :: OPPCAT_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Functor of C,B
for c being Object of C holds (Obj (*' S)) . (c opp ) = (Obj S) . c
proof end;

Lm11: for C, B being Category
for S being Functor of C,B
for c being Object of C holds (S *' ) . (id c) = id (((Obj S) . c) opp )
proof end;

theorem Th43: :: OPPCAT_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Functor of C,B
for c being Object of C holds (Obj (S *' )) . c = ((Obj S) . c) opp
proof end;

Lm12: for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of (C opp ) holds (*' S) . (id c) = id ((Obj S) . (opp c))
proof end;

theorem Th44: :: OPPCAT_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of (C opp ) holds (Obj (*' S)) . c = (Obj S) . (opp c)
proof end;

theorem :: OPPCAT_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (Obj (*' S)) . (c opp ) = (Obj S) . c
proof end;

Lm13: for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (S *' ) . (id c) = id (((Obj S) . c) opp )
proof end;

theorem Th46: :: OPPCAT_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (Obj (S *' )) . c = ((Obj S) . c) opp
proof end;

Lm14: for C, D being Category
for F being Function of the Morphisms of C,the Morphisms of D
for f being Morphism of (C opp ) holds ((*' F) *' ) . f = (F . (opp f)) opp
proof end;

theorem Th47: :: OPPCAT_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for F being Function of the Morphisms of C,the Morphisms of D
for f being Morphism of C holds ((*' F) *' ) . (f opp ) = (F . f) opp
proof end;

theorem Th48: :: OPPCAT_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Function of the Morphisms of C,the Morphisms of D holds /* (*' S) = S
proof end;

theorem :: OPPCAT_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Function of the Morphisms of (C opp ),the Morphisms of D holds *' (/* S) = S
proof end;

theorem :: OPPCAT_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Function of the Morphisms of C,the Morphisms of D holds (*' S) *' = *' (S *' )
proof end;

theorem :: OPPCAT_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for D being strict Category
for S being Function of the Morphisms of C,the Morphisms of D holds (S *' ) *' = S
proof end;

theorem :: OPPCAT_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being Category
for C being strict Category
for S being Function of the Morphisms of C,the Morphisms of D holds *' (*' S) = S
proof end;

Lm15: for C, B, D being Category
for S being Function of the Morphisms of (C opp ),the Morphisms of B
for T being Function of the Morphisms of B,the Morphisms of D holds /* (T * S) = T * (/* S)
proof end;

theorem :: OPPCAT_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B, D being Category
for S being Function of the Morphisms of C,the Morphisms of B
for T being Function of the Morphisms of B,the Morphisms of D holds *' (T * S) = T * (*' S)
proof end;

theorem :: OPPCAT_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B, D being Category
for S being Function of the Morphisms of C,the Morphisms of B
for T being Function of the Morphisms of B,the Morphisms of D holds (T * S) *' = (T *' ) * S
proof end;

theorem :: OPPCAT_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B, D being Category
for F1 being Function of the Morphisms of C,the Morphisms of B
for F2 being Function of the Morphisms of B,the Morphisms of D holds (*' (F2 * F1)) *' = ((*' F2) *' ) * ((*' F1) *' )
proof end;

Lm16: for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of (C opp ) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
proof end;

Lm17: for C, B being Category
for S being Contravariant_Functor of C,B
for f being Morphism of (C opp ) holds
( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
proof end;

theorem Th56: :: OPPCAT_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Contravariant_Functor of C,D holds *' S is Functor of C opp ,D
proof end;

Lm18: for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (S *' ) . (id c) = id ((Obj (S *' )) . c)
proof end;

Lm19: for C, B being Category
for S being Contravariant_Functor of C,B
for f being Morphism of C holds
( (Obj (S *' )) . (dom f) = dom ((S *' ) . f) & (Obj (S *' )) . (cod f) = cod ((S *' ) . f) )
proof end;

theorem Th57: :: OPPCAT_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Contravariant_Functor of C,D holds S *' is Functor of C,D opp
proof end;

Lm20: for C, B being Category
for S being Functor of C,B
for c being Object of (C opp ) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
proof end;

Lm21: for C, B being Category
for S being Functor of C,B
for f being Morphism of (C opp ) holds
( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) )
proof end;

theorem Th58: :: OPPCAT_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Functor of C,D holds *' S is Contravariant_Functor of C opp ,D
proof end;

Lm22: for C, B being Category
for S being Functor of C,B
for c being Object of C holds (S *' ) . (id c) = id ((Obj (S *' )) . c)
proof end;

Lm23: for C, B being Category
for S being Functor of C,B
for f being Morphism of C holds
( (Obj (S *' )) . (dom f) = cod ((S *' ) . f) & (Obj (S *' )) . (cod f) = dom ((S *' ) . f) )
proof end;

theorem Th59: :: OPPCAT_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Functor of C,D holds S *' is Contravariant_Functor of C,D opp
proof end;

theorem :: OPPCAT_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B, D being Category
for S1 being Contravariant_Functor of C,B
for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
proof end;

theorem :: OPPCAT_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B, D being Category
for S1 being Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
proof end;

theorem :: OPPCAT_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for F being Functor of C,D
for c being Object of C holds (Obj ((*' F) *' )) . (c opp ) = ((Obj F) . c) opp
proof end;

theorem :: OPPCAT_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for F being Contravariant_Functor of C,D
for c being Object of C holds (Obj ((*' F) *' )) . (c opp ) = ((Obj F) . c) opp
proof end;

theorem :: OPPCAT_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for F being Functor of C,D holds (*' F) *' is Functor of C opp ,D opp
proof end;

theorem :: OPPCAT_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for F being Contravariant_Functor of C,D holds (*' F) *' is Contravariant_Functor of C opp ,D opp
proof end;

definition
let C be Category;
func id* C -> Contravariant_Functor of C,C opp equals :: OPPCAT_1:def 10
(id C) *' ;
coherence
(id C) *' is Contravariant_Functor of C,C opp
by Th59;
func *id C -> Contravariant_Functor of C opp ,C equals :: OPPCAT_1:def 11
*' (id C);
coherence
*' (id C) is Contravariant_Functor of C opp ,C
by Th58;
end;

:: deftheorem defines id* OPPCAT_1:def 10 :
for C being Category holds id* C = (id C) *' ;

:: deftheorem defines *id OPPCAT_1:def 11 :
for C being Category holds *id C = *' (id C);

theorem Th66: :: OPPCAT_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds (id* C) . f = f opp
proof end;

theorem :: OPPCAT_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C holds (Obj (id* C)) . c = c opp
proof end;

theorem Th68: :: OPPCAT_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of (C opp ) holds (*id C) . f = opp f
proof end;

theorem :: OPPCAT_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of (C opp ) holds (Obj (*id C)) . c = opp c
proof end;

theorem :: OPPCAT_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for S being Function of the Morphisms of C,the Morphisms of D holds
( *' S = S * (*id C) & S *' = (id* D) * S )
proof end;