let C be category; :: thesis: AllIso (AllEpi C) = AllIso C
A1:
the carrier of (AllIso (AllEpi C)) = the carrier of (AllEpi C)
by Def5;
A2:
the carrier of (AllIso C) = the carrier of C
by Def5;
A3:
the carrier of (AllEpi C) = the carrier of C
by Def2;
A4:
AllIso C is non empty subcategory of AllRetr C
by Th41;
AllRetr C is non empty subcategory of AllEpi C
by Th44;
then A5:
AllIso C is non empty subcategory of AllEpi C
by A4, Th36;
B18:
now let i be
set ;
:: thesis: ( i in [:the carrier of C,the carrier of C:] implies the Arrows of (AllIso (AllEpi C)) . i = the Arrows of (AllIso C) . i )assume A6:
i in [:the carrier of C,the carrier of C:]
;
:: thesis: the Arrows of (AllIso (AllEpi C)) . i = the Arrows of (AllIso C) . ithen consider o1,
o2 being
set such that A7:
(
o1 in the
carrier of
C &
o2 in the
carrier of
C &
i = [o1,o2] )
by ZFMISC_1:103;
reconsider o1 =
o1,
o2 =
o2 as
object of
(AllEpi C) by A7, Def2;
thus
the
Arrows of
(AllIso (AllEpi C)) . i = the
Arrows of
(AllIso C) . i
:: thesis: verumproof
thus
the
Arrows of
(AllIso (AllEpi C)) . i c= the
Arrows of
(AllIso C) . i
:: according to XBOOLE_0:def 10 :: thesis: the Arrows of (AllIso C) . i c= the Arrows of (AllIso (AllEpi C)) . iproof
let n be
set ;
:: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of (AllIso (AllEpi C)) . i or n in the Arrows of (AllIso C) . i )
assume A8:
n in the
Arrows of
(AllIso (AllEpi C)) . i
;
:: thesis: n in the Arrows of (AllIso C) . i
reconsider q1 =
o1,
q2 =
o2 as
object of
(AllIso (AllEpi C)) by Def5;
A9:
n in the
Arrows of
(AllIso (AllEpi C)) . q1,
q2
by A7, A8;
A10:
n in <^q1,q2^>
by A7, A8;
A11:
(
<^q1,q2^> c= <^o1,o2^> &
<^q2,q1^> c= <^o2,o1^> )
by ALTCAT_2:32;
then reconsider n2 =
n as
Morphism of
o1,
o2 by A7, A8;
reconsider r1 =
o1,
r2 =
o2 as
object of
C by Def2;
(
<^o1,o2^> c= <^r1,r2^> &
<^o2,o1^> c= <^r2,r1^> )
by ALTCAT_2:32;
then
<^q1,q2^> c= <^r1,r2^>
by A11, XBOOLE_1:1;
then reconsider n1 =
n as
Morphism of
r1,
r2 by A7, A8;
<^q2,q1^> <> {}
by A10, Th52;
then A12:
(
<^o1,o2^> <> {} &
<^o2,o1^> <> {} )
by A7, A8, A11;
then A13:
(
<^r1,r2^> <> {} &
<^r2,r1^> <> {} )
by ALTCAT_2:32, XBOOLE_1:3;
n2 is
iso
by A9, Def5;
then
n1 is
iso
by A12, Th40;
then
n in the
Arrows of
(AllIso C) . r1,
r2
by A13, Def5;
hence
n in the
Arrows of
(AllIso C) . i
by A7;
:: thesis: verum
end;
let n be
set ;
:: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of (AllIso C) . i or n in the Arrows of (AllIso (AllEpi C)) . i )
assume A14:
n in the
Arrows of
(AllIso C) . i
;
:: thesis: n in the Arrows of (AllIso (AllEpi C)) . i
reconsider p1 =
o1,
p2 =
o2 as
object of
(AllIso C) by A3, Def5;
the
Arrows of
(AllIso C) cc= the
Arrows of
(AllEpi C)
by A5, ALTCAT_2:def 11;
then A15:
the
Arrows of
(AllIso C) . i c= the
Arrows of
(AllEpi C) . i
by A2, A6, ALTCAT_2:def 2;
then reconsider n1 =
n as
Morphism of
o1,
o2 by A7, A14;
reconsider n2 =
n as
Morphism of
p1,
p2 by A7, A14;
A16:
n2 " in <^p2,p1^>
by A7, A14, Th52;
A17:
<^p2,p1^> c= <^o2,o1^>
by A5, ALTCAT_2:32;
n2 is
iso
by A7, A14, Th52;
then
n1 is
iso
by A5, A7, A14, A16, Th40;
then
n in the
Arrows of
(AllIso (AllEpi C)) . o1,
o2
by A7, A14, A15, A16, A17, Def5;
hence
n in the
Arrows of
(AllIso (AllEpi C)) . i
by A7;
:: thesis: verum
end; end;
then A18:
the Arrows of (AllIso (AllEpi C)) = the Arrows of (AllIso C)
by A1, A2, A3, PBOOLE:3;
AllIso (AllEpi C) is non empty transitive SubCatStr of C
by ALTCAT_2:22;
then
AllIso (AllEpi C) is SubCatStr of AllIso C
by A1, A2, A3, A18, ALTCAT_2:25;
hence
AllIso (AllEpi C) = AllIso C
by A1, A2, A3, B18, ALTCAT_2:26, PBOOLE:3; :: thesis: verum