let C be category; :: thesis: AllIso (AllCoretr C) = AllIso C

A1: AllIso (AllCoretr C) is non empty transitive SubCatStr of C by ALTCAT_2:21;

A2: the carrier of (AllIso (AllCoretr C)) = the carrier of (AllCoretr C) by Def5;

A3: the carrier of (AllIso C) = the carrier of C by Def5;

A4: the carrier of (AllCoretr C) = the carrier of C by Def4;

A5: AllIso C is non empty subcategory of AllCoretr C by Th42;

then AllIso (AllCoretr C) is SubCatStr of AllIso C by A2, A3, A4, A1, ALTCAT_2:24;

hence AllIso (AllCoretr C) = AllIso C by A2, A3, A4, A6, ALTCAT_2:25, PBOOLE:3; :: thesis: verum

A1: AllIso (AllCoretr C) is non empty transitive SubCatStr of C by ALTCAT_2:21;

A2: the carrier of (AllIso (AllCoretr C)) = the carrier of (AllCoretr C) by Def5;

A3: the carrier of (AllIso C) = the carrier of C by Def5;

A4: the carrier of (AllCoretr C) = the carrier of C by Def4;

A5: AllIso C is non empty subcategory of AllCoretr C by Th42;

A6: now :: thesis: for i being object st i in [: the carrier of C, the carrier of C:] holds

the Arrows of (AllIso (AllCoretr C)) . i = the Arrows of (AllIso C) . i

then
the Arrows of (AllIso (AllCoretr C)) = the Arrows of (AllIso C)
by A2, A3, A4, PBOOLE:3;the Arrows of (AllIso (AllCoretr C)) . i = the Arrows of (AllIso C) . i

let i be object ; :: 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 A7: i in [: the carrier of C, the carrier of C:] ; :: thesis: the Arrows of (AllIso (AllCoretr C)) . i = the Arrows of (AllIso C) . i

then 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 (AllCoretr C) by A8, Def4;

thus the Arrows of (AllIso (AllCoretr C)) . i = the Arrows of (AllIso C) . i :: thesis: verum

end;assume A7: i in [: the carrier of C, the carrier of C:] ; :: thesis: the Arrows of (AllIso (AllCoretr C)) . i = the Arrows of (AllIso C) . i

then 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 (AllCoretr C) by A8, Def4;

thus the Arrows of (AllIso (AllCoretr C)) . i = the Arrows of (AllIso C) . i :: thesis: verum

proof

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)) . i

A16: <^p2,p1^> c= <^o2,o1^> by A5, ALTCAT_2:31;

let n be object ; :: 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 A17: n in the Arrows of (AllIso C) . i ; :: thesis: n in the Arrows of (AllIso (AllCoretr C)) . i

reconsider n2 = n as Morphism of p1,p2 by A9, A17;

the Arrows of (AllIso C) cc= the Arrows of (AllCoretr C) by A5, ALTCAT_2:def 11;

then A18: the Arrows of (AllIso C) . i c= the Arrows of (AllCoretr 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 (AllCoretr C)) . (o1,o2) by A9, A17, A18, A19, A16, Def5;

hence n in the Arrows of (AllIso (AllCoretr C)) . i by A9; :: thesis: verum

end;proof

reconsider p1 = o1, p2 = o2 as Object of (AllIso C) by A4, Def5;
reconsider r1 = o1, r2 = o2 as Object of C by Def4;

reconsider q1 = o1, q2 = o2 as Object of (AllIso (AllCoretr C)) by Def5;

A10: <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;

let n be object ; :: 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 A11: n in the Arrows of (AllIso (AllCoretr C)) . i ; :: thesis: 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 (AllCoretr 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; :: thesis: verum

end;reconsider q1 = o1, q2 = o2 as Object of (AllIso (AllCoretr C)) by Def5;

A10: <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;

let n be object ; :: 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 A11: n in the Arrows of (AllIso (AllCoretr C)) . i ; :: thesis: 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 (AllCoretr 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; :: thesis: verum

A16: <^p2,p1^> c= <^o2,o1^> by A5, ALTCAT_2:31;

let n be object ; :: 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 A17: n in the Arrows of (AllIso C) . i ; :: thesis: n in the Arrows of (AllIso (AllCoretr C)) . i

reconsider n2 = n as Morphism of p1,p2 by A9, A17;

the Arrows of (AllIso C) cc= the Arrows of (AllCoretr C) by A5, ALTCAT_2:def 11;

then A18: the Arrows of (AllIso C) . i c= the Arrows of (AllCoretr 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 (AllCoretr C)) . (o1,o2) by A9, A17, A18, A19, A16, Def5;

hence n in the Arrows of (AllIso (AllCoretr C)) . i by A9; :: thesis: verum

then AllIso (AllCoretr C) is SubCatStr of AllIso C by A2, A3, A4, A1, ALTCAT_2:24;

hence AllIso (AllCoretr C) = AllIso C by A2, A3, A4, A6, ALTCAT_2:25, PBOOLE:3; :: thesis: verum