set C = TolCat X;
set M = MapsT X;
set d = fDom X;
set c = fCod X;
set p = fComp X;
thus P1:
TolCat X is Category-like
( TolCat X is transitive & TolCat X is associative & TolCat X is reflexive )
thus P2:
TolCat X is transitive
( TolCat X is associative & TolCat X is reflexive )proof
let ff,
gg be
Morphism of
(TolCat X);
CAT_1:def 7 ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
assume A1:
dom gg = cod ff
;
( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )
[gg,ff] in dom the
Comp of
(TolCat X)
by A1, P1, CAT_1:def 6;
then U:
the
Comp of
(TolCat X) . (
gg,
ff)
= gg (*) ff
by CAT_1:def 1;
reconsider f =
ff,
g =
gg as
Element of
MapsT X ;
A2:
(
(fDom X) . g = dom g &
(fCod X) . f = cod f )
by Def25, Def26;
then A3:
(fComp X) . [g,f] = g * f
by A1, Def27;
A4:
(
(fDom X) . f = dom f &
(fCod X) . g = cod g )
by Def25, Def26;
(
dom (g * f) = dom f &
cod (g * f) = cod g )
by A1, A2, Th44;
hence
(
dom (gg (*) ff) = dom ff &
cod (gg (*) ff) = cod gg )
by A3, A4, Def25, Def26, U;
verum
end;
thus
TolCat X is associative
TolCat X is reflexive proof
let ff,
gg,
hh be
Morphism of
(TolCat X);
CAT_1:def 8 ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff )
assume that A5:
dom hh = cod gg
and A6:
dom gg = cod ff
;
hh (*) (gg (*) ff) = (hh (*) gg) (*) ff
reconsider f =
ff,
g =
gg,
h =
hh as
Element of
MapsT X ;
A7:
(
dom h = (fDom X) . h &
cod g = (fCod X) . g )
by Def25, Def26;
then A8:
dom (h * g) = dom g
by A5, Th44;
A9:
(
dom g = (fDom X) . g &
cod f = (fCod X) . f )
by Def25, Def26;
then A10:
cod (g * f) = dom h
by A5, A6, A7, Th44;
[hh,gg] in dom the
Comp of
(TolCat X)
by A5, P1, CAT_1:def 6;
then X2:
hh (*) gg = the
Comp of
(TolCat X) . (
hh,
gg)
by CAT_1:def 1;
[gg,ff] in dom the
Comp of
(TolCat X)
by A6, P1, CAT_1:def 6;
then X1:
gg (*) ff = the
Comp of
(TolCat X) . (
gg,
ff)
by CAT_1:def 1;
dom (hh (*) gg) = dom gg
by P2, CAT_1:def 7, A5;
then X3:
[(hh (*) gg),ff] in dom the
Comp of
(TolCat X)
by P1, CAT_1:def 6, A6;
cod (gg (*) ff) = cod gg
by P2, CAT_1:def 7, A6;
then
[hh,(gg (*) ff)] in dom the
Comp of
(TolCat X)
by P1, CAT_1:def 6, A5;
hence hh (*) (gg (*) ff) =
the
Comp of
(TolCat X) . (
hh,
( the Comp of (TolCat X) . (gg,ff)))
by X1, CAT_1:def 1
.=
(fComp X) . [h,(g * f)]
by A6, A9, Def27
.=
h * (g * f)
by A10, Def27
.=
(h * g) * f
by A5, A6, A7, A9, Th45
.=
(fComp X) . [(h * g),f]
by A6, A9, A8, Def27
.=
the
Comp of
(TolCat X) . (
( the Comp of (TolCat X) . (hh,gg)),
ff)
by A5, A7, Def27
.=
(hh (*) gg) (*) ff
by X2, X3, CAT_1:def 1
;
verum
end;
let a be Object of (TolCat X); CAT_1:def 9 not Hom (a,a) = {}
reconsider aa = a as Element of TOL X ;
reconsider ii = id$ aa as Morphism of (TolCat X) ;
A12: cod ii =
cod (id$ aa)
by Def26
.=
aa
by Th46
;
dom ii =
dom (id$ aa)
by Def25
.=
aa
by Th46
;
then
id$ aa in Hom (a,a)
by A12;
hence
Hom (a,a) <> {}
; verum