set M = Maps V;
set d = fDom V;
set c = fCod V;
set p = fComp V;
reconsider C = CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #) as non empty non void CatStr ;
A1: C is Category-like
proof
let ff, gg be Morphism of C; :: according to CAT_1:def 6 :: thesis: ( ( not [gg,ff] in proj1 the Comp of C or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of C ) )
reconsider f = ff, g = gg as Element of Maps V ;
( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def9, Def10;
hence ( ( not [gg,ff] in proj1 the Comp of C or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of C ) ) by Def11; :: thesis: verum
end;
A2: C is transitive
proof
let ff, gg be Morphism of C; :: according to CAT_1:def 7 :: thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
assume A3: dom gg = cod ff ; :: thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )
[gg,ff] in dom the Comp of C by A3, A1;
then A4: the Comp of C . (gg,ff) = gg (*) ff by CAT_1:def 1;
reconsider f = ff, g = gg as Element of Maps V ;
A5: ( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def9, Def10;
then A6: (fComp V) . [g,f] = g * f by A3, Def11;
A7: ( (fDom V) . f = dom f & (fCod V) . g = cod g ) by Def9, Def10;
( dom (g * f) = dom f & cod (g * f) = cod g ) by A3, A5, Th12;
hence ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A6, A7, Def9, Def10, A4; :: thesis: verum
end;
A8: C is associative
proof
let ff, gg, hh be Morphism of C; :: 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 )
assume that
A9: dom hh = cod gg and
A10: dom gg = cod ff ; :: thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff
reconsider f = ff, g = gg, h = hh as Element of Maps V ;
A11: ( dom h = (fDom V) . h & cod g = (fCod V) . g ) by Def9, Def10;
then A12: dom (h * g) = dom g by A9, Th12;
A13: ( dom g = (fDom V) . g & cod f = (fCod V) . f ) by Def9, Def10;
then A14: cod (g * f) = dom h by A9, A10, A11, Th12;
[hh,gg] in dom the Comp of C by A9, A1;
then A15: hh (*) gg = the Comp of C . (hh,gg) by CAT_1:def 1;
dom (hh (*) gg) = dom gg by A2, A9;
then A16: [(hh (*) gg),ff] in dom the Comp of C by A1, A10;
[gg,ff] in dom the Comp of C by A10, A1;
then A17: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:def 1;
cod (gg (*) ff) = cod gg by A2, A10;
then [hh,(gg (*) ff)] in dom the Comp of C by A1, A9;
hence hh (*) (gg (*) ff) = the Comp of C . (hh,( the Comp of C . (gg,ff))) by A17, CAT_1:def 1
.= (fComp V) . [h,(g * f)] by A10, A13, Def11
.= h * (g * f) by A14, Def11
.= (h * g) * f by A9, A10, A11, A13, Th13
.= (fComp V) . [(h * g),f] by A10, A13, A12, Def11
.= the Comp of C . (( the Comp of C . (hh,gg)),ff) by A9, A11, Def11
.= (hh (*) gg) (*) ff by A16, A15, CAT_1:def 1 ;
:: thesis: verum
end;
A18: C is reflexive
proof
let a be Element of C; :: according to CAT_1:def 9 :: thesis: not Hom (a,a) = {}
reconsider aa = a as Element of V ;
reconsider ii = id$ aa as Morphism of C ;
A19: cod ii = cod (id$ aa) by Def10
.= a ;
dom ii = dom (id$ aa) by Def9
.= a ;
then ii in Hom (a,a) by A19;
hence Hom (a,a) <> {} ; :: thesis: verum
end;
C is with_identities
proof
let a be Element of C; :: according to CAT_1:def 10 :: thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of C 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 V ;
reconsider ii = id$ aa as Morphism of C ;
A20: cod ii = cod (id$ aa) by Def10
.= a ;
A21: dom ii = dom (id$ aa) by Def9
.= a ;
then reconsider ii = ii as Morphism of a,a by A20, CAT_1:4;
take ii ; :: thesis: for b1 being Element of the carrier of C 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; :: 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 ) )
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 A22: 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 Element of Maps V ;
A23: dom gg = dom g by Def9
.= aa by A22, CAT_1:5 ;
then A24: cod (id$ aa) = dom gg ;
dom g = a by A22, CAT_1:5;
then [g,ii] in dom (fComp V) by A20, A1;
hence g (*) ii = (fComp V) . (g,ii) by CAT_1:def 1
.= gg * (id$ aa) by A24, Def11
.= g by A23, Th14 ;
:: thesis: verum
end;
assume A25: 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 Element of Maps V ;
A26: cod gg = cod g by Def10
.= aa by A25, CAT_1:5 ;
then A27: dom (id$ aa) = cod gg ;
cod g = a by A25, CAT_1:5;
then [ii,g] in dom (fComp V) by A21, A1;
hence ii (*) g = (fComp V) . (ii,g) by CAT_1:def 1
.= (id$ aa) * gg by A27, Def11
.= g by A26, Th14 ;
:: thesis: verum
end;
hence ( Ens V is Category-like & Ens V is reflexive & Ens V is transitive & Ens V is associative & Ens V is with_identities ) by A1, A2, A8, A18; :: thesis: verum