let C be category; AllRetr C is non empty subcategory of AllEpi C
the carrier of (AllRetr C) = the carrier of C
by Def3;
then A1:
the carrier of (AllRetr C) c= the carrier of (AllEpi C)
by Def2;
the Arrows of (AllRetr C) cc= the Arrows of (AllEpi C)
proof
thus
[: the carrier of (AllRetr C), the carrier of (AllRetr C):] c= [: the carrier of (AllEpi C), the carrier of (AllEpi C):]
by A1, ZFMISC_1:96;
ALTCAT_2:def 2 for b1 being set holds
( not b1 in [: the carrier of (AllRetr C), the carrier of (AllRetr C):] or the Arrows of (AllRetr C) . b1 c= the Arrows of (AllEpi C) . b1 )
let i be
set ;
( not i in [: the carrier of (AllRetr C), the carrier of (AllRetr C):] or the Arrows of (AllRetr C) . i c= the Arrows of (AllEpi C) . i )
assume A2:
i in [: the carrier of (AllRetr C), the carrier of (AllRetr C):]
;
the Arrows of (AllRetr C) . i c= the Arrows of (AllEpi C) . i
then consider o1,
o2 being
object such that A3:
(
o1 in the
carrier of
(AllRetr C) &
o2 in the
carrier of
(AllRetr C) )
and A4:
i = [o1,o2]
by ZFMISC_1:84;
reconsider o1 =
o1,
o2 =
o2 as
Object of
C by A3, Def3;
let m be
object ;
TARSKI:def 3 ( not m in the Arrows of (AllRetr C) . i or m in the Arrows of (AllEpi C) . i )
assume A5:
m in the
Arrows of
(AllRetr C) . i
;
m in the Arrows of (AllEpi C) . i
the
Arrows of
(AllRetr C) cc= the
Arrows of
C
by Def3;
then
the
Arrows of
(AllRetr C) . [o1,o2] c= the
Arrows of
C . (
o1,
o2)
by A2, A4;
then reconsider m1 =
m as
Morphism of
o1,
o2 by A4, A5;
m in the
Arrows of
(AllRetr C) . (
o1,
o2)
by A4, A5;
then A6:
m1 is
retraction
by Def3;
A7:
m1 in the
Arrows of
(AllRetr C) . (
o1,
o2)
by A4, A5;
then A8:
<^o1,o2^> <> {}
by Def3;
<^o2,o1^> <> {}
by A7, Def3;
then
m1 is
epi
by A8, A6, ALTCAT_3:15;
then
m in the
Arrows of
(AllEpi C) . (
o1,
o2)
by A8, Def2;
hence
m in the
Arrows of
(AllEpi C) . i
by A4;
verum
end;
then reconsider A = AllRetr C as non empty with_units SubCatStr of AllEpi C by A1, ALTCAT_2:24;
hence
AllRetr C is non empty subcategory of AllEpi C
by ALTCAT_2:def 14; verum