set C = GroupCat UN;
thus
GroupCat UN is reflexive
GroupCat UN is Category-like proof
let a be
Element of
(GroupCat UN);
CAT_1:def 9 not Hom (a,a) = {}
reconsider G =
a as
Element of
GroupObjects UN ;
consider x being
object such that
x in UN
and A1:
GO x,
G
by Def22;
set ii =
ID G;
consider x1,
x2,
x3,
x4 being
set such that
x = [x1,x2,x3,x4]
and A2:
ex
H being
strict AddGroup st
(
G = H &
x1 = the
carrier of
H &
x2 = the
addF of
H &
x3 = comp H &
x4 = 0. H )
by A1;
reconsider G =
G as
strict Element of
GroupObjects UN by A2;
reconsider ii =
ID G as
Morphism of
(GroupCat UN) ;
reconsider ia =
ii as
GroupMorphismStr ;
A3:
dom ii =
dom ia
by Def25
.=
a
;
cod ii =
cod ia
by Def26
.=
a
;
then
ii in Hom (
a,
a)
by A3;
hence
Hom (
a,
a)
<> {}
;
verum
end;
let f, g be Morphism of (GroupCat UN); CAT_1:def 6 ( ( not [g,f] in proj1 the Comp of (GroupCat UN) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of (GroupCat UN) ) )
reconsider ff = f, gg = g as Element of Morphs (GroupObjects UN) ;
thus
( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f )
by Th35; verum