set M = the carrier' of C;
set d = the Target of C;
set c = the Source of C;
set p = ~ the Comp of C;
set B = C opp ;
thus A1: C opp is Category-like :: thesis: ( C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities )
proof
let f, g be Morphism of (C opp); :: according to CAT_1:def 6 :: thesis: ( ( not [g,f] in dom the Comp of (C opp) or dom g = cod f ) & ( not dom g = cod f or [g,f] in dom the Comp of (C opp) ) )
reconsider ff = f, gg = g as Morphism of C ;
thus ( [g,f] in dom the Comp of (C opp) implies dom g = cod f ) :: thesis: ( not dom g = cod f or [g,f] in dom the Comp of (C opp) )
proof
assume [g,f] in dom the Comp of (C opp) ; :: thesis: dom g = cod f
then [ff,gg] in dom the Comp of C by FUNCT_4:42;
then dom ff = cod gg by CAT_1:def 6;
hence dom g = cod f ; :: thesis: verum
end;
assume A2: dom g = cod f ; :: thesis: [g,f] in dom the Comp of (C opp)
cod gg = dom ff by A2;
then [ff,gg] in dom the Comp of C by CAT_1:def 6;
hence [g,f] in dom the Comp of (C opp) by FUNCT_4:42; :: thesis: verum
end;
A3: for f, g being Element of the carrier' of C st the Target of C . g = the Source of C . f holds
(~ the Comp of C) . (g,f) = the Comp of C . (f,g)
proof
let f, g be Element of the carrier' of C; :: thesis: ( the Target of C . g = the Source of C . f implies (~ the Comp of C) . (g,f) = the Comp of C . (f,g) )
reconsider ff = f, gg = g as Morphism of (C opp) ;
assume the Target of C . g = the Source of C . f ; :: thesis: (~ the Comp of C) . (g,f) = the Comp of C . (f,g)
then dom gg = cod ff ;
then [gg,ff] in dom (~ the Comp of C) by A1;
hence (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by FUNCT_4:43; :: thesis: verum
end;
thus A4: C opp is transitive :: thesis: ( C opp is associative & C opp is reflexive & C opp is with_identities )
proof
let ff, gg be Morphism of (C opp); :: according to CAT_1:def 7 :: thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
reconsider f = ff, g = gg as Morphism of C ;
assume A5: dom gg = cod ff ; :: thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )
then A6: cod g = dom f ;
then A7: [f,g] in dom the Comp of C by CAT_1:def 6;
[gg,ff] in dom the Comp of (C opp) by A5, A1;
then A8: gg (*) ff = (~ the Comp of C) . (g,f) by CAT_1:def 1
.= the Comp of C . (f,g) by A3, A5
.= f (*) g by A7, CAT_1:def 1 ;
hence dom (gg (*) ff) = cod (f (*) g)
.= cod f by A6, CAT_1:def 7
.= dom ff ;
:: thesis: cod (gg (*) ff) = cod gg
thus cod (gg (*) ff) = dom (f (*) g) by A8
.= dom g by A6, CAT_1:def 7
.= cod gg ; :: thesis: verum
end;
thus C opp is associative :: thesis: ( C opp is reflexive & C opp is with_identities )
proof
let ff, gg, hh be Morphism of (C opp); :: according to CAT_1:def 8 :: thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff )
reconsider f = ff, g = gg, h = hh as Morphism of C ;
assume that
A9: dom hh = cod gg and
A10: dom gg = cod ff ; :: thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff
A11: [h,g] in dom (~ the Comp of C) by A1, A9;
then A12: (~ the Comp of C) . (h,g) is Element of the carrier' of C by PARTFUN1:4;
A13: [g,f] in dom (~ the Comp of C) by A1, A10;
then A14: (~ the Comp of C) . (g,f) is Element of the carrier' of C by PARTFUN1:4;
A15: (~ the Comp of C) . (h,g) = the Comp of C . (g,h) by A3, A9;
the Target of C . ((~ the Comp of C) . (h,g)) = dom (hh (*) gg) by A11, CAT_1:def 1
.= dom gg by A4, A9 ;
then A16: (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) = the Comp of C . (f,( the Comp of C . (g,h))) by A3, A10, A12, A15;
A17: ( cod h = dom g & cod g = dom f ) by A9, A10;
A18: (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by A3, A10;
A19: the Source of C . ((~ the Comp of C) . (g,f)) = cod (gg (*) ff) by A13, CAT_1:def 1
.= cod gg by A4, A10 ;
dom (hh (*) gg) = dom gg by A4, A9;
then A20: [(hh (*) gg),ff] in dom the Comp of (C opp) by A1, A10;
cod (gg (*) ff) = cod gg by A4, A10;
then A21: [hh,(gg (*) ff)] in dom the Comp of (C opp) by A1, A9;
[hh,gg] in dom the Comp of (C opp) by A9, A1;
then A22: hh (*) gg = (~ the Comp of C) . (h,g) by CAT_1:def 1;
A23: f (*) g = the Comp of C . (f,g) by A17, CAT_1:16;
A24: dom (f (*) g) = dom g by A17, CAT_1:def 7;
A25: g (*) h = the Comp of C . (g,h) by A17, CAT_1:16;
A26: cod (g (*) h) = cod g by A17, CAT_1:def 7;
[gg,ff] in dom the Comp of (C opp) by A10, A1;
then gg (*) ff = (~ the Comp of C) . (g,f) by CAT_1:def 1;
hence hh (*) (gg (*) ff) = (~ the Comp of C) . (h,((~ the Comp of C) . (g,f))) by A21, CAT_1:def 1
.= the Comp of C . (( the Comp of C . (f,g)),h) by A3, A9, A14, A18, A19
.= (f (*) g) (*) h by A23, A17, A24, CAT_1:16
.= f (*) (g (*) h) by A17, CAT_1:def 8
.= (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) by A16, A17, A25, A26, CAT_1:16
.= (hh (*) gg) (*) ff by A20, A22, CAT_1:def 1 ;
:: thesis: verum
end;
thus C opp is reflexive :: thesis: C opp is with_identities
proof
let bb be Object of (C opp); :: according to CAT_1:def 9 :: thesis: not Hom (bb,bb) = {}
reconsider b = bb as Element of C ;
consider f being Morphism of C such that
A27: f in Hom (b,b) by SUBSET_1:4;
reconsider ff = f as Morphism of (C opp) ;
A28: dom ff = cod f
.= bb by A27, CAT_1:1 ;
cod ff = dom f
.= bb by A27, CAT_1:1 ;
then ff in Hom (bb,bb) by A28;
hence Hom (bb,bb) <> {} ; :: thesis: verum
end;
let a be Element of (C opp); :: according to CAT_1:def 10 :: thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of (C opp) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider aa = a as Element of C ;
reconsider ii = id aa as Morphism of (C opp) ;
A29: dom ii = cod (id aa)
.= aa ;
A30: cod ii = dom (id aa)
.= aa ;
then reconsider ii = ii as Morphism of a,a by A29, CAT_1:4;
take ii ; :: thesis: for b1 being Element of the carrier of (C opp) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be Element of (C opp); :: thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
reconsider bb = b as Element of C ;
thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) :: thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
assume A31: Hom (a,b) <> {} ; :: thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; :: thesis: g (*) ii = g
reconsider gg = g as Morphism of C ;
A32: dom gg = cod g
.= bb by A31, CAT_1:5 ;
A33: cod gg = dom g
.= aa by A31, CAT_1:5 ;
then A34: cod gg = dom (id aa) ;
reconsider gg = gg as Morphism of bb,aa by A32, A33, CAT_1:4;
A35: the Source of C . ii = aa by A30
.= dom g by A31, CAT_1:5
.= the Target of C . g ;
then dom g = cod ii ;
then [g,ii] in dom the Comp of (C opp) by A1;
hence g (*) ii = (~ the Comp of C) . (g,ii) by CAT_1:def 1
.= the Comp of C . (ii,g) by A35, A3
.= (id aa) (*) gg by A34, CAT_1:16
.= g by A33, CAT_1:21 ;
:: thesis: verum
end;
assume A36: Hom (b,a) <> {} ; :: thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1
let g be Morphism of b,a; :: thesis: ii (*) g = g
reconsider gg = g as Morphism of C ;
A37: cod gg = dom g
.= bb by A36, CAT_1:5 ;
A38: dom gg = cod g
.= aa by A36, CAT_1:5 ;
then A39: dom gg = cod (id aa) ;
reconsider gg = gg as Morphism of aa,bb by A37, A38, CAT_1:4;
A40: the Target of C . ii = aa by A29
.= cod g by A36, CAT_1:5
.= the Source of C . g ;
then cod g = dom ii ;
then [ii,g] in dom the Comp of (C opp) by A1;
hence ii (*) g = (~ the Comp of C) . (ii,g) by CAT_1:def 1
.= the Comp of C . (g,ii) by A40, A3
.= gg (*) (id aa) by A39, CAT_1:16
.= g by A38, CAT_1:22 ;
:: thesis: verum