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
A2:
C is transitive
proof
let ff,
gg be
Morphism of
C;
CAT_1:def 7 ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
assume A3:
dom gg = cod ff
;
( 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;
verum
end;
A8:
C is associative
proof
let ff,
gg,
hh be
Morphism of
C;
CAT_1:def 8 ( 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
;
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
;
verum
end;
A18:
C is reflexive
C is with_identities
proof
let a be
Element of
C;
CAT_1:def 10 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
;
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;
( ( 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 )
( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )proof
assume A22:
Hom (
a,
b)
<> {}
;
for g being Morphism of a,b holds g (*) ii = g
let g be
Morphism of
a,
b;
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
;
verum
end;
assume A25:
Hom (
b,
a)
<> {}
;
for b1 being Morphism of b,a holds ii (*) b1 = b1
let g be
Morphism of
b,
a;
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
;
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; verum