let C be category; :: thesis: AllIso C is non empty subcategory of AllRetr C

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

then A1: the carrier of (AllIso C) c= the carrier of (AllRetr C) by Def3;

the Arrows of (AllIso C) cc= the Arrows of (AllRetr C)

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

then A1: the carrier of (AllIso C) c= the carrier of (AllRetr C) by Def3;

the Arrows of (AllIso C) cc= the Arrows of (AllRetr C)

proof

then reconsider A = AllIso C as non empty with_units SubCatStr of AllRetr C by A1, ALTCAT_2:24;
thus
[: the carrier of (AllIso C), the carrier of (AllIso C):] c= [: the carrier of (AllRetr C), the carrier of (AllRetr C):]
by A1, ZFMISC_1:96; :: according to ALTCAT_2:def 2 :: thesis: for b_{1} being set holds

( not b_{1} in [: the carrier of (AllIso C), the carrier of (AllIso C):] or the Arrows of (AllIso C) . b_{1} c= the Arrows of (AllRetr C) . b_{1} )

let i be set ; :: thesis: ( not i in [: the carrier of (AllIso C), the carrier of (AllIso C):] or the Arrows of (AllIso C) . i c= the Arrows of (AllRetr C) . i )

assume A2: i in [: the carrier of (AllIso C), the carrier of (AllIso C):] ; :: thesis: the Arrows of (AllIso C) . i c= the Arrows of (AllRetr C) . i

then consider o1, o2 being object such that

A3: ( o1 in the carrier of (AllIso C) & o2 in the carrier of (AllIso C) ) and

A4: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of C by A3, Def5;

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in the Arrows of (AllIso C) . i or m in the Arrows of (AllRetr C) . i )

assume A5: m in the Arrows of (AllIso C) . i ; :: thesis: m in the Arrows of (AllRetr C) . i

the Arrows of (AllIso C) cc= the Arrows of C by Def5;

then the Arrows of (AllIso 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 (AllIso C) . (o1,o2) by A4, A5;

then m1 is iso by Def5;

then A6: m1 is retraction by ALTCAT_3:5;

m1 in the Arrows of (AllIso C) . (o1,o2) by A4, A5;

then ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by Def5;

then m in the Arrows of (AllRetr C) . (o1,o2) by A6, Def3;

hence m in the Arrows of (AllRetr C) . i by A4; :: thesis: verum

end;( not b

let i be set ; :: thesis: ( not i in [: the carrier of (AllIso C), the carrier of (AllIso C):] or the Arrows of (AllIso C) . i c= the Arrows of (AllRetr C) . i )

assume A2: i in [: the carrier of (AllIso C), the carrier of (AllIso C):] ; :: thesis: the Arrows of (AllIso C) . i c= the Arrows of (AllRetr C) . i

then consider o1, o2 being object such that

A3: ( o1 in the carrier of (AllIso C) & o2 in the carrier of (AllIso C) ) and

A4: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of C by A3, Def5;

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in the Arrows of (AllIso C) . i or m in the Arrows of (AllRetr C) . i )

assume A5: m in the Arrows of (AllIso C) . i ; :: thesis: m in the Arrows of (AllRetr C) . i

the Arrows of (AllIso C) cc= the Arrows of C by Def5;

then the Arrows of (AllIso 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 (AllIso C) . (o1,o2) by A4, A5;

then m1 is iso by Def5;

then A6: m1 is retraction by ALTCAT_3:5;

m1 in the Arrows of (AllIso C) . (o1,o2) by A4, A5;

then ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by Def5;

then m in the Arrows of (AllRetr C) . (o1,o2) by A6, Def3;

hence m in the Arrows of (AllRetr C) . i by A4; :: thesis: verum

now :: thesis: for o being Object of A

for o1 being Object of (AllRetr C) st o = o1 holds

idm o1 in <^o,o^>

hence
AllIso C is non empty subcategory of AllRetr C
by ALTCAT_2:def 14; :: thesis: verumfor o1 being Object of (AllRetr C) st o = o1 holds

idm o1 in <^o,o^>

let o be Object of A; :: thesis: for o1 being Object of (AllRetr C) st o = o1 holds

idm o1 in <^o,o^>

let o1 be Object of (AllRetr C); :: thesis: ( o = o1 implies idm o1 in <^o,o^> )

assume A7: o = o1 ; :: thesis: idm o1 in <^o,o^>

reconsider oo = o as Object of C by Def5;

idm o = idm oo by ALTCAT_2:34

.= idm o1 by A7, ALTCAT_2:34 ;

hence idm o1 in <^o,o^> ; :: thesis: verum

end;idm o1 in <^o,o^>

let o1 be Object of (AllRetr C); :: thesis: ( o = o1 implies idm o1 in <^o,o^> )

assume A7: o = o1 ; :: thesis: idm o1 in <^o,o^>

reconsider oo = o as Object of C by Def5;

idm o = idm oo by ALTCAT_2:34

.= idm o1 by A7, ALTCAT_2:34 ;

hence idm o1 in <^o,o^> ; :: thesis: verum