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