let C be category; AllIso (AllMono C) = AllIso C
A1:
AllIso (AllMono C) is non empty transitive SubCatStr of C
by ALTCAT_2:21;
A2:
the carrier of (AllIso (AllMono C)) = the carrier of (AllMono C)
by Def5;
A3:
the carrier of (AllIso C) = the carrier of C
by Def5;
A4:
the carrier of (AllMono C) = the carrier of C
by Def1;
( AllIso C is non empty subcategory of AllCoretr C & AllCoretr C is non empty subcategory of AllMono C )
by Th42, Th43;
then A5:
AllIso C is non empty subcategory of AllMono C
by Th36;
A6:
now for i being object st i in [: the carrier of C, the carrier of C:] holds
the Arrows of (AllIso (AllMono C)) . i = the Arrows of (AllIso C) . ilet i be
object ;
( i in [: the carrier of C, the carrier of C:] implies the Arrows of (AllIso (AllMono C)) . i = the Arrows of (AllIso C) . i )assume A7:
i in [: the carrier of C, the carrier of C:]
;
the Arrows of (AllIso (AllMono C)) . i = the Arrows of (AllIso C) . ithen consider o1,
o2 being
object such that A8:
(
o1 in the
carrier of
C &
o2 in the
carrier of
C )
and A9:
i = [o1,o2]
by ZFMISC_1:84;
reconsider o1 =
o1,
o2 =
o2 as
Object of
(AllMono C) by A8, Def1;
thus
the
Arrows of
(AllIso (AllMono C)) . i = the
Arrows of
(AllIso C) . i
verumproof
thus
the
Arrows of
(AllIso (AllMono C)) . i c= the
Arrows of
(AllIso C) . i
XBOOLE_0:def 10 the Arrows of (AllIso C) . i c= the Arrows of (AllIso (AllMono C)) . iproof
reconsider r1 =
o1,
r2 =
o2 as
Object of
C by Def1;
reconsider q1 =
o1,
q2 =
o2 as
Object of
(AllIso (AllMono C)) by Def5;
A10:
<^q2,q1^> c= <^o2,o1^>
by ALTCAT_2:31;
let n be
object ;
TARSKI:def 3 ( not n in the Arrows of (AllIso (AllMono C)) . i or n in the Arrows of (AllIso C) . i )
assume A11:
n in the
Arrows of
(AllIso (AllMono C)) . i
;
n in the Arrows of (AllIso C) . i
n in <^q1,q2^>
by A9, A11;
then A12:
<^o2,o1^> <> {}
by A10, Th52;
then A13:
<^r2,r1^> <> {}
by ALTCAT_2:31, XBOOLE_1:3;
A14:
<^q1,q2^> c= <^o1,o2^>
by ALTCAT_2:31;
then reconsider n2 =
n as
Morphism of
o1,
o2 by A9, A11;
A15:
<^r1,r2^> <> {}
by A9, A11, A14, ALTCAT_2:31, XBOOLE_1:3;
<^o1,o2^> c= <^r1,r2^>
by ALTCAT_2:31;
then
<^q1,q2^> c= <^r1,r2^>
by A14;
then reconsider n1 =
n as
Morphism of
r1,
r2 by A9, A11;
n in the
Arrows of
(AllIso (AllMono C)) . (
q1,
q2)
by A9, A11;
then
n2 is
iso
by Def5;
then
n1 is
iso
by A9, A11, A14, A12, Th40;
then
n in the
Arrows of
(AllIso C) . (
r1,
r2)
by A15, A13, Def5;
hence
n in the
Arrows of
(AllIso C) . i
by A9;
verum
end;
reconsider p1 =
o1,
p2 =
o2 as
Object of
(AllIso C) by A4, Def5;
A16:
<^p2,p1^> c= <^o2,o1^>
by A5, ALTCAT_2:31;
let n be
object ;
TARSKI:def 3 ( not n in the Arrows of (AllIso C) . i or n in the Arrows of (AllIso (AllMono C)) . i )
assume A17:
n in the
Arrows of
(AllIso C) . i
;
n in the Arrows of (AllIso (AllMono C)) . i
reconsider n2 =
n as
Morphism of
p1,
p2 by A9, A17;
the
Arrows of
(AllIso C) cc= the
Arrows of
(AllMono C)
by A5, ALTCAT_2:def 11;
then A18:
the
Arrows of
(AllIso C) . i c= the
Arrows of
(AllMono C) . i
by A3, A7;
then reconsider n1 =
n as
Morphism of
o1,
o2 by A9, A17;
A19:
n2 " in <^p2,p1^>
by A9, A17, Th52;
n2 is
iso
by A9, A17, Th52;
then
n1 is
iso
by A5, A9, A17, A19, Th40;
then
n in the
Arrows of
(AllIso (AllMono C)) . (
o1,
o2)
by A9, A17, A18, A19, A16, Def5;
hence
n in the
Arrows of
(AllIso (AllMono C)) . i
by A9;
verum
end; end;
then
the Arrows of (AllIso (AllMono C)) = the Arrows of (AllIso C)
by A2, A3, A4, PBOOLE:3;
then
AllIso (AllMono C) is SubCatStr of AllIso C
by A2, A3, A4, A1, ALTCAT_2:24;
hence
AllIso (AllMono C) = AllIso C
by A2, A3, A4, A6, ALTCAT_2:25, PBOOLE:3; verum