### The Mizar article:

### On the Categories Without Uniqueness of \bf cod and \bf dom . Some Properties of the Morphisms and the Functors

**by****Artur Kornilowicz**

- Received October 3, 1997
Copyright (c) 1997 Association of Mizar Users

- MML identifier: ALTCAT_4
- [ MML identifier index ]

environ vocabulary ALTCAT_1, CAT_1, RELAT_1, BOOLE, ALTCAT_3, CAT_3, RELAT_2, FUNCTOR0, FUNCT_1, SGRAPH1, PRALG_1, MSUALG_3, PBOOLE, MSUALG_6, ALTCAT_2, ALTCAT_4; notation TARSKI, XBOOLE_0, ZFMISC_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, MULTOP_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_3, ALTCAT_1, ALTCAT_2, ALTCAT_3, FUNCTOR0; constructors ALTCAT_3, FUNCTOR0, MCART_1; clusters FUNCTOR0, ALTCAT_2, MSUALG_1, PRALG_1, FUNCTOR2, RELSET_1, SUBSET_1, ALTCAT_1, STRUCT_0, XBOOLE_0; requirements SUBSET, BOOLE; definitions ALTCAT_1, ALTCAT_2, ALTCAT_3, FUNCTOR0, MSUALG_1, MSUALG_3, STRUCT_0, TARSKI, FUNCT_2, XBOOLE_0; theorems ALTCAT_1, ALTCAT_2, ALTCAT_3, BINOP_1, FUNCT_1, FUNCT_2, FUNCTOR0, MCART_1, MULTOP_1, FUNCTOR1, FUNCTOR2, MSUALG_3, PBOOLE, RELAT_1, ZFMISC_1, XBOOLE_0, XBOOLE_1; schemes MSUALG_1, XBOOLE_0; begin :: Preliminaries reserve C for category, o1, o2, o3 for object of C; definition let C be with_units (non empty AltCatStr), o be object of C; cluster <^o,o^> -> non empty; coherence by ALTCAT_1:23; end; theorem Th1: for v being Morphism of o1, o2, u being Morphism of o1, o3 for f being Morphism of o2, o3 st u = f * v & f" * f = idm o2 & <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} holds v = f" * u proof let v be Morphism of o1, o2, u be Morphism of o1, o3, f be Morphism of o2, o3 such that A1: u = f * v and A2: f" * f = idm o2 and A3: <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {}; thus f" * u = f" * f * v by A1,A3,ALTCAT_1:25 .= v by A2,A3,ALTCAT_1:24; end; theorem Th2: for v being Morphism of o2, o3, u being Morphism of o1, o3 for f being Morphism of o1, o2 st u = v * f & f * f" = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} holds v = u * f" proof let v be Morphism of o2, o3, u be Morphism of o1, o3, f be Morphism of o1, o2 such that A1: u = v * f and A2: f * f" = idm o2 and A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {}; thus u * f" = v * (f * f") by A1,A3,ALTCAT_1:25 .= v by A2,A3,ALTCAT_1:def 19; end; theorem Th3: for m being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso holds m" is iso proof let m be Morphism of o1, o2 such that A1: <^o1,o2^> <> {} & <^o2,o1^> <> {}; assume m is iso; then A2: m is retraction coretraction by ALTCAT_3:5; hence m"*(m")" = m" * m by A1,ALTCAT_3:3 .= idm o1 by A1,A2,ALTCAT_3:2; thus (m")"*m" = m * m" by A1,A2,ALTCAT_3:3 .= idm o2 by A1,A2,ALTCAT_3:2; end; theorem Th4: for C being with_units (non empty AltCatStr), o being object of C holds idm o is epi mono proof let C be with_units (non empty AltCatStr), o be object of C; thus idm o is epi proof let o1 be object of C such that A1: <^o,o1^> <> {}; let B, C be Morphism of o, o1 such that A2: B * idm o = C * idm o; thus B = B * idm o by A1,ALTCAT_1:def 19 .= C by A1,A2,ALTCAT_1:def 19; end; let o1 be object of C such that A3: <^o1,o^> <> {}; let B, C be Morphism of o1, o such that A4: idm o * B = idm o * C; thus B = idm o * B by A3,ALTCAT_1:24 .= C by A3,A4,ALTCAT_1:24; end; definition let C be with_units (non empty AltCatStr), o be object of C; cluster idm o -> epi mono retraction coretraction; coherence by Th4,ALTCAT_3:1; end; definition let C be category, o be object of C; cluster idm o -> iso; coherence by ALTCAT_3:6; end; theorem for f being Morphism of o1, o2, g, h being Morphism of o2, o1 st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds g = h proof let f be Morphism of o1, o2, g, h be Morphism of o2, o1 such that A1: h * f = idm o1 and A2: f * g = idm o2 and A3: <^o1,o2^> <> {} & <^o2,o1^> <> {}; thus g = h * f * g by A1,A3,ALTCAT_1:24 .= h * idm o2 by A2,A3,ALTCAT_1:25 .= h by A3,ALTCAT_1:def 19; end; theorem (for o1, o2 being object of C, f being Morphism of o1, o2 holds f is coretraction) implies for a, b being object of C, g being Morphism of a, b st <^a,b^> <> {} & <^b,a^> <> {} holds g is iso proof assume A1: for o1, o2 being object of C, f being Morphism of o1, o2 holds f is coretraction; let a, b be object of C, g be Morphism of a, b such that A2: <^a,b^> <> {} & <^b,a^> <> {}; A3: g is coretraction by A1; g is retraction proof consider f be Morphism of b, a such that A4: f is_left_inverse_of g by A3,ALTCAT_3:def 3; take f; f is coretraction by A1; then A5: f is mono by A2,ALTCAT_3:16; f * (g * f) = f * g * f by A2,ALTCAT_1:25 .= idm a * f by A4,ALTCAT_3:def 1 .= f by A2,ALTCAT_1:24 .= f * idm b by A2,ALTCAT_1:def 19; hence g * f = idm b by A5,ALTCAT_3:def 7; end; hence g is iso by A2,A3,ALTCAT_3:6; end; begin :: Some properties of the initial and terminal objects theorem for m, m' being Morphism of o1, o2 st m is _zero & m' is _zero & ex O being object of C st O is _zero holds m = m' proof let m, m' be Morphism of o1, o2 such that A1: m is _zero and A2: m' is _zero; given O being object of C such that A3: O is _zero; consider a being Morphism of o1, O; consider b being Morphism of O, o2; consider n being Morphism of O, O; thus m = b * (n" * n) * a by A1,A3,ALTCAT_3:def 12 .= m' by A2,A3,ALTCAT_3:def 12; end; theorem for C being non empty AltCatStr, O, A being object of C for M being Morphism of O, A st O is terminal holds M is mono proof let C be non empty AltCatStr, O, A be object of C, M be Morphism of O, A such that A1: O is terminal; let o be object of C such that A2: <^o,O^> <> {}; let a, b be Morphism of o, O such that M * a = M * b; consider N being Morphism of o, O such that N in <^o,O^> and A3: for M1 being Morphism of o, O st M1 in <^o,O^> holds N = M1 by A1,ALTCAT_3:27; thus a = N by A2,A3 .= b by A2,A3; end; theorem for C being non empty AltCatStr, O, A being object of C for M being Morphism of A, O st O is initial holds M is epi proof let C be non empty AltCatStr, O, A be object of C, M be Morphism of A, O such that A1: O is initial; let o be object of C such that A2: <^O,o^> <> {}; let a, b be Morphism of O, o such that a * M = b * M; consider N being Morphism of O, o such that N in <^O,o^> and A3: for M1 being Morphism of O, o st M1 in <^O,o^> holds N = M1 by A1,ALTCAT_3:25; thus a = N by A2,A3 .= b by A2,A3; end; theorem o2 is terminal & o1, o2 are_iso implies o1 is terminal proof assume that A1: o2 is terminal and A2: o1, o2 are_iso; for o3 being object of C holds ex M being Morphism of o3, o1 st M in <^o3,o1^> & for v being Morphism of o3, o1 st v in <^o3,o1^> holds M = v proof let o3 be object of C; consider u being Morphism of o3, o2 such that A3: u in <^o3,o2^> and A4: for M1 being Morphism of o3, o2 st M1 in <^o3,o2^> holds u = M1 by A1,ALTCAT_3:27; consider f being Morphism of o1, o2 such that A5: f is iso by A2,ALTCAT_3:def 6; A6: f" * f = idm o1 by A5,ALTCAT_3:def 5; take f" * u; A7: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A2,ALTCAT_3:def 6; then A8: <^o3,o1^> <> {} by A3,ALTCAT_1:def 4; hence f" * u in <^o3,o1^>; let v be Morphism of o3, o1 such that v in <^o3,o1^>; f * v = u by A3,A4; hence f" * u = v by A6,A7,A8,Th1; end; hence o1 is terminal by ALTCAT_3:27; end; theorem o1 is initial & o1, o2 are_iso implies o2 is initial proof assume that A1: o1 is initial and A2: o1, o2 are_iso; for o3 being object of C holds ex M being Morphism of o2, o3 st M in <^o2,o3^> & for v being Morphism of o2, o3 st v in <^o2,o3^> holds M = v proof let o3 be object of C; consider u being Morphism of o1, o3 such that A3: u in <^o1,o3^> and A4: for M1 being Morphism of o1, o3 st M1 in <^o1,o3^> holds u = M1 by A1,ALTCAT_3:25; consider f being Morphism of o1, o2 such that A5: f is iso by A2,ALTCAT_3:def 6; A6: f * f" = idm o2 by A5,ALTCAT_3:def 5; take u * f"; A7: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A2,ALTCAT_3:def 6; then A8: <^o2,o3^> <> {} by A3,ALTCAT_1:def 4; hence u * f" in <^o2,o3^>; let v be Morphism of o2, o3 such that v in <^o2,o3^>; v * f = u by A3,A4; hence u * f" = v by A6,A7,A8,Th2; end; hence o2 is initial by ALTCAT_3:25; end; theorem o1 is initial & o2 is terminal & <^o2,o1^> <> {} implies o2 is initial & o1 is terminal proof assume that A1: o1 is initial and A2: o2 is terminal; assume <^o2,o1^> <> {}; then consider m being set such that A3: m in <^o2,o1^> by XBOOLE_0:def 1; reconsider m as Morphism of o2, o1 by A3; consider l being Morphism of o1, o2 such that A4: l in <^o1,o2^> and for M1 being Morphism of o1, o2 st M1 in <^o1,o2^> holds l = M1 by A1,ALTCAT_3:25; for o3 being object of C holds ex M being Morphism of o2, o3 st M in <^o2,o3^> & for M1 being Morphism of o2, o3 st M1 in <^o2,o3^> holds M = M1 proof let o3 be object of C; consider M being Morphism of o1, o3 such that A5: M in <^o1,o3^> & for M1 being Morphism of o1, o3 st M1 in <^o1,o3^> holds M = M1 by A1,ALTCAT_3:25; take M * m; <^o2,o3^> <> {} by A3,A5,ALTCAT_1:def 4; hence M * m in <^o2,o3^>; let M1 be Morphism of o2, o3 such that A6: M1 in <^o2,o3^>; consider i2 being Morphism of o2, o2 such that i2 in <^o2,o2^> and A7: for M1 being Morphism of o2, o2 st M1 in <^o2,o2^> holds i2 = M1 by A2,ALTCAT_3:27; thus M * m = M1 * l * m by A5 .= M1 * (l * m) by A3,A4,A6,ALTCAT_1:25 .= M1 * i2 by A7 .= M1 * idm o2 by A7 .= M1 by A6,ALTCAT_1:def 19; end; hence o2 is initial by ALTCAT_3:25; for o3 being object of C holds ex M being Morphism of o3, o1 st M in <^o3,o1^> & for M1 being Morphism of o3, o1 st M1 in <^o3,o1^> holds M = M1 proof let o3 be object of C; consider M being Morphism of o3, o2 such that A8: M in <^o3,o2^> & for M1 being Morphism of o3, o2 st M1 in <^o3,o2^> holds M = M1 by A2,ALTCAT_3:27; take m * M; <^o3,o1^> <> {} by A3,A8,ALTCAT_1:def 4; hence m * M in <^o3,o1^>; let M1 be Morphism of o3, o1 such that A9: M1 in <^o3,o1^>; consider i1 being Morphism of o1, o1 such that i1 in <^o1,o1^> and A10: for M1 being Morphism of o1, o1 st M1 in <^o1,o1^> holds i1 = M1 by A1,ALTCAT_3:25; thus m * M = m * (l * M1) by A8 .= m * l * M1 by A3,A4,A9,ALTCAT_1:25 .= i1 * M1 by A10 .= idm o1 * M1 by A10 .= M1 by A9,ALTCAT_1:24; end; hence o1 is terminal by ALTCAT_3:27; end; begin :: The properties of the functors theorem Th13: for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for a being object of A holds F.idm a = idm (F.a) proof let A, B be transitive with_units (non empty AltCatStr), F be contravariant Functor of A, B; let a be object of A; thus F.idm a = Morph-Map(F,a,a).idm a by FUNCTOR0:def 17 .= idm (F.a) by FUNCTOR0:def 21; end; theorem Th14: for C1, C2 being non empty AltCatStr for F being Contravariant FunctorStr over C1, C2 holds F is full iff for o1, o2 being object of C1 holds Morph-Map(F,o2,o1) is onto proof let C1, C2 be non empty AltCatStr, F be Contravariant FunctorStr over C1, C2; set I = [:the carrier of C1, the carrier of C1:]; hereby assume A1: F is full; let o1, o2 be object of C1; thus Morph-Map(F,o2,o1) is onto proof consider f being ManySortedFunction of the Arrows of C1, (the Arrows of C2)*the ObjectMap of F such that A2: f = the MorphMap of F & f is "onto" by A1,FUNCTOR0:def 33; A3: [o2,o1] in I by ZFMISC_1:106; A4: (the MorphMap of F).[o2,o1] = (the MorphMap of F).(o2,o1) by BINOP_1:def 1; A5: [o2,o1] in dom(the ObjectMap of F) by A3,FUNCT_2:def 1; rng(f.[o2,o1]) = ((the Arrows of C2)*the ObjectMap of F).[o2,o1] by A2,A3,MSUALG_3:def 3; hence rng(Morph-Map(F,o2,o1)) = ((the Arrows of C2)*the ObjectMap of F).[o2,o1] by A2,A4,FUNCTOR0:def 15 .= (the Arrows of C2).((the ObjectMap of F).[o2,o1]) by A5,FUNCT_1:23 .= (the Arrows of C2).((the ObjectMap of F).(o2,o1)) by BINOP_1:def 1 .= (the Arrows of C2).[F.o1,F.o2] by FUNCTOR0:24 .= (the Arrows of C2).(F.o1,F.o2) by BINOP_1:def 1 .= <^F.o1,F.o2^> by ALTCAT_1:def 2; end; end; assume A6: for o1,o2 being object of C1 holds Morph-Map(F,o2,o1) is onto; consider I2' being non empty set, B' being ManySortedSet of I2', f' being Function of I, I2' such that A7: the ObjectMap of F = f' and A8: the Arrows of C2 = B' & the MorphMap of F is ManySortedFunction of the Arrows of C1, B'*f' by FUNCTOR0:def 4; reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of C1, (the Arrows of C2)*the ObjectMap of F by A7,A8; take f; thus f = the MorphMap of F; let i be set; assume i in I; then consider o2, o1 being set such that A9: o2 in the carrier of C1 & o1 in the carrier of C1 & i = [o2,o1] by ZFMISC_1:103; reconsider o1, o2 as object of C1 by A9; A10: [o2,o1] in I by ZFMISC_1:106; A11: (the MorphMap of F).[o2,o1] = (the MorphMap of F).(o2,o1) by BINOP_1:def 1; A12: [o2,o1] in dom(the ObjectMap of F) by A10,FUNCT_2:def 1; Morph-Map(F,o2,o1) is onto by A6; then rng(Morph-Map(F,o2,o1)) = <^F.o1,F.o2^> by FUNCT_2:def 3 .= (the Arrows of C2).(F.o1,F.o2) by ALTCAT_1:def 2 .= (the Arrows of C2).[F.o1,F.o2] by BINOP_1:def 1 .= (the Arrows of C2).((the ObjectMap of F).(o2,o1)) by FUNCTOR0:24 .= (the Arrows of C2).((the ObjectMap of F).[o2,o1]) by BINOP_1:def 1 .= ((the Arrows of C2)*the ObjectMap of F).[o2,o1] by A12,FUNCT_1:23; hence rng(f.i) = ((the Arrows of C2)*the ObjectMap of F).i by A9,A11, FUNCTOR0:def 15; end; theorem Th15: for C1, C2 being non empty AltCatStr for F being Contravariant FunctorStr over C1, C2 holds F is faithful iff for o1, o2 being object of C1 holds Morph-Map(F,o2,o1) is one-to-one proof let C1, C2 be non empty AltCatStr, F be Contravariant FunctorStr over C1,C2; set I = [:the carrier of C1, the carrier of C1:]; hereby assume A1: F is faithful; let o1, o2 be object of C1; A2: (the MorphMap of F) is "1-1" by A1,FUNCTOR0:def 31; A3: [o2,o1] in I by ZFMISC_1:106; A4: (the MorphMap of F).[o2,o1] = (the MorphMap of F).(o2,o1) by BINOP_1:def 1; reconsider g = (the MorphMap of F).[o2,o1] as Function; dom(the MorphMap of F) = I by PBOOLE:def 3; then g is one-to-one by A2,A3,MSUALG_3:def 2; hence Morph-Map(F,o2,o1) is one-to-one by A4,FUNCTOR0:def 15; end; assume A5: for o1, o2 being object of C1 holds Morph-Map(F,o2,o1) is one-to-one; let i be set, f be Function such that A6: i in dom(the MorphMap of F) & (the MorphMap of F).i = f; dom(the MorphMap of F) = I by PBOOLE:def 3; then consider o1, o2 being set such that A7: o1 in the carrier of C1 & o2 in the carrier of C1 & i = [o1,o2] by A6,ZFMISC_1:103; reconsider o1, o2 as object of C1 by A7; A8: (the MorphMap of F).(o1,o2) = Morph-Map(F,o1,o2) by FUNCTOR0:def 15; (the MorphMap of F).[o1,o2] = (the MorphMap of F).(o1,o2) by BINOP_1:def 1; hence f is one-to-one by A5,A6,A7,A8; end; theorem Th16: for C1, C2 being non empty AltCatStr for F being Covariant FunctorStr over C1, C2 for o1, o2 being object of C1, Fm being Morphism of F.o1, F.o2 st <^o1,o2^> <> {} & F is full feasible ex m being Morphism of o1, o2 st Fm = F.m proof let C1, C2 be non empty AltCatStr, F be Covariant FunctorStr over C1, C2, o1, o2 be object of C1, Fm be Morphism of F.o1, F.o2 such that A1: <^o1,o2^> <> {}; assume F is full; then Morph-Map(F,o1,o2) is onto by FUNCTOR1:18; then A2: rng Morph-Map(F,o1,o2) = <^F.o1,F.o2^> by FUNCT_2:def 3; assume F is feasible; then A3: <^F.o1,F.o2^> <> {} by A1,FUNCTOR0:def 19; then consider m being set such that A4: m in dom Morph-Map(F,o1,o2) and A5: Fm = Morph-Map(F,o1,o2).m by A2,FUNCT_1:def 5; dom Morph-Map(F,o1,o2) = <^o1,o2^> by A3,FUNCT_2:def 1; then reconsider m as Morphism of o1, o2 by A4; take m; thus Fm = F.m by A1,A3,A5,FUNCTOR0:def 16; end; theorem Th17: for C1, C2 being non empty AltCatStr for F being Contravariant FunctorStr over C1, C2 for o1, o2 being object of C1, Fm being Morphism of F.o2, F.o1 st <^o1,o2^> <> {} & F is full feasible ex m being Morphism of o1, o2 st Fm = F.m proof let C1, C2 be non empty AltCatStr, F be Contravariant FunctorStr over C1, C2, o1, o2 be object of C1, Fm be Morphism of F.o2, F.o1 such that A1: <^o1,o2^> <> {}; assume F is full; then Morph-Map(F,o1,o2) is onto by Th14; then A2: rng Morph-Map(F,o1,o2) = <^F.o2,F.o1^> by FUNCT_2:def 3; assume F is feasible; then A3: <^F.o2,F.o1^> <> {} by A1,FUNCTOR0:def 20; then consider m being set such that A4: m in dom Morph-Map(F,o1,o2) and A5: Fm = Morph-Map(F,o1,o2).m by A2,FUNCT_1:def 5; dom Morph-Map(F,o1,o2) = <^o1,o2^> by A3,FUNCT_2:def 1; then reconsider m as Morphism of o1, o2 by A4; take m; thus Fm = F.m by A1,A3,A5,FUNCTOR0:def 17; end; theorem Th18: for A, B being transitive with_units (non empty AltCatStr) for F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds F.a is retraction proof let A, B be transitive with_units (non empty AltCatStr), F be covariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: <^o1,o2^> <> {} & <^o2,o1^> <> {}; assume a is retraction; then consider b being Morphism of o2, o1 such that A2: b is_right_inverse_of a by ALTCAT_3:def 2; take F.b; a * b = idm o2 by A2,ALTCAT_3:def 1; hence (F.a) * (F.b) = F.idm o2 by A1,FUNCTOR0:def 24 .= idm F.o2 by FUNCTOR2:2; end; theorem Th19: for A, B being transitive with_units (non empty AltCatStr) for F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds F.a is coretraction proof let A, B be transitive with_units (non empty AltCatStr), F be covariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: <^o1,o2^> <> {} & <^o2,o1^> <> {}; assume a is coretraction; then consider b being Morphism of o2, o1 such that A2: a is_right_inverse_of b by ALTCAT_3:def 3; take F.b; b * a = idm o1 by A2,ALTCAT_3:def 1; hence (F.b) * (F.a) = F.idm o1 by A1,FUNCTOR0:def 24 .= idm F.o1 by FUNCTOR2:2; end; theorem Th20: for A, B being category, F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds F.a is iso proof let A, B be category, F be covariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: <^o1,o2^> <> {} & <^o2,o1^> <> {} and A2: a is iso; A3: <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A1,FUNCTOR0:def 19; a is retraction coretraction by A1,A2,ALTCAT_3:6; then F.a is retraction coretraction by A1,Th18,Th19; hence F.a is iso by A3,ALTCAT_3:6; end; theorem for A, B being category, F being covariant Functor of A, B for o1, o2 being object of A st o1, o2 are_iso holds F.o1, F.o2 are_iso proof let A, B be category, F be covariant Functor of A, B, o1, o2 be object of A; assume A1: o1, o2 are_iso; then A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} by ALTCAT_3:def 6; hence <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by FUNCTOR0:def 19; consider a being Morphism of o1, o2 such that A3: a is iso by A1,ALTCAT_3:def 6; take F.a; thus F.a is iso by A2,A3,Th20; end; theorem Th22: for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds F.a is coretraction proof let A, B be transitive with_units (non empty AltCatStr), F be contravariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: <^o1,o2^> <> {} & <^o2,o1^> <> {}; assume a is retraction; then consider b being Morphism of o2, o1 such that A2: b is_right_inverse_of a by ALTCAT_3:def 2; take F.b; a * b = idm o2 by A2,ALTCAT_3:def 1; hence (F.b) * (F.a) = F.idm o2 by A1,FUNCTOR0:def 25 .= idm F.o2 by Th13; end; theorem Th23: for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds F.a is retraction proof let A, B be transitive with_units (non empty AltCatStr), F be contravariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: <^o1,o2^> <> {} & <^o2,o1^> <> {}; assume a is coretraction; then consider b being Morphism of o2, o1 such that A2: a is_right_inverse_of b by ALTCAT_3:def 3; take F.b; b * a = idm o1 by A2,ALTCAT_3:def 1; hence (F.a) * (F.b) = F.idm o1 by A1,FUNCTOR0:def 25 .= idm F.o1 by Th13; end; theorem Th24: for A, B being category, F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds F.a is iso proof let A, B be category, F be contravariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: <^o1,o2^> <> {} & <^o2,o1^> <> {} and A2: a is iso; A3: <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A1,FUNCTOR0:def 20; a is retraction coretraction by A1,A2,ALTCAT_3:6; then F.a is retraction coretraction by A1,Th22,Th23; hence F.a is iso by A3,ALTCAT_3:6; end; theorem for A, B being category, F being contravariant Functor of A, B for o1, o2 being object of A st o1, o2 are_iso holds F.o2, F.o1 are_iso proof let A, B be category, F be contravariant Functor of A, B, o1, o2 be object of A; assume A1: o1, o2 are_iso; then A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} by ALTCAT_3:def 6; hence <^F.o2,F.o1^> <> {} & <^F.o1,F.o2^> <> {} by FUNCTOR0:def 20; consider a being Morphism of o1, o2 such that A3: a is iso by A1,ALTCAT_3:def 6; take F.a; thus F.a is iso by A2,A3,Th24; end; theorem Th26: for A, B being transitive with_units (non empty AltCatStr) for F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is retraction holds a is retraction proof let A, B be transitive with_units (non empty AltCatStr), F be covariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: F is full faithful and A2: <^o1,o2^> <> {} and A3: <^o2,o1^> <> {}; assume F.a is retraction; then consider b being Morphism of F.o2, F.o1 such that A4: b is_right_inverse_of F.a by ALTCAT_3:def 2; A5: (F.a) * b = idm F.o2 by A4,ALTCAT_3:def 1; Morph-Map(F,o2,o1) is onto by A1,FUNCTOR1:18; then A6: rng Morph-Map(F,o2,o1) = <^F.o2,F.o1^> by FUNCT_2:def 3; A7: <^F.o2,F.o1^> <> {} by A3,FUNCTOR0:def 19; then consider a' being set such that A8: a' in dom Morph-Map(F,o2,o1) and A9: b = Morph-Map(F,o2,o1).a' by A6,FUNCT_1:def 5; A10: dom Morph-Map(F,o2,o2) = <^o2,o2^> by FUNCT_2:def 1; dom Morph-Map(F,o2,o1) = <^o2,o1^> by A7,FUNCT_2:def 1; then reconsider a' as Morphism of o2, o1 by A8; take a'; A11: Morph-Map(F,o2,o2) is one-to-one by A1,FUNCTOR1:19; Morph-Map(F,o2,o2).idm o2 = F.(idm o2) by FUNCTOR0:def 16 .= idm F.o2 by FUNCTOR2:2 .= (F.a) * F.a' by A3,A5,A7,A9,FUNCTOR0:def 16 .= F.(a * a') by A2,A3,FUNCTOR0:def 24 .= Morph-Map(F,o2,o2).(a * a') by FUNCTOR0:def 16; hence a * a' = idm o2 by A10,A11,FUNCT_1:def 8; end; theorem Th27: for A, B being transitive with_units (non empty AltCatStr) for F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is coretraction holds a is coretraction proof let A, B be transitive with_units (non empty AltCatStr), F be covariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: F is full faithful and A2: <^o1,o2^> <> {} and A3: <^o2,o1^> <> {}; assume F.a is coretraction; then consider b being Morphism of F.o2, F.o1 such that A4: F.a is_right_inverse_of b by ALTCAT_3:def 3; A5: b * (F.a) = idm F.o1 by A4,ALTCAT_3:def 1; Morph-Map(F,o2,o1) is onto by A1,FUNCTOR1:18; then A6: rng Morph-Map(F,o2,o1) = <^F.o2,F.o1^> by FUNCT_2:def 3; A7: <^F.o2,F.o1^> <> {} by A3,FUNCTOR0:def 19; then consider a' being set such that A8: a' in dom Morph-Map(F,o2,o1) and A9: b = Morph-Map(F,o2,o1).a' by A6,FUNCT_1:def 5; A10: dom Morph-Map(F,o1,o1) = <^o1,o1^> by FUNCT_2:def 1; dom Morph-Map(F,o2,o1) = <^o2,o1^> by A7,FUNCT_2:def 1; then reconsider a' as Morphism of o2, o1 by A8; take a'; A11: Morph-Map(F,o1,o1) is one-to-one by A1,FUNCTOR1:19; Morph-Map(F,o1,o1).idm o1 = F.(idm o1) by FUNCTOR0:def 16 .= idm F.o1 by FUNCTOR2:2 .= (F.a') * F.a by A3,A5,A7,A9,FUNCTOR0:def 16 .= F.(a' * a) by A2,A3,FUNCTOR0:def 24 .= Morph-Map(F,o1,o1).(a' * a) by FUNCTOR0:def 16; hence a' * a = idm o1 by A10,A11,FUNCT_1:def 8; end; theorem Th28: for A, B being category, F being covariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is iso holds a is iso proof let A, B be category, F be covariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: F is full faithful and A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} and A3: F.a is iso; <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A2,FUNCTOR0:def 19; then F.a is retraction coretraction by A3,ALTCAT_3:6; then a is retraction coretraction by A1,A2,Th26,Th27; hence a is iso by A2,ALTCAT_3:6; end; theorem for A, B being category, F being covariant Functor of A, B for o1, o2 being object of A st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.o1, F.o2 are_iso holds o1, o2 are_iso proof let A, B be category, F be covariant Functor of A, B, o1, o2 be object of A such that A1: F is full faithful and A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} and A3: F.o1, F.o2 are_iso; thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A2; consider Fa being Morphism of F.o1, F.o2 such that A4: Fa is iso by A3,ALTCAT_3:def 6; consider a being Morphism of o1, o2 such that A5: Fa = F.a by A1,A2,Th16; take a; thus a is iso by A1,A2,A4,A5,Th28; end; theorem Th30: for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is retraction holds a is coretraction proof let A, B be transitive with_units (non empty AltCatStr), F be contravariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: F is full faithful and A2: <^o1,o2^> <> {} and A3: <^o2,o1^> <> {}; assume F.a is retraction; then consider b being Morphism of F.o1, F.o2 such that A4: b is_right_inverse_of F.a by ALTCAT_3:def 2; A5: (F.a) * b = idm F.o1 by A4,ALTCAT_3:def 1; Morph-Map(F,o2,o1) is onto by A1,Th14; then A6: rng Morph-Map(F,o2,o1) = <^F.o1,F.o2^> by FUNCT_2:def 3; A7: <^F.o1,F.o2^> <> {} by A3,FUNCTOR0:def 20; then consider a' being set such that A8: a' in dom Morph-Map(F,o2,o1) and A9: b = Morph-Map(F,o2,o1).a' by A6,FUNCT_1:def 5; A10: dom Morph-Map(F,o1,o1) = <^o1,o1^> by FUNCT_2:def 1; dom Morph-Map(F,o2,o1) = <^o2,o1^> by A7,FUNCT_2:def 1; then reconsider a' as Morphism of o2, o1 by A8; take a'; A11: Morph-Map(F,o1,o1) is one-to-one by A1,Th15; Morph-Map(F,o1,o1).idm o1 = F.(idm o1) by FUNCTOR0:def 17 .= idm F.o1 by Th13 .= (F.a) * F.a' by A3,A5,A7,A9,FUNCTOR0:def 17 .= F.(a' * a) by A2,A3,FUNCTOR0:def 25 .= Morph-Map(F,o1,o1).(a' * a) by FUNCTOR0:def 17; hence a' * a = idm o1 by A10,A11,FUNCT_1:def 8; end; theorem Th31: for A, B being transitive with_units (non empty AltCatStr) for F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is coretraction holds a is retraction proof let A, B be transitive with_units (non empty AltCatStr), F be contravariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: F is full faithful and A2: <^o1,o2^> <> {} and A3: <^o2,o1^> <> {}; assume F.a is coretraction; then consider b being Morphism of F.o1, F.o2 such that A4: F.a is_right_inverse_of b by ALTCAT_3:def 3; A5: b * (F.a) = idm F.o2 by A4,ALTCAT_3:def 1; Morph-Map(F,o2,o1) is onto by A1,Th14; then A6: rng Morph-Map(F,o2,o1) = <^F.o1,F.o2^> by FUNCT_2:def 3; A7: <^F.o1,F.o2^> <> {} by A3,FUNCTOR0:def 20; then consider a' being set such that A8: a' in dom Morph-Map(F,o2,o1) and A9: b = Morph-Map(F,o2,o1).a' by A6,FUNCT_1:def 5; A10: dom Morph-Map(F,o2,o2) = <^o2,o2^> by FUNCT_2:def 1; dom Morph-Map(F,o2,o1) = <^o2,o1^> by A7,FUNCT_2:def 1; then reconsider a' as Morphism of o2, o1 by A8; take a'; A11: Morph-Map(F,o2,o2) is one-to-one by A1,Th15; Morph-Map(F,o2,o2).idm o2 = F.(idm o2) by FUNCTOR0:def 17 .= idm F.o2 by Th13 .= (F.a') * F.a by A3,A5,A7,A9,FUNCTOR0:def 17 .= F.(a * a') by A2,A3,FUNCTOR0:def 25 .= Morph-Map(F,o2,o2).(a * a') by FUNCTOR0:def 17; hence a * a' = idm o2 by A10,A11,FUNCT_1:def 8; end; theorem Th32: for A, B being category, F being contravariant Functor of A, B for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is iso holds a is iso proof let A, B be category, F be contravariant Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that A1: F is full faithful and A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} and A3: F.a is iso; <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A2,FUNCTOR0:def 20; then F.a is retraction coretraction by A3,ALTCAT_3:6; then a is retraction coretraction by A1,A2,Th30,Th31; hence a is iso by A2,ALTCAT_3:6; end; theorem for A, B being category, F being contravariant Functor of A, B for o1, o2 being object of A st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.o2, F.o1 are_iso holds o1, o2 are_iso proof let A, B be category, F be contravariant Functor of A, B, o1, o2 be object of A such that A1: F is full faithful and A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} and A3: F.o2, F.o1 are_iso; thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A2; consider Fa being Morphism of F.o2, F.o1 such that A4: Fa is iso by A3,ALTCAT_3:def 6; consider a being Morphism of o1, o2 such that A5: Fa = F.a by A1,A2,Th17; take a; thus a is iso by A1,A2,A4,A5,Th32; end; Lm1: now let C be non empty transitive AltCatStr, p1, p2, p3 be object of C such that A1: (the Arrows of C).(p1,p3) = {}; thus [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] = {} proof assume [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] <> {}; then consider k being set such that A2: k in [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] by XBOOLE_0:def 1; consider u1, u2 being set such that A3: u1 in (the Arrows of C).(p2,p3) & u2 in (the Arrows of C).(p1,p2) & k = [u1,u2] by A2,ZFMISC_1:def 2; u1 in <^p2,p3^> & u2 in <^p1,p2^> by A3,ALTCAT_1:def 2; then <^p1,p3^> <> {} by ALTCAT_1:def 4; hence contradiction by A1,ALTCAT_1:def 2; end; end; begin :: The subcategories of the morphisms theorem Th34: for C being AltCatStr, D being SubCatStr of C st the carrier of C = the carrier of D & the Arrows of C = the Arrows of D holds D is full proof let C be AltCatStr, D be SubCatStr of C; assume A1: the carrier of C = the carrier of D & the Arrows of C = the Arrows of D; then dom (the Arrows of C) = [:the carrier of D, the carrier of D:] by PBOOLE:def 3; hence the Arrows of D = (the Arrows of C)|[:the carrier of D, the carrier of D:] by A1,RELAT_1:97; end; theorem Th35: for C being with_units (non empty AltCatStr), D being SubCatStr of C st the carrier of C = the carrier of D & the Arrows of C = the Arrows of D holds D is full id-inheriting proof let C be with_units (non empty AltCatStr), D be SubCatStr of C; assume A1: the carrier of C = the carrier of D & the Arrows of C = the Arrows of D; hence D is full by Th34; D is non empty proof thus the carrier of D is non empty by A1; end; then reconsider D as full non empty SubCatStr of C by A1,Th34; now let o be object of D, o' be object of C such that A2: o = o'; <^o',o'^> = <^o,o^> by A2,ALTCAT_2:29; hence idm o' in <^o,o^>; end; hence thesis by ALTCAT_2:def 14; end; definition let C be category; cluster full non empty strict subcategory of C; existence proof the AltCatStr of C is SubCatStr of C proof thus the carrier of the AltCatStr of C c= the carrier of C; thus the Arrows of the AltCatStr of C cc= the Arrows of C; thus the Comp of the AltCatStr of C cc= the Comp of C; end; then reconsider D = the AltCatStr of C as SubCatStr of C; reconsider D as full non empty id-inheriting SubCatStr of C by Th35; take D; thus thesis; end; end; theorem Th36: for B being non empty subcategory of C for A being non empty subcategory of B holds A is non empty subcategory of C proof let B be non empty subcategory of C, A be non empty subcategory of B; reconsider D = A as with_units (non empty SubCatStr of C) by ALTCAT_2:22; D is id-inheriting proof now let o be object of D, o1 be object of C such that A1: o = o1; A2: o in the carrier of D; the carrier of D c= the carrier of B by ALTCAT_2:def 11; then reconsider oo = o as object of B by A2; idm o = idm oo by ALTCAT_2:35 .= idm o1 by A1,ALTCAT_2:35; hence idm o1 in <^o,o^>; end; hence thesis by ALTCAT_2:def 14; end; hence A is non empty subcategory of C; end; theorem Th37: for C being non empty transitive AltCatStr for D being non empty transitive SubCatStr of C for o1, o2 being object of C, p1, p2 being object of D for m being Morphism of o1, o2, n being Morphism of p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds (m is mono implies n is mono) & (m is epi implies n is epi) proof let C be non empty transitive AltCatStr, D be non empty transitive SubCatStr of C, o1, o2 be object of C, p1, p2 be object of D, m be Morphism of o1, o2, n be Morphism of p1, p2 such that A1: p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {}; thus m is mono implies n is mono proof assume A2: m is mono; let p3 be object of D such that A3: <^p3,p1^> <> {}; let f, g be Morphism of p3, p1 such that A4: n * f = n * g; reconsider o3 = p3 as object of C by ALTCAT_2:30; <^p3,p1^> c= <^o3,o1^> by A1,ALTCAT_2:32; then A5: <^o3,o1^> <> {} by A3,XBOOLE_1:3; reconsider f1 = f, g1 = g as Morphism of o3, o1 by A1,A3,ALTCAT_2:34; m * f1 = n * f by A1,A3,ALTCAT_2:33 .= m * g1 by A1,A3,A4,ALTCAT_2:33; hence f = g by A2,A5,ALTCAT_3:def 7; end; assume A6: m is epi; let p3 be object of D such that A7: <^p2,p3^> <> {}; let f, g be Morphism of p2, p3 such that A8: f * n = g * n; reconsider o3 = p3 as object of C by ALTCAT_2:30; <^p2,p3^> c= <^o2,o3^> by A1,ALTCAT_2:32; then A9: <^o2,o3^> <> {} by A7,XBOOLE_1:3; reconsider f1 = f, g1 = g as Morphism of o2, o3 by A1,A7,ALTCAT_2:34; f1 * m = f * n by A1,A7,ALTCAT_2:33 .= g1 * m by A1,A7,A8,ALTCAT_2:33; hence f = g by A6,A9,ALTCAT_3:def 8; end; theorem Th38: for D being non empty subcategory of C for o1, o2 being object of C, p1, p2 being object of D for m being Morphism of o1, o2, m1 being Morphism of o2, o1 for n being Morphism of p1, p2, n1 being Morphism of p2, p1 st p1 = o1 & p2 = o2 & m = n & m1 = n1 & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds (m is_left_inverse_of m1 iff n is_left_inverse_of n1) & (m is_right_inverse_of m1 iff n is_right_inverse_of n1) proof let D be non empty subcategory of C, o1, o2 be object of C, p1, p2 be object of D, m be Morphism of o1, o2, m1 be Morphism of o2, o1, n be Morphism of p1, p2, n1 be Morphism of p2, p1 such that A1: p1 = o1 & p2 = o2 & m = n & m1 = n1 & <^p1,p2^> <> {} & <^p2,p1^> <> {}; thus m is_left_inverse_of m1 iff n is_left_inverse_of n1 proof thus m is_left_inverse_of m1 implies n is_left_inverse_of n1 proof assume A2: m is_left_inverse_of m1; thus n * n1 = m * m1 by A1,ALTCAT_2:33 .= idm o2 by A2,ALTCAT_3:def 1 .= idm p2 by A1,ALTCAT_2:35; end; assume A3: n is_left_inverse_of n1; thus m * m1 = n * n1 by A1,ALTCAT_2:33 .= idm p2 by A3,ALTCAT_3:def 1 .= idm o2 by A1,ALTCAT_2:35; end; thus m is_right_inverse_of m1 implies n is_right_inverse_of n1 proof assume A4: m is_right_inverse_of m1; thus n1 * n = m1 * m by A1,ALTCAT_2:33 .= idm o1 by A4,ALTCAT_3:def 1 .= idm p1 by A1,ALTCAT_2:35; end; assume A5: n is_right_inverse_of n1; thus m1 * m = n1 * n by A1,ALTCAT_2:33 .= idm p1 by A5,ALTCAT_3:def 1 .= idm o1 by A1,ALTCAT_2:35; end; theorem for D being full non empty subcategory of C for o1, o2 being object of C, p1, p2 being object of D for m being Morphism of o1, o2, n being Morphism of p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds (m is retraction implies n is retraction) & (m is coretraction implies n is coretraction) & (m is iso implies n is iso) proof let D be full non empty subcategory of C, o1, o2 be object of C, p1, p2 be object of D, m be Morphism of o1, o2, n be Morphism of p1, p2; assume A1: p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {}; then A2: <^p2,p1^> = <^o2,o1^> by ALTCAT_2:29; thus A3: m is retraction implies n is retraction proof assume m is retraction; then consider B being Morphism of o2, o1 such that A4: B is_right_inverse_of m by ALTCAT_3:def 2; reconsider B1 = B as Morphism of p2, p1 by A2; take B1; thus B1 is_right_inverse_of n by A1,A4,Th38; end; thus A5: m is coretraction implies n is coretraction proof assume m is coretraction; then consider B being Morphism of o2, o1 such that A6: B is_left_inverse_of m by ALTCAT_3:def 3; reconsider B1 = B as Morphism of p2, p1 by A2; take B1; thus B1 is_left_inverse_of n by A1,A6,Th38; end; assume m is iso; hence n is iso by A1,A3,A5,ALTCAT_3:5,6; end; theorem Th40: for D being non empty subcategory of C for o1, o2 being object of C, p1, p2 being object of D for m being Morphism of o1, o2, n being Morphism of p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds (n is retraction implies m is retraction) & (n is coretraction implies m is coretraction) & (n is iso implies m is iso) proof let D be non empty subcategory of C, o1, o2 be object of C, p1, p2 be object of D, m be Morphism of o1, o2, n be Morphism of p1, p2 such that A1: p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {}; thus A2: n is retraction implies m is retraction proof assume n is retraction; then consider B being Morphism of p2, p1 such that A3: B is_right_inverse_of n by ALTCAT_3:def 2; reconsider B1 = B as Morphism of o2, o1 by A1,ALTCAT_2:34; take B1; thus B1 is_right_inverse_of m by A1,A3,Th38; end; thus A4: n is coretraction implies m is coretraction proof assume n is coretraction; then consider B being Morphism of p2, p1 such that A5: B is_left_inverse_of n by ALTCAT_3:def 3; reconsider B1 = B as Morphism of o2, o1 by A1,ALTCAT_2:34; take B1; thus B1 is_left_inverse_of m by A1,A5,Th38; end; assume A6: n is iso; <^p1,p2^> c= <^o1,o2^> & <^p2,p1^> c= <^o2,o1^> by A1,ALTCAT_2:32; then <^o1,o2^> <> {} & <^o2,o1^> <> {} by A1,XBOOLE_1:3; hence m is iso by A2,A4,A6,ALTCAT_3:5,6; end; definition let C be category; func AllMono C -> strict non empty transitive SubCatStr of C means :Def1: the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & m is mono; existence proof set I = the carrier of C; defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & x = m & m is mono; A1: for i being set st i in [:I,I:] ex X being set st P[i,X] proof let i be set; assume i in [:I,I:]; then consider o1, o2 being set such that A2: o1 in I & o2 in I & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A2; defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} & m = $1 & m is mono; consider X being set such that A3: for x being set holds x in X iff x in (the Arrows of C).(o1,o2) & P[x] from Separation; take X; let x be set; thus x in X implies ex o1, o2 being object of C, m being Morphism of o1, o2 st i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is mono proof assume x in X; then consider m being Morphism of o1, o2 such that A4: <^o1,o2^> <> {} & m = x & m is mono by A3; take o1, o2, m; thus i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is mono by A2,A4; end; given p1, p2 being object of C, m being Morphism of p1, p2 such that A5: i = [p1,p2] & <^p1,p2^> <> {} & x = m & m is mono; A6: o1 = p1 & o2 = p2 by A2,A5,ZFMISC_1:33; m in <^p1,p2^> by A5; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence x in X by A3,A5,A6; end; consider Ar being ManySortedSet of [:I,I:] such that A7: for i being set st i in [:I,I:] holds P[i,Ar.i] from MSSEx(A1); A8: Ar cc= the Arrows of C proof thus [:I,I:] c= [:the carrier of C,the carrier of C:]; let i be set; assume A9: i in [:I,I:]; let q be set; assume q in Ar.i; then consider p1, p2 being object of C, m being Morphism of p1, p2 such that A10: i = [p1,p2] & <^p1,p2^> <> {} & q = m & m is mono by A7,A9; m in <^p1,p2^> by A10; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence q in (the Arrows of C).i by A10,BINOP_1:def 1; end; defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3] & $2 = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; A11: for i being set st i in [:I,I,I:] ex j being set st R[i,j] proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being set such that A12: p1 in I & p2 in I & p3 in I & i = [p1,p2,p3] by MCART_1:72; reconsider p1, p2, p3 as object of C by A12; take ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; take p1, p2, p3; thus i = [p1,p2,p3] by A12; thus thesis; end; consider Co being ManySortedSet of [:I,I,I:] such that A13: for i being set st i in [:I,I,I:] holds R[i,Co.i] from MSSEx(A11); Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|} proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being object of C such that A14: i = [p1,p2,p3] and A15: Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13; A16: (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] = {} by Lm1; [p2,p3] in [:I,I:] & [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then Ar.[p2,p3] c= (the Arrows of C).[p2,p3] & Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A8,ALTCAT_2:def 2; then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) & Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; then A17: Ar.(p2,p3) c= (the Arrows of C).(p2,p3) & Ar.(p1,p2) c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; A18: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {} proof assume A19: (the Arrows of C).(p1,p3) = {}; assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {}; then consider k being set such that A20: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1; consider u1, u2 being set such that A21: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) & k = [u1,u2] by A20,ZFMISC_1:def 2; u1 in (the Arrows of C).(p2,p3) & u2 in (the Arrows of C).(p1,p2) by A17,A21; then u1 in <^p2,p3^> & u2 in <^p1,p2^> by ALTCAT_1:def 2; then <^p1,p3^> <> {} by ALTCAT_1:def 4; hence contradiction by A19,ALTCAT_1:def 2; end; [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] by A17,ZFMISC_1:119; then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the Arrows of C).(p1,p3) by A15,A16,FUNCT_2:38; A22: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 5; A23: {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 6; A24: rng f c= {|Ar|}.i proof let q be set; assume q in rng f; then consider x being set such that A25: x in dom f and A26: q = f.x by FUNCT_1:def 5; A27: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A18,FUNCT_2:def 1; then consider m1, m2 being set such that A28: m1 in Ar.(p2,p3) & m2 in Ar.(p1,p2) and A29: x = [m1,m2] by A25,ZFMISC_1:103; A30: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by A28,BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A31: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & m1 = qq & qq is mono by A7,A30; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A32: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & m2 = rr & rr is mono by A7,A30; A33: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & q = m & m is mono proof A34: r2 = p2 by A32,ZFMISC_1:33; A35: p2 = q2 by A31,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A32,ZFMISC_1:33; take r1, q3, mm * rr; A36: p1 = r1 & p3 = q3 by A31,A32,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus <^r1,q3^> <> {} by A31,A32,A34,A35,ALTCAT_1:def 4; thus q = (the Comp of C).(p1,p2,p3).x by A15,A25,A26,A27,FUNCT_1:72 .= (the Comp of C).(p1,p2,p3).(mm,rr) by A29,A31,A32,BINOP_1:def 1 .= mm * rr by A31,A32,A34,A35,A36,ALTCAT_1:def 10; thus mm * rr is mono by A31,A32,A34,A35,ALTCAT_3:9; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then q in Ar.[p1,p3] by A7,A33; then q in Ar.(p1,p3) by BINOP_1:def 1; hence q in {|Ar|}.i by A14,A22,MULTOP_1:def 1; end; [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A14,A23,MULTOP_1:def 1; hence Co.i is Function of {|Ar,Ar|}.i, {|Ar|}.i by A18,A24,FUNCT_2:8; end; then reconsider Co as BinComp of Ar; set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT; IT is SubCatStr of C proof thus the carrier of IT c= the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; thus [:J,J,J:] c= [:I,I,I:]; let i be set such that A37: i in [:J,J,J:]; let q be set such that A38: q in (the Comp of IT).i; consider p1, p2, p3 being object of C such that A39: i = [p1,p2,p3] & Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13,A37; ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] c= (the Comp of C).(p1,p2,p3) by RELAT_1:88; then q in (the Comp of C).(p1,p2,p3) by A38,A39; hence q in (the Comp of C).i by A39,MULTOP_1:def 1; end; then reconsider IT as strict non empty SubCatStr of C; IT is transitive proof let p1, p2, p3 be object of IT; assume A40: <^p1,p2^> <> {} & <^p2,p3^> <> {}; then consider m2 being set such that A41: m2 in <^p1,p2^> by XBOOLE_0:def 1; consider m1 being set such that A42: m1 in <^p2,p3^> by A40,XBOOLE_0:def 1; m2 in Ar.(p1,p2) & m1 in Ar.(p2,p3) by A41,A42,ALTCAT_1:def 2; then A43: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A44: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & m1 = qq & qq is mono by A7,A43; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A45: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & m2 = rr & rr is mono by A7,A43; A46: r2 = p2 by A45,ZFMISC_1:33; A47: p2 = q2 by A44,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A45,ZFMISC_1:33; A48: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & mm * rr = m & m is mono proof take r1, q3, mm * rr; p1 = r1 & p3 = q3 by A44,A45,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus <^r1,q3^> <> {} by A44,A45,A46,A47,ALTCAT_1:def 4; thus mm * rr = mm * rr; thus mm * rr is mono by A44,A45,A46,A47,ALTCAT_3:9; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then mm * rr in Ar.[p1,p3] by A7,A48; then mm * rr in Ar.(p1,p3) by BINOP_1:def 1; hence <^p1,p3^> <> {} by ALTCAT_1:def 2; end; then reconsider IT as strict non empty transitive SubCatStr of C; take IT; thus the carrier of IT = the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; let o1, o2 be object of C, m be Morphism of o1, o2; A49: [o1,o2] in [:I,I:] by ZFMISC_1:def 2; thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & m is mono proof assume m in (the Arrows of IT).(o1,o2); then m in Ar.[o1,o2] by BINOP_1:def 1; then consider p1, p2 being object of C, n being Morphism of p1, p2 such that A50: [o1,o2] = [p1,p2] & <^p1,p2^> <> {} & m = n & n is mono by A7,A49; o1 = p1 & o2 = p2 by A50,ZFMISC_1:33; hence <^o1,o2^> <> {} & m is mono by A50; end; assume <^o1,o2^> <> {} & m is mono; then m in (the Arrows of IT).[o1,o2] by A7,A49; hence m in (the Arrows of IT).(o1,o2) by BINOP_1:def 1; end; uniqueness proof let S1, S2 be strict non empty transitive SubCatStr of C such that A51: the carrier of S1 = the carrier of C and A52: the Arrows of S1 cc= the Arrows of C and A53: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & m is mono and A54: the carrier of S2 = the carrier of C and A55: the Arrows of S2 cc= the Arrows of C and A56: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & m is mono; now let i be set; assume A57: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A58: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A58; thus (the Arrows of S1).i = (the Arrows of S2).i proof thus (the Arrows of S1).i c= (the Arrows of S2).i proof let n be set such that A59: n in (the Arrows of S1).i; (the Arrows of S1).i c= (the Arrows of C).i by A51,A52,A57,ALTCAT_2:def 2; then n in (the Arrows of C).i by A59; then n in (the Arrows of C).(o1,o2) by A58,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S1).(o1,o2) by A58,A59,BINOP_1:def 1; then <^o1,o2^> <> {} & m is mono by A53; then m in (the Arrows of S2).(o1,o2) by A56; hence n in (the Arrows of S2).i by A58,BINOP_1:def 1; end; let n be set such that A60: n in (the Arrows of S2).i; (the Arrows of S2).i c= (the Arrows of C).i by A54,A55,A57,ALTCAT_2:def 2; then n in (the Arrows of C).i by A60; then n in (the Arrows of C).(o1,o2) by A58,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S2).(o1,o2) by A58,A60,BINOP_1:def 1; then <^o1,o2^> <> {} & m is mono by A56; then m in (the Arrows of S1).(o1,o2) by A53; hence n in (the Arrows of S1).i by A58,BINOP_1:def 1; end; end; then the Arrows of S1 = the Arrows of S2 by A51,A54,PBOOLE:3; hence S1 = S2 by A51,A54,ALTCAT_2:27; end; end; definition let C be category; cluster AllMono C -> id-inheriting; coherence proof now let o be object of AllMono C, o' be object of C such that A1: o = o'; idm o' in (the Arrows of AllMono C).(o,o) by A1,Def1; hence idm o' in <^o,o^> by ALTCAT_1:def 2; end; hence thesis by ALTCAT_2:def 14; end; end; definition let C be category; func AllEpi C -> strict non empty transitive SubCatStr of C means :Def2: the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & m is epi; existence proof set I = the carrier of C; defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi; A1: for i being set st i in [:I,I:] ex X being set st P[i,X] proof let i be set; assume i in [:I,I:]; then consider o1, o2 being set such that A2: o1 in I & o2 in I & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A2; defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} & m = $1 & m is epi; consider X being set such that A3: for x being set holds x in X iff x in (the Arrows of C).(o1,o2) & P[x] from Separation; take X; let x be set; thus x in X implies ex o1, o2 being object of C, m being Morphism of o1, o2 st i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi proof assume x in X; then consider m being Morphism of o1, o2 such that A4: <^o1,o2^> <> {} & m = x & m is epi by A3; take o1, o2, m; thus i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi by A2,A4; end; given p1, p2 being object of C, m being Morphism of p1, p2 such that A5: i = [p1,p2] & <^p1,p2^> <> {} & x = m & m is epi; A6: o1 = p1 & o2 = p2 by A2,A5,ZFMISC_1:33; m in <^p1,p2^> by A5; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence x in X by A3,A5,A6; end; consider Ar being ManySortedSet of [:I,I:] such that A7: for i being set st i in [:I,I:] holds P[i,Ar.i] from MSSEx(A1); A8: Ar cc= the Arrows of C proof thus [:I,I:] c= [:the carrier of C,the carrier of C:]; let i be set; assume A9: i in [:I,I:]; let q be set; assume q in Ar.i; then consider p1, p2 being object of C, m being Morphism of p1, p2 such that A10: i = [p1,p2] & <^p1,p2^> <> {} & q = m & m is epi by A7,A9; m in <^p1,p2^> by A10; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence q in (the Arrows of C).i by A10,BINOP_1:def 1; end; defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3] & $2 = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; A11: for i being set st i in [:I,I,I:] ex j being set st R[i,j] proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being set such that A12: p1 in I & p2 in I & p3 in I & i = [p1,p2,p3] by MCART_1:72; reconsider p1, p2, p3 as object of C by A12; take ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; take p1, p2, p3; thus i = [p1,p2,p3] by A12; thus thesis; end; consider Co being ManySortedSet of [:I,I,I:] such that A13: for i being set st i in [:I,I,I:] holds R[i,Co.i] from MSSEx(A11); Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|} proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being object of C such that A14: i = [p1,p2,p3] and A15: Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13; A16: (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] = {} by Lm1; [p2,p3] in [:I,I:] & [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then Ar.[p2,p3] c= (the Arrows of C).[p2,p3] & Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A8,ALTCAT_2:def 2; then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) & Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; then A17: Ar.(p2,p3) c= (the Arrows of C).(p2,p3) & Ar.(p1,p2) c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; A18: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {} proof assume A19: (the Arrows of C).(p1,p3) = {}; assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {}; then consider k being set such that A20: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1; consider u1, u2 being set such that A21: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) & k = [u1,u2] by A20,ZFMISC_1:def 2; u1 in (the Arrows of C).(p2,p3) & u2 in (the Arrows of C).(p1,p2) by A17,A21; then u1 in <^p2,p3^> & u2 in <^p1,p2^> by ALTCAT_1:def 2; then <^p1,p3^> <> {} by ALTCAT_1:def 4; hence contradiction by A19,ALTCAT_1:def 2; end; [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] by A17,ZFMISC_1:119; then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the Arrows of C).(p1,p3) by A15,A16,FUNCT_2:38; A22: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 5; A23: {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 6; A24: rng f c= {|Ar|}.i proof let q be set; assume q in rng f; then consider x being set such that A25: x in dom f and A26: q = f.x by FUNCT_1:def 5; A27: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A18,FUNCT_2:def 1; then consider m1, m2 being set such that A28: m1 in Ar.(p2,p3) & m2 in Ar.(p1,p2) and A29: x = [m1,m2] by A25,ZFMISC_1:103; A30: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by A28,BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A31: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & m1 = qq & qq is epi by A7,A30 ; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A32: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & m2 = rr & rr is epi by A7,A30 ; A33: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & q = m & m is epi proof A34: r2 = p2 by A32,ZFMISC_1:33; A35: p2 = q2 by A31,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A32,ZFMISC_1:33; take r1, q3, mm * rr; A36: p1 = r1 & p3 = q3 by A31,A32,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus <^r1,q3^> <> {} by A31,A32,A34,A35,ALTCAT_1:def 4; thus q = (the Comp of C).(p1,p2,p3).x by A15,A25,A26,A27,FUNCT_1:72 .= (the Comp of C).(p1,p2,p3).(mm,rr) by A29,A31,A32,BINOP_1:def 1 .= mm * rr by A31,A32,A34,A35,A36,ALTCAT_1:def 10; thus mm * rr is epi by A31,A32,A34,A35,ALTCAT_3:10; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then q in Ar.[p1,p3] by A7,A33; then q in Ar.(p1,p3) by BINOP_1:def 1; hence q in {|Ar|}.i by A14,A22,MULTOP_1:def 1; end; [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A14,A23,MULTOP_1:def 1; hence Co.i is Function of {|Ar,Ar|}.i, {|Ar|}.i by A18,A24,FUNCT_2:8; end; then reconsider Co as BinComp of Ar; set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT; IT is SubCatStr of C proof thus the carrier of IT c= the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; thus [:J,J,J:] c= [:I,I,I:]; let i be set such that A37: i in [:J,J,J:]; let q be set such that A38: q in (the Comp of IT).i; consider p1, p2, p3 being object of C such that A39: i = [p1,p2,p3] & Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13,A37; ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] c= (the Comp of C).(p1,p2,p3) by RELAT_1:88; then q in (the Comp of C).(p1,p2,p3) by A38,A39; hence q in (the Comp of C).i by A39,MULTOP_1:def 1; end; then reconsider IT as strict non empty SubCatStr of C; IT is transitive proof let p1, p2, p3 be object of IT; assume A40: <^p1,p2^> <> {} & <^p2,p3^> <> {}; then consider m2 being set such that A41: m2 in <^p1,p2^> by XBOOLE_0:def 1; consider m1 being set such that A42: m1 in <^p2,p3^> by A40,XBOOLE_0:def 1; m2 in Ar.(p1,p2) & m1 in Ar.(p2,p3) by A41,A42,ALTCAT_1:def 2; then A43: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A44: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & m1 = qq & qq is epi by A7,A43; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A45: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & m2 = rr & rr is epi by A7,A43; A46: r2 = p2 by A45,ZFMISC_1:33; A47: p2 = q2 by A44,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A45,ZFMISC_1:33; A48: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & mm * rr = m & m is epi proof take r1, q3, mm * rr; p1 = r1 & p3 = q3 by A44,A45,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus <^r1,q3^> <> {} by A44,A45,A46,A47,ALTCAT_1:def 4; thus mm * rr = mm * rr; thus mm * rr is epi by A44,A45,A46,A47,ALTCAT_3:10; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then mm * rr in Ar.[p1,p3] by A7,A48; then mm * rr in Ar.(p1,p3) by BINOP_1:def 1; hence <^p1,p3^> <> {} by ALTCAT_1:def 2; end; then reconsider IT as strict non empty transitive SubCatStr of C; take IT; thus the carrier of IT = the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; let o1, o2 be object of C, m be Morphism of o1, o2; A49: [o1,o2] in [:I,I:] by ZFMISC_1:def 2; thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & m is epi proof assume m in (the Arrows of IT).(o1,o2); then m in Ar.[o1,o2] by BINOP_1:def 1; then consider p1, p2 being object of C, n being Morphism of p1, p2 such that A50: [o1,o2] = [p1,p2] & <^p1,p2^> <> {} & m = n & n is epi by A7,A49; o1 = p1 & o2 = p2 by A50,ZFMISC_1:33; hence <^o1,o2^> <> {} & m is epi by A50; end; assume <^o1,o2^> <> {} & m is epi; then m in (the Arrows of IT).[o1,o2] by A7,A49; hence m in (the Arrows of IT).(o1,o2) by BINOP_1:def 1; end; uniqueness proof let S1, S2 be strict non empty transitive SubCatStr of C such that A51: the carrier of S1 = the carrier of C and A52: the Arrows of S1 cc= the Arrows of C and A53: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & m is epi and A54: the carrier of S2 = the carrier of C and A55: the Arrows of S2 cc= the Arrows of C and A56: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & m is epi; now let i be set; assume A57: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A58: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A58; thus (the Arrows of S1).i = (the Arrows of S2).i proof thus (the Arrows of S1).i c= (the Arrows of S2).i proof let n be set such that A59: n in (the Arrows of S1).i; (the Arrows of S1).i c= (the Arrows of C).i by A51,A52,A57,ALTCAT_2:def 2; then n in (the Arrows of C).i by A59; then n in (the Arrows of C).(o1,o2) by A58,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S1).(o1,o2) by A58,A59,BINOP_1:def 1; then <^o1,o2^> <> {} & m is epi by A53; then m in (the Arrows of S2).(o1,o2) by A56; hence n in (the Arrows of S2).i by A58,BINOP_1:def 1; end; let n be set such that A60: n in (the Arrows of S2).i; (the Arrows of S2).i c= (the Arrows of C).i by A54,A55,A57,ALTCAT_2:def 2; then n in (the Arrows of C).i by A60; then n in (the Arrows of C).(o1,o2) by A58,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S2).(o1,o2) by A58,A60,BINOP_1:def 1; then <^o1,o2^> <> {} & m is epi by A56; then m in (the Arrows of S1).(o1,o2) by A53; hence n in (the Arrows of S1).i by A58,BINOP_1:def 1; end; end; then the Arrows of S1 = the Arrows of S2 by A51,A54,PBOOLE:3; hence S1 = S2 by A51,A54,ALTCAT_2:27; end; end; definition let C be category; cluster AllEpi C -> id-inheriting; coherence proof now let o be object of AllEpi C, o' be object of C such that A1: o = o'; idm o' in (the Arrows of AllEpi C).(o,o) by A1,Def2; hence idm o' in <^o,o^> by ALTCAT_1:def 2; end; hence thesis by ALTCAT_2:def 14; end; end; definition let C be category; func AllRetr C -> strict non empty transitive SubCatStr of C means :Def3: the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction; existence proof set I = the carrier of C; defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction; A1: for i being set st i in [:I,I:] ex X being set st P[i,X] proof let i be set; assume i in [:I,I:]; then consider o1, o2 being set such that A2: o1 in I & o2 in I & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A2; defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = $1 & m is retraction; consider X being set such that A3: for x being set holds x in X iff x in (the Arrows of C).(o1,o2) & P[x] from Separation; take X; let x be set; thus x in X implies ex o1, o2 being object of C, m being Morphism of o1, o2 st i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction proof assume x in X; then consider m being Morphism of o1, o2 such that A4: <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is retraction by A3; take o1, o2, m; thus i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction by A2,A4; end; given p1, p2 being object of C, m being Morphism of p1, p2 such that A5: i = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is retraction; A6: o1 = p1 & o2 = p2 by A2,A5,ZFMISC_1:33; m in <^p1,p2^> by A5; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence x in X by A3,A5,A6; end; consider Ar being ManySortedSet of [:I,I:] such that A7: for i being set st i in [:I,I:] holds P[i,Ar.i] from MSSEx(A1); A8: Ar cc= the Arrows of C proof thus [:I,I:] c= [:the carrier of C,the carrier of C:]; let i be set; assume A9: i in [:I,I:]; let q be set; assume q in Ar.i; then consider p1, p2 being object of C, m being Morphism of p1, p2 such that A10: i = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is retraction by A7,A9; m in <^p1,p2^> by A10; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence q in (the Arrows of C).i by A10,BINOP_1:def 1; end; defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3] & $2 = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; A11: for i being set st i in [:I,I,I:] ex j being set st R[i,j] proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being set such that A12: p1 in I & p2 in I & p3 in I & i = [p1,p2,p3] by MCART_1:72; reconsider p1, p2, p3 as object of C by A12; take ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; take p1, p2, p3; thus i = [p1,p2,p3] by A12; thus thesis; end; consider Co being ManySortedSet of [:I,I,I:] such that A13: for i being set st i in [:I,I,I:] holds R[i,Co.i] from MSSEx(A11); Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|} proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being object of C such that A14: i = [p1,p2,p3] and A15: Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13; A16: (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] = {} by Lm1; [p2,p3] in [:I,I:] & [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then Ar.[p2,p3] c= (the Arrows of C).[p2,p3] & Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A8,ALTCAT_2:def 2; then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) & Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; then A17: Ar.(p2,p3) c= (the Arrows of C).(p2,p3) & Ar.(p1,p2) c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; A18: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {} proof assume A19: (the Arrows of C).(p1,p3) = {}; assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {}; then consider k being set such that A20: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1; consider u1, u2 being set such that A21: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) & k = [u1,u2] by A20,ZFMISC_1:def 2; u1 in (the Arrows of C).(p2,p3) & u2 in (the Arrows of C).(p1,p2) by A17,A21; then u1 in <^p2,p3^> & u2 in <^p1,p2^> by ALTCAT_1:def 2; then <^p1,p3^> <> {} by ALTCAT_1:def 4; hence contradiction by A19,ALTCAT_1:def 2; end; [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] by A17,ZFMISC_1:119; then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the Arrows of C).(p1,p3) by A15,A16,FUNCT_2:38; A22: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 5; A23: {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 6; A24: rng f c= {|Ar|}.i proof let q be set; assume q in rng f; then consider x being set such that A25: x in dom f and A26: q = f.x by FUNCT_1:def 5; A27: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A18,FUNCT_2:def 1; then consider m1, m2 being set such that A28: m1 in Ar.(p2,p3) & m2 in Ar.(p1,p2) and A29: x = [m1,m2] by A25,ZFMISC_1:103; A30: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by A28,BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A31: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & <^q3,q2^> <> {} & m1 = qq & qq is retraction by A7,A30; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A32: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & <^r2,r1^> <> {} & m2 = rr & rr is retraction by A7,A30; A33: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is retraction proof A34: r2 = p2 by A32,ZFMISC_1:33; A35: p2 = q2 by A31,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A32,ZFMISC_1:33; take r1, q3, mm * rr; A36: p1 = r1 & p3 = q3 by A31,A32,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus A37: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A31,A32,A34,A35,ALTCAT_1:def 4; thus q = (the Comp of C).(p1,p2,p3).x by A15,A25,A26,A27,FUNCT_1:72 .= (the Comp of C).(p1,p2,p3).(mm,rr) by A29,A31,A32,BINOP_1:def 1 .= mm * rr by A31,A32,A34,A35,A36,ALTCAT_1:def 10; thus mm * rr is retraction by A31,A32,A34,A35,A37,ALTCAT_3:18; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then q in Ar.[p1,p3] by A7,A33; then q in Ar.(p1,p3) by BINOP_1:def 1; hence q in {|Ar|}.i by A14,A22,MULTOP_1:def 1; end; [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A14,A23,MULTOP_1:def 1; hence Co.i is Function of {|Ar,Ar|}.i, {|Ar|}.i by A18,A24,FUNCT_2:8; end; then reconsider Co as BinComp of Ar; set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT; IT is SubCatStr of C proof thus the carrier of IT c= the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; thus [:J,J,J:] c= [:I,I,I:]; let i be set such that A38: i in [:J,J,J:]; let q be set such that A39: q in (the Comp of IT).i; consider p1, p2, p3 being object of C such that A40: i = [p1,p2,p3] & Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13,A38; ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] c= (the Comp of C).(p1,p2,p3) by RELAT_1:88; then q in (the Comp of C).(p1,p2,p3) by A39,A40; hence q in (the Comp of C).i by A40,MULTOP_1:def 1; end; then reconsider IT as strict non empty SubCatStr of C; IT is transitive proof let p1, p2, p3 be object of IT; assume A41: <^p1,p2^> <> {} & <^p2,p3^> <> {}; then consider m2 being set such that A42: m2 in <^p1,p2^> by XBOOLE_0:def 1; consider m1 being set such that A43: m1 in <^p2,p3^> by A41,XBOOLE_0:def 1; m2 in Ar.(p1,p2) & m1 in Ar.(p2,p3) by A42,A43,ALTCAT_1:def 2; then A44: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A45: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & <^q3,q2^> <> {} & m1 = qq & qq is retraction by A7,A44; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A46: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & <^r2,r1^> <> {} & m2 = rr & rr is retraction by A7,A44; A47: r2 = p2 by A46,ZFMISC_1:33; A48: p2 = q2 by A45,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A46,ZFMISC_1:33; A49: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is retraction proof take r1, q3, mm * rr; p1 = r1 & p3 = q3 by A45,A46,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus A50: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A45,A46,A47,A48,ALTCAT_1:def 4; thus mm * rr = mm * rr; thus mm * rr is retraction by A45,A46,A47,A48,A50,ALTCAT_3:18; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then mm * rr in Ar.[p1,p3] by A7,A49; then mm * rr in Ar.(p1,p3) by BINOP_1:def 1; hence <^p1,p3^> <> {} by ALTCAT_1:def 2; end; then reconsider IT as strict non empty transitive SubCatStr of C; take IT; thus the carrier of IT = the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; let o1, o2 be object of C, m be Morphism of o1, o2; A51: [o1,o2] in [:I,I:] by ZFMISC_1:def 2; thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction proof assume m in (the Arrows of IT).(o1,o2); then m in Ar.[o1,o2] by BINOP_1:def 1; then consider p1, p2 being object of C, n being Morphism of p1, p2 such that A52: [o1,o2] = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is retraction by A7,A51; o1 = p1 & o2 = p2 by A52,ZFMISC_1:33; hence <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction by A52; end; assume <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction; then m in (the Arrows of IT).[o1,o2] by A7,A51; hence m in (the Arrows of IT).(o1,o2) by BINOP_1:def 1; end; uniqueness proof let S1, S2 be strict non empty transitive SubCatStr of C such that A53: the carrier of S1 = the carrier of C and A54: the Arrows of S1 cc= the Arrows of C and A55: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction and A56: the carrier of S2 = the carrier of C and A57: the Arrows of S2 cc= the Arrows of C and A58: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction; now let i be set; assume A59: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A60: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A60; thus (the Arrows of S1).i = (the Arrows of S2).i proof thus (the Arrows of S1).i c= (the Arrows of S2).i proof let n be set such that A61: n in (the Arrows of S1).i; (the Arrows of S1).i c= (the Arrows of C).i by A53,A54,A59,ALTCAT_2:def 2; then n in (the Arrows of C).i by A61; then n in (the Arrows of C).(o1,o2) by A60,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S1).(o1,o2) by A60,A61,BINOP_1:def 1; then <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction by A55; then m in (the Arrows of S2).(o1,o2) by A58; hence n in (the Arrows of S2).i by A60,BINOP_1:def 1; end; let n be set such that A62: n in (the Arrows of S2).i; (the Arrows of S2).i c= (the Arrows of C).i by A56,A57,A59,ALTCAT_2:def 2; then n in (the Arrows of C).i by A62; then n in (the Arrows of C).(o1,o2) by A60,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S2).(o1,o2) by A60,A62,BINOP_1:def 1; then <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction by A58; then m in (the Arrows of S1).(o1,o2) by A55; hence n in (the Arrows of S1).i by A60,BINOP_1:def 1; end; end; then the Arrows of S1 = the Arrows of S2 by A53,A56,PBOOLE:3; hence S1 = S2 by A53,A56,ALTCAT_2:27; end; end; definition let C be category; cluster AllRetr C -> id-inheriting; coherence proof now let o be object of AllRetr C, o' be object of C such that A1: o = o'; idm o' in (the Arrows of AllRetr C).(o,o) by A1,Def3; hence idm o' in <^o,o^> by ALTCAT_1:def 2; end; hence thesis by ALTCAT_2:def 14; end; end; definition let C be category; func AllCoretr C -> strict non empty transitive SubCatStr of C means :Def4: the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction; existence proof set I = the carrier of C; defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is coretraction; A1: for i being set st i in [:I,I:] ex X being set st P[i,X] proof let i be set; assume i in [:I,I:]; then consider o1, o2 being set such that A2: o1 in I & o2 in I & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A2; defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = $1 & m is coretraction; consider X being set such that A3: for x being set holds x in X iff x in (the Arrows of C).(o1,o2) & P[x] from Separation; take X; let x be set; thus x in X implies ex o1, o2 being object of C, m being Morphism of o1, o2 st i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is coretraction proof assume x in X; then consider m being Morphism of o1, o2 such that A4: <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is coretraction by A3; take o1, o2, m; thus i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is coretraction by A2,A4; end; given p1, p2 being object of C, m being Morphism of p1, p2 such that A5: i = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is coretraction; A6: o1 = p1 & o2 = p2 by A2,A5,ZFMISC_1:33; m in <^p1,p2^> by A5; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence x in X by A3,A5,A6; end; consider Ar being ManySortedSet of [:I,I:] such that A7: for i being set st i in [:I,I:] holds P[i,Ar.i] from MSSEx(A1); A8: Ar cc= the Arrows of C proof thus [:I,I:] c= [:the carrier of C,the carrier of C:]; let i be set; assume A9: i in [:I,I:]; let q be set; assume q in Ar.i; then consider p1, p2 being object of C, m being Morphism of p1, p2 such that A10: i = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is coretraction by A7,A9; m in <^p1,p2^> by A10; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence q in (the Arrows of C).i by A10,BINOP_1:def 1; end; defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3] & $2 = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; A11: for i being set st i in [:I,I,I:] ex j being set st R[i,j] proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being set such that A12: p1 in I & p2 in I & p3 in I & i = [p1,p2,p3] by MCART_1:72; reconsider p1, p2, p3 as object of C by A12; take ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; take p1, p2, p3; thus i = [p1,p2,p3] by A12; thus thesis; end; consider Co being ManySortedSet of [:I,I,I:] such that A13: for i being set st i in [:I,I,I:] holds R[i,Co.i] from MSSEx(A11); Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|} proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being object of C such that A14: i = [p1,p2,p3] and A15: Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13; A16: (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] = {} by Lm1; [p2,p3] in [:I,I:] & [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then Ar.[p2,p3] c= (the Arrows of C).[p2,p3] & Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A8,ALTCAT_2:def 2; then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) & Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; then A17: Ar.(p2,p3) c= (the Arrows of C).(p2,p3) & Ar.(p1,p2) c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; A18: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {} proof assume A19: (the Arrows of C).(p1,p3) = {}; assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {}; then consider k being set such that A20: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1; consider u1, u2 being set such that A21: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) & k = [u1,u2] by A20,ZFMISC_1:def 2; u1 in (the Arrows of C).(p2,p3) & u2 in (the Arrows of C).(p1,p2) by A17,A21; then u1 in <^p2,p3^> & u2 in <^p1,p2^> by ALTCAT_1:def 2; then <^p1,p3^> <> {} by ALTCAT_1:def 4; hence contradiction by A19,ALTCAT_1:def 2; end; [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] by A17,ZFMISC_1:119; then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the Arrows of C).(p1,p3) by A15,A16,FUNCT_2:38; A22: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 5; A23: {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 6; A24: rng f c= {|Ar|}.i proof let q be set; assume q in rng f; then consider x being set such that A25: x in dom f and A26: q = f.x by FUNCT_1:def 5; A27: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A18,FUNCT_2:def 1; then consider m1, m2 being set such that A28: m1 in Ar.(p2,p3) & m2 in Ar.(p1,p2) and A29: x = [m1,m2] by A25,ZFMISC_1:103; A30: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by A28,BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A31: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & <^q3,q2^> <> {} & m1 = qq & qq is coretraction by A7,A30; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A32: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & <^r2,r1^> <> {} & m2 = rr & rr is coretraction by A7,A30; A33: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is coretraction proof A34: r2 = p2 by A32,ZFMISC_1:33; A35: p2 = q2 by A31,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A32,ZFMISC_1:33; take r1, q3, mm * rr; A36: p1 = r1 & p3 = q3 by A31,A32,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus A37: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A31,A32,A34,A35,ALTCAT_1:def 4; thus q = (the Comp of C).(p1,p2,p3).x by A15,A25,A26,A27,FUNCT_1:72 .= (the Comp of C).(p1,p2,p3).(mm,rr) by A29,A31,A32,BINOP_1:def 1 .= mm * rr by A31,A32,A34,A35,A36,ALTCAT_1:def 10; thus mm * rr is coretraction by A31,A32,A34,A35,A37,ALTCAT_3:19; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then q in Ar.[p1,p3] by A7,A33; then q in Ar.(p1,p3) by BINOP_1:def 1; hence q in {|Ar|}.i by A14,A22,MULTOP_1:def 1; end; [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A14,A23,MULTOP_1:def 1; hence Co.i is Function of {|Ar,Ar|}.i, {|Ar|}.i by A18,A24,FUNCT_2:8; end; then reconsider Co as BinComp of Ar; set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT; IT is SubCatStr of C proof thus the carrier of IT c= the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; thus [:J,J,J:] c= [:I,I,I:]; let i be set such that A38: i in [:J,J,J:]; let q be set such that A39: q in (the Comp of IT).i; consider p1, p2, p3 being object of C such that A40: i = [p1,p2,p3] & Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13,A38; ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] c= (the Comp of C).(p1,p2,p3) by RELAT_1:88; then q in (the Comp of C).(p1,p2,p3) by A39,A40; hence q in (the Comp of C).i by A40,MULTOP_1:def 1; end; then reconsider IT as strict non empty SubCatStr of C; IT is transitive proof let p1, p2, p3 be object of IT; assume A41: <^p1,p2^> <> {} & <^p2,p3^> <> {}; then consider m2 being set such that A42: m2 in <^p1,p2^> by XBOOLE_0:def 1; consider m1 being set such that A43: m1 in <^p2,p3^> by A41,XBOOLE_0:def 1; m2 in Ar.(p1,p2) & m1 in Ar.(p2,p3) by A42,A43,ALTCAT_1:def 2; then A44: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A45: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & <^q3,q2^> <> {} & m1 = qq & qq is coretraction by A7,A44; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A46: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & <^r2,r1^> <> {} & m2 = rr & rr is coretraction by A7,A44; A47: r2 = p2 by A46,ZFMISC_1:33; A48: p2 = q2 by A45,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A46,ZFMISC_1:33; A49: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is coretraction proof take r1, q3, mm * rr; p1 = r1 & p3 = q3 by A45,A46,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus A50: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A45,A46,A47,A48,ALTCAT_1:def 4; thus mm * rr = mm * rr; thus mm * rr is coretraction by A45,A46,A47,A48,A50,ALTCAT_3:19; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then mm * rr in Ar.[p1,p3] by A7,A49; then mm * rr in Ar.(p1,p3) by BINOP_1:def 1; hence <^p1,p3^> <> {} by ALTCAT_1:def 2; end; then reconsider IT as strict non empty transitive SubCatStr of C; take IT; thus the carrier of IT = the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; let o1, o2 be object of C, m be Morphism of o1, o2; A51: [o1,o2] in [:I,I:] by ZFMISC_1:def 2; thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction proof assume m in (the Arrows of IT).(o1,o2); then m in Ar.[o1,o2] by BINOP_1:def 1; then consider p1, p2 being object of C, n being Morphism of p1, p2 such that A52: [o1,o2] = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is coretraction by A7,A51; o1 = p1 & o2 = p2 by A52,ZFMISC_1:33; hence <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction by A52; end; assume <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction; then m in (the Arrows of IT).[o1,o2] by A7,A51; hence m in (the Arrows of IT).(o1,o2) by BINOP_1:def 1; end; uniqueness proof let S1, S2 be strict non empty transitive SubCatStr of C such that A53: the carrier of S1 = the carrier of C and A54: the Arrows of S1 cc= the Arrows of C and A55: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction and A56: the carrier of S2 = the carrier of C and A57: the Arrows of S2 cc= the Arrows of C and A58: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction; now let i be set; assume A59: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A60: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A60; thus (the Arrows of S1).i = (the Arrows of S2).i proof thus (the Arrows of S1).i c= (the Arrows of S2).i proof let n be set such that A61: n in (the Arrows of S1).i; (the Arrows of S1).i c= (the Arrows of C).i by A53,A54,A59,ALTCAT_2:def 2; then n in (the Arrows of C).i by A61; then n in (the Arrows of C).(o1,o2) by A60,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S1).(o1,o2) by A60,A61,BINOP_1:def 1; then <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction by A55; then m in (the Arrows of S2).(o1,o2) by A58; hence n in (the Arrows of S2).i by A60,BINOP_1:def 1; end; let n be set such that A62: n in (the Arrows of S2).i; (the Arrows of S2).i c= (the Arrows of C).i by A56,A57,A59,ALTCAT_2:def 2; then n in (the Arrows of C).i by A62; then n in (the Arrows of C).(o1,o2) by A60,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S2).(o1,o2) by A60,A62,BINOP_1:def 1; then <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction by A58; then m in (the Arrows of S1).(o1,o2) by A55; hence n in (the Arrows of S1).i by A60,BINOP_1:def 1; end; end; then the Arrows of S1 = the Arrows of S2 by A53,A56,PBOOLE:3; hence S1 = S2 by A53,A56,ALTCAT_2:27; end; end; definition let C be category; cluster AllCoretr C -> id-inheriting; coherence proof now let o be object of AllCoretr C, o' be object of C such that A1: o = o'; idm o' in (the Arrows of AllCoretr C).(o,o) by A1,Def4; hence idm o' in <^o,o^> by ALTCAT_1:def 2; end; hence thesis by ALTCAT_2:def 14; end; end; definition let C be category; func AllIso C -> strict non empty transitive SubCatStr of C means :Def5: the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso; existence proof set I = the carrier of C; defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is iso; A1: for i being set st i in [:I,I:] ex X being set st P[i,X] proof let i be set; assume i in [:I,I:]; then consider o1, o2 being set such that A2: o1 in I & o2 in I & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A2; defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = $1 & m is iso; consider X being set such that A3: for x being set holds x in X iff x in (the Arrows of C).(o1,o2) & P[x] from Separation; take X; let x be set; thus x in X implies ex o1, o2 being object of C, m being Morphism of o1, o2 st i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is iso proof assume x in X; then consider m being Morphism of o1, o2 such that A4: <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is iso by A3; take o1, o2, m; thus i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is iso by A2,A4; end; given p1, p2 being object of C, m being Morphism of p1, p2 such that A5: i = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is iso; A6: o1 = p1 & o2 = p2 by A2,A5,ZFMISC_1:33; m in <^p1,p2^> by A5; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence x in X by A3,A5,A6; end; consider Ar being ManySortedSet of [:I,I:] such that A7: for i being set st i in [:I,I:] holds P[i,Ar.i] from MSSEx(A1); A8: Ar cc= the Arrows of C proof thus [:I,I:] c= [:the carrier of C,the carrier of C:]; let i be set; assume A9: i in [:I,I:]; let q be set; assume q in Ar.i; then consider p1, p2 being object of C, m being Morphism of p1, p2 such that A10: i = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is iso by A7,A9; m in <^p1,p2^> by A10; then m in (the Arrows of C).(p1,p2) by ALTCAT_1:def 2; hence q in (the Arrows of C).i by A10,BINOP_1:def 1; end; defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3] & $2 = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; A11: for i being set st i in [:I,I,I:] ex j being set st R[i,j] proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being set such that A12: p1 in I & p2 in I & p3 in I & i = [p1,p2,p3] by MCART_1:72; reconsider p1, p2, p3 as object of C by A12; take ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):]; take p1, p2, p3; thus i = [p1,p2,p3] by A12; thus thesis; end; consider Co being ManySortedSet of [:I,I,I:] such that A13: for i being set st i in [:I,I,I:] holds R[i,Co.i] from MSSEx(A11); Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|} proof let i be set; assume i in [:I,I,I:]; then consider p1, p2, p3 being object of C such that A14: i = [p1,p2,p3] and A15: Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13; A16: (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] = {} by Lm1; [p2,p3] in [:I,I:] & [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then Ar.[p2,p3] c= (the Arrows of C).[p2,p3] & Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A8,ALTCAT_2:def 2; then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) & Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; then A17: Ar.(p2,p3) c= (the Arrows of C).(p2,p3) & Ar.(p1,p2) c= (the Arrows of C).(p1,p2) by BINOP_1:def 1; A18: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {} proof assume A19: (the Arrows of C).(p1,p3) = {}; assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {}; then consider k being set such that A20: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1; consider u1, u2 being set such that A21: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) & k = [u1,u2] by A20,ZFMISC_1:def 2; u1 in (the Arrows of C).(p2,p3) & u2 in (the Arrows of C).(p1,p2) by A17,A21; then u1 in <^p2,p3^> & u2 in <^p1,p2^> by ALTCAT_1:def 2; then <^p1,p3^> <> {} by ALTCAT_1:def 4; hence contradiction by A19,ALTCAT_1:def 2; end; [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] by A17,ZFMISC_1:119; then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the Arrows of C).(p1,p3) by A15,A16,FUNCT_2:38; A22: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 5; A23: {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 6; A24: rng f c= {|Ar|}.i proof let q be set; assume q in rng f; then consider x being set such that A25: x in dom f and A26: q = f.x by FUNCT_1:def 5; A27: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A18,FUNCT_2:def 1; then consider m1, m2 being set such that A28: m1 in Ar.(p2,p3) & m2 in Ar.(p1,p2) and A29: x = [m1,m2] by A25,ZFMISC_1:103; A30: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by A28,BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A31: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & <^q3,q2^> <> {} & m1 = qq & qq is iso by A7,A30; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A32: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & <^r2,r1^> <> {} & m2 = rr & rr is iso by A7,A30; A33: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is iso proof A34: r2 = p2 by A32,ZFMISC_1:33; A35: p2 = q2 by A31,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A32,ZFMISC_1:33; take r1, q3, mm * rr; A36: p1 = r1 & p3 = q3 by A31,A32,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus A37: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A31,A32,A34,A35,ALTCAT_1:def 4; thus q = (the Comp of C).(p1,p2,p3).x by A15,A25,A26,A27,FUNCT_1:72 .= (the Comp of C).(p1,p2,p3).(mm,rr) by A29,A31,A32,BINOP_1:def 1 .= mm * rr by A31,A32,A34,A35,A36,ALTCAT_1:def 10; thus mm * rr is iso by A31,A32,A34,A35,A37,ALTCAT_3:7; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then q in Ar.[p1,p3] by A7,A33; then q in Ar.(p1,p3) by BINOP_1:def 1; hence q in {|Ar|}.i by A14,A22,MULTOP_1:def 1; end; [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A14,A23,MULTOP_1:def 1; hence Co.i is Function of {|Ar,Ar|}.i, {|Ar|}.i by A18,A24,FUNCT_2:8; end; then reconsider Co as BinComp of Ar; set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT; IT is SubCatStr of C proof thus the carrier of IT c= the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; thus [:J,J,J:] c= [:I,I,I:]; let i be set such that A38: i in [:J,J,J:]; let q be set such that A39: q in (the Comp of IT).i; consider p1, p2, p3 being object of C such that A40: i = [p1,p2,p3] & Co.i = ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] by A13,A38; ((the Comp of C).(p1,p2,p3))|[:Ar.(p2,p3),Ar.(p1,p2):] c= (the Comp of C).(p1,p2,p3) by RELAT_1:88; then q in (the Comp of C).(p1,p2,p3) by A39,A40; hence q in (the Comp of C).i by A40,MULTOP_1:def 1; end; then reconsider IT as strict non empty SubCatStr of C; IT is transitive proof let p1, p2, p3 be object of IT; assume A41: <^p1,p2^> <> {} & <^p2,p3^> <> {}; then consider m2 being set such that A42: m2 in <^p1,p2^> by XBOOLE_0:def 1; consider m1 being set such that A43: m1 in <^p2,p3^> by A41,XBOOLE_0:def 1; m2 in Ar.(p1,p2) & m1 in Ar.(p2,p3) by A42,A43,ALTCAT_1:def 2; then A44: m1 in Ar.[p2,p3] & m2 in Ar.[p1,p2] by BINOP_1:def 1; [p2,p3] in [:I,I:] by ZFMISC_1:def 2; then consider q2, q3 being object of C, qq being Morphism of q2, q3 such that A45: [p2,p3] = [q2,q3] & <^q2,q3^> <> {} & <^q3,q2^> <> {} & m1 = qq & qq is iso by A7,A44; [p1,p2] in [:I,I:] by ZFMISC_1:def 2; then consider r1, r2 being object of C, rr being Morphism of r1, r2 such that A46: [p1,p2] = [r1,r2] & <^r1,r2^> <> {} & <^r2,r1^> <> {} & m2 = rr & rr is iso by A7,A44; A47: r2 = p2 by A46,ZFMISC_1:33; A48: p2 = q2 by A45,ZFMISC_1:33; then reconsider mm = qq as Morphism of r2, q3 by A46,ZFMISC_1:33; A49: ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is iso proof take r1, q3, mm * rr; p1 = r1 & p3 = q3 by A45,A46,ZFMISC_1:33; hence [p1,p3] = [r1,q3]; thus A50: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A45,A46,A47,A48,ALTCAT_1:def 4; thus mm * rr = mm * rr; thus mm * rr is iso by A45,A46,A47,A48,A50,ALTCAT_3:7; end; [p1,p3] in [:I,I:] by ZFMISC_1:def 2; then mm * rr in Ar.[p1,p3] by A7,A49; then mm * rr in Ar.(p1,p3) by BINOP_1:def 1; hence <^p1,p3^> <> {} by ALTCAT_1:def 2; end; then reconsider IT as strict non empty transitive SubCatStr of C; take IT; thus the carrier of IT = the carrier of C; thus the Arrows of IT cc= the Arrows of C by A8; let o1, o2 be object of C, m be Morphism of o1, o2; A51: [o1,o2] in [:I,I:] by ZFMISC_1:def 2; thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso proof assume m in (the Arrows of IT).(o1,o2); then m in Ar.[o1,o2] by BINOP_1:def 1; then consider p1, p2 being object of C, n being Morphism of p1, p2 such that A52: [o1,o2] = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is iso by A7,A51; o1 = p1 & o2 = p2 by A52,ZFMISC_1:33; hence <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso by A52; end; assume <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso; then m in (the Arrows of IT).[o1,o2] by A7,A51; hence m in (the Arrows of IT).(o1,o2) by BINOP_1:def 1; end; uniqueness proof let S1, S2 be strict non empty transitive SubCatStr of C such that A53: the carrier of S1 = the carrier of C and A54: the Arrows of S1 cc= the Arrows of C and A55: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso and A56: the carrier of S2 = the carrier of C and A57: the Arrows of S2 cc= the Arrows of C and A58: for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso; now let i be set; assume A59: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A60: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A60; thus (the Arrows of S1).i = (the Arrows of S2).i proof thus (the Arrows of S1).i c= (the Arrows of S2).i proof let n be set such that A61: n in (the Arrows of S1).i; (the Arrows of S1).i c= (the Arrows of C).i by A53,A54,A59,ALTCAT_2:def 2; then n in (the Arrows of C).i by A61; then n in (the Arrows of C).(o1,o2) by A60,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S1).(o1,o2) by A60,A61,BINOP_1:def 1; then <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso by A55; then m in (the Arrows of S2).(o1,o2) by A58; hence n in (the Arrows of S2).i by A60,BINOP_1:def 1; end; let n be set such that A62: n in (the Arrows of S2).i; (the Arrows of S2).i c= (the Arrows of C).i by A56,A57,A59,ALTCAT_2:def 2; then n in (the Arrows of C).i by A62; then n in (the Arrows of C).(o1,o2) by A60,BINOP_1:def 1; then n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m = n as Morphism of o1, o2 ; m in (the Arrows of S2).(o1,o2) by A60,A62,BINOP_1:def 1; then <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso by A58; then m in (the Arrows of S1).(o1,o2) by A55; hence n in (the Arrows of S1).i by A60,BINOP_1:def 1; end; end; then the Arrows of S1 = the Arrows of S2 by A53,A56,PBOOLE:3; hence S1 = S2 by A53,A56,ALTCAT_2:27; end; end; definition let C be category; cluster AllIso C -> id-inheriting; coherence proof now let o be object of AllIso C, o' be object of C such that A1: o = o'; idm o' in (the Arrows of AllIso C).(o,o) by A1,Def5; hence idm o' in <^o,o^> by ALTCAT_1:def 2; end; hence thesis by ALTCAT_2:def 14; end; end; theorem Th41: AllIso C is non empty subcategory of AllRetr C proof A1: the carrier of AllIso C = the carrier of C by Def5; then A2: the carrier of AllIso C c= the carrier of AllRetr C by Def3; AllIso C is SubCatStr of AllRetr C proof the Arrows of AllIso C cc= the Arrows of AllRetr C proof thus [:the carrier of AllIso C,the carrier of AllIso C:] c= [:the carrier of AllRetr C,the carrier of AllRetr C:] by A2,ZFMISC_1:119; let i be set; assume A3: i in [:the carrier of AllIso C,the carrier of AllIso C:]; then consider o1, o2 being set such that A4: o1 in the carrier of AllIso C & o2 in the carrier of AllIso C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A1,A4; let m be set; assume A5: m in (the Arrows of AllIso C).i; then A6: m in (the Arrows of AllIso C).(o1,o2) by A4,BINOP_1:def 1; 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 A3,A4,ALTCAT_2:def 2; then (the Arrows of AllIso C).[o1,o2] c= (the Arrows of C).(o1,o2) by BINOP_1:def 1; then (the Arrows of AllIso C).(o1,o2) c= (the Arrows of C).(o1,o2) by BINOP_1:def 1; then m in (the Arrows of C).(o1,o2) by A6; then m in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m1 = m as Morphism of o1, o2 ; m1 in (the Arrows of AllIso C).(o1,o2) by A4,A5,BINOP_1:def 1; then A7: <^o1,o2^> <> {} & <^o2,o1^> <> {} by Def5; m1 is iso by A6,Def5; then m1 is retraction by ALTCAT_3:5; then m in (the Arrows of AllRetr C).(o1,o2) by A7,Def3; hence m in (the Arrows of AllRetr C).i by A4,BINOP_1:def 1; end; hence thesis by A2,ALTCAT_2:25; end; then reconsider A = AllIso C as with_units (non empty SubCatStr of AllRetr C); A is id-inheriting proof now let o be object of A, o1 be object of AllRetr C such that A8: o = o1; reconsider oo = o as object of C by A1; idm o = idm oo by ALTCAT_2:35 .= idm o1 by A8,ALTCAT_2:35; hence idm o1 in <^o,o^>; end; hence thesis by ALTCAT_2:def 14; end; hence AllIso C is non empty subcategory of AllRetr C; end; theorem Th42: AllIso C is non empty subcategory of AllCoretr C proof A1: the carrier of AllIso C = the carrier of C by Def5; then A2: the carrier of AllIso C c= the carrier of AllCoretr C by Def4; AllIso C is SubCatStr of AllCoretr C proof the Arrows of AllIso C cc= the Arrows of AllCoretr C proof thus [:the carrier of AllIso C,the carrier of AllIso C:] c= [:the carrier of AllCoretr C,the carrier of AllCoretr C:] by A2,ZFMISC_1:119; let i be set; assume A3: i in [:the carrier of AllIso C,the carrier of AllIso C:]; then consider o1, o2 being set such that A4: o1 in the carrier of AllIso C & o2 in the carrier of AllIso C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A1,A4; let m be set; assume A5: m in (the Arrows of AllIso C).i; then A6: m in (the Arrows of AllIso C).(o1,o2) by A4,BINOP_1:def 1; 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 A3,A4,ALTCAT_2:def 2; then (the Arrows of AllIso C).[o1,o2] c= (the Arrows of C).(o1,o2) by BINOP_1:def 1; then (the Arrows of AllIso C).(o1,o2) c= (the Arrows of C).(o1,o2) by BINOP_1:def 1; then m in (the Arrows of C).(o1,o2) by A6; then m in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m1 = m as Morphism of o1, o2 ; m1 in (the Arrows of AllIso C).(o1,o2) by A4,A5,BINOP_1:def 1; then A7: <^o1,o2^> <> {} & <^o2,o1^> <> {} by Def5; m1 is iso by A6,Def5; then m1 is coretraction by ALTCAT_3:5; then m in (the Arrows of AllCoretr C).(o1,o2) by A7,Def4; hence m in (the Arrows of AllCoretr C).i by A4,BINOP_1:def 1; end; hence thesis by A2,ALTCAT_2:25; end; then reconsider A = AllIso C as with_units (non empty SubCatStr of AllCoretr C); A is id-inheriting proof now let o be object of A, o1 be object of AllCoretr C such that A8: o = o1; reconsider oo = o as object of C by A1; idm o = idm oo by ALTCAT_2:35 .= idm o1 by A8,ALTCAT_2:35; hence idm o1 in <^o,o^>; end; hence thesis by ALTCAT_2:def 14; end; hence AllIso C is non empty subcategory of AllCoretr C; end; theorem Th43: AllCoretr C is non empty subcategory of AllMono C proof A1: the carrier of AllCoretr C = the carrier of C by Def4; then A2: the carrier of AllCoretr C c= the carrier of AllMono C by Def1; AllCoretr C is SubCatStr of AllMono C proof the Arrows of AllCoretr C cc= the Arrows of AllMono C proof thus [:the carrier of AllCoretr C,the carrier of AllCoretr C:] c= [:the carrier of AllMono C,the carrier of AllMono C:] by A2,ZFMISC_1:119; let i be set; assume A3: i in [:the carrier of AllCoretr C,the carrier of AllCoretr C:]; then consider o1, o2 being set such that A4: o1 in the carrier of AllCoretr C & o2 in the carrier of AllCoretr C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A1,A4; let m be set; assume A5: m in (the Arrows of AllCoretr C).i; then A6: m in (the Arrows of AllCoretr C).(o1,o2) by A4,BINOP_1:def 1; the Arrows of AllCoretr C cc= the Arrows of C by Def4; then (the Arrows of AllCoretr C).[o1,o2] c= (the Arrows of C).[o1,o2] by A3,A4,ALTCAT_2:def 2; then (the Arrows of AllCoretr C).[o1,o2] c= (the Arrows of C).(o1,o2) by BINOP_1:def 1; then (the Arrows of AllCoretr C).(o1,o2) c= (the Arrows of C).(o1,o2) by BINOP_1:def 1; then m in (the Arrows of C).(o1,o2) by A6; then m in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m1 = m as Morphism of o1, o2 ; m1 in (the Arrows of AllCoretr C).(o1,o2) by A4,A5,BINOP_1:def 1; then A7: <^o1,o2^> <> {} & <^o2,o1^> <> {} by Def4; m1 is coretraction by A6,Def4; then m1 is mono by A7,ALTCAT_3:16; then m in (the Arrows of AllMono C).(o1,o2) by A7,Def1; hence m in (the Arrows of AllMono C).i by A4,BINOP_1:def 1; end; hence thesis by A2,ALTCAT_2:25; end; then reconsider A = AllCoretr C as with_units (non empty SubCatStr of AllMono C); A is id-inheriting proof now let o be object of A, o1 be object of AllMono C such that A8: o = o1; reconsider oo = o as object of C by A1; idm o = idm oo by ALTCAT_2:35 .= idm o1 by A8,ALTCAT_2:35; hence idm o1 in <^o,o^>; end; hence thesis by ALTCAT_2:def 14; end; hence AllCoretr C is non empty subcategory of AllMono C; end; theorem Th44: AllRetr C is non empty subcategory of AllEpi C proof A1: the carrier of AllRetr C = the carrier of C by Def3; then A2: the carrier of AllRetr C c= the carrier of AllEpi C by Def2; AllRetr C is SubCatStr of AllEpi C proof the Arrows of AllRetr C cc= the Arrows of AllEpi C proof thus [:the carrier of AllRetr C,the carrier of AllRetr C:] c= [:the carrier of AllEpi C,the carrier of AllEpi C:] by A2,ZFMISC_1:119; let i be set; assume A3: i in [:the carrier of AllRetr C,the carrier of AllRetr C:]; then consider o1, o2 being set such that A4: o1 in the carrier of AllRetr C & o2 in the carrier of AllRetr C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A1,A4; let m be set; assume A5: m in (the Arrows of AllRetr C).i; then A6: m in (the Arrows of AllRetr C).(o1,o2) by A4,BINOP_1:def 1; the Arrows of AllRetr C cc= the Arrows of C by Def3; then (the Arrows of AllRetr C).[o1,o2] c= (the Arrows of C).[o1,o2] by A3,A4,ALTCAT_2:def 2; then (the Arrows of AllRetr C).[o1,o2] c= (the Arrows of C).(o1,o2) by BINOP_1:def 1; then (the Arrows of AllRetr C).(o1,o2) c= (the Arrows of C).(o1,o2) by BINOP_1:def 1; then m in (the Arrows of C).(o1,o2) by A6; then m in <^o1,o2^> by ALTCAT_1:def 2; then reconsider m1 = m as Morphism of o1, o2 ; m1 in (the Arrows of AllRetr C).(o1,o2) by A4,A5,BINOP_1:def 1; then A7: <^o1,o2^> <> {} & <^o2,o1^> <> {} by Def3; m1 is retraction by A6,Def3; then m1 is epi by A7,ALTCAT_3:15; then m in (the Arrows of AllEpi C).(o1,o2) by A7,Def2; hence m in (the Arrows of AllEpi C).i by A4,BINOP_1:def 1; end; hence thesis by A2,ALTCAT_2:25; end; then reconsider A = AllRetr C as with_units (non empty SubCatStr of AllEpi C); A is id-inheriting proof now let o be object of A, o1 be object of AllEpi C such that A8: o = o1; reconsider oo = o as object of C by A1; idm o = idm oo by ALTCAT_2:35 .= idm o1 by A8,ALTCAT_2:35; hence idm o1 in <^o,o^>; end; hence thesis by ALTCAT_2:def 14; end; hence AllRetr C is non empty subcategory of AllEpi C; end; theorem (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is mono) implies the AltCatStr of C = AllMono C proof assume A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is mono; A2: the carrier of AllMono C = the carrier of the AltCatStr of C by Def1; A3: the Arrows of AllMono C cc= the Arrows of C by Def1; now let i be set; assume A4: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A5: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A5; thus (the Arrows of AllMono C).i = (the Arrows of C).i proof thus (the Arrows of AllMono C).i c= (the Arrows of C).i by A2,A3,A4,ALTCAT_2:def 2; let n be set; assume n in (the Arrows of C).i; then n in (the Arrows of C).(o1,o2) by A5,BINOP_1:def 1; then A6: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; n1 is mono by A1; then n in (the Arrows of AllMono C).(o1,o2) by A6,Def1; hence n in (the Arrows of AllMono C).i by A5,BINOP_1:def 1; end; end; then the Arrows of AllMono C = the Arrows of the AltCatStr of C by A2, PBOOLE:3; hence the AltCatStr of C = AllMono C by A2,ALTCAT_2:26; end; theorem (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is epi) implies the AltCatStr of C = AllEpi C proof assume A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is epi; A2: the carrier of AllEpi C = the carrier of the AltCatStr of C by Def2; A3: the Arrows of AllEpi C cc= the Arrows of C by Def2; now let i be set; assume A4: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A5: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A5; thus (the Arrows of AllEpi C).i = (the Arrows of C).i proof thus (the Arrows of AllEpi C).i c= (the Arrows of C).i by A2,A3,A4,ALTCAT_2:def 2; let n be set; assume n in (the Arrows of C).i; then n in (the Arrows of C).(o1,o2) by A5,BINOP_1:def 1; then A6: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; n1 is epi by A1; then n in (the Arrows of AllEpi C).(o1,o2) by A6,Def2; hence n in (the Arrows of AllEpi C).i by A5,BINOP_1:def 1; end; end; then the Arrows of AllEpi C = the Arrows of the AltCatStr of C by A2,PBOOLE :3; hence the AltCatStr of C = AllEpi C by A2,ALTCAT_2:26; end; theorem (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is retraction & <^o2,o1^> <> {}) implies the AltCatStr of C = AllRetr C proof assume A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is retraction & <^o2,o1^> <> {}; A2: the carrier of AllRetr C = the carrier of the AltCatStr of C by Def3; A3: the Arrows of AllRetr C cc= the Arrows of C by Def3; now let i be set; assume A4: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A5: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A5; thus (the Arrows of AllRetr C).i = (the Arrows of C).i proof thus (the Arrows of AllRetr C).i c= (the Arrows of C).i by A2,A3,A4,ALTCAT_2:def 2; let n be set; assume n in (the Arrows of C).i; then n in (the Arrows of C).(o1,o2) by A5,BINOP_1:def 1; then A6: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; <^o2,o1^> <> {} & n1 is retraction by A1; then n in (the Arrows of AllRetr C).(o1,o2) by A6,Def3; hence n in (the Arrows of AllRetr C).i by A5,BINOP_1:def 1; end; end; then the Arrows of AllRetr C = the Arrows of the AltCatStr of C by A2, PBOOLE:3; hence the AltCatStr of C = AllRetr C by A2,ALTCAT_2:26; end; theorem (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is coretraction & <^o2,o1^> <> {}) implies the AltCatStr of C = AllCoretr C proof assume A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is coretraction & <^o2,o1^> <> {}; A2: the carrier of AllCoretr C = the carrier of the AltCatStr of C by Def4; A3: the Arrows of AllCoretr C cc= the Arrows of C by Def4; now let i be set; assume A4: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A5: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A5; thus (the Arrows of AllCoretr C).i = (the Arrows of C).i proof thus (the Arrows of AllCoretr C).i c= (the Arrows of C).i by A2,A3,A4,ALTCAT_2:def 2; let n be set; assume n in (the Arrows of C).i; then n in (the Arrows of C).(o1,o2) by A5,BINOP_1:def 1; then A6: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; <^o2,o1^> <> {} & n1 is coretraction by A1; then n in (the Arrows of AllCoretr C).(o1,o2) by A6,Def4; hence n in (the Arrows of AllCoretr C).i by A5,BINOP_1:def 1; end; end; then the Arrows of AllCoretr C = the Arrows of the AltCatStr of C by A2,PBOOLE:3; hence the AltCatStr of C = AllCoretr C by A2,ALTCAT_2:26; end; theorem (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is iso & <^o2,o1^> <> {}) implies the AltCatStr of C = AllIso C proof assume A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is iso & <^o2,o1^> <> {}; A2: the carrier of AllIso C = the carrier of the AltCatStr of C by Def5; A3: the Arrows of AllIso C cc= the Arrows of C by Def5; now let i be set; assume A4: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A5: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of C by A5; thus (the Arrows of AllIso C).i = (the Arrows of C).i proof thus (the Arrows of AllIso C).i c= (the Arrows of C).i by A2,A3,A4,ALTCAT_2:def 2; let n be set; assume n in (the Arrows of C).i; then n in (the Arrows of C).(o1,o2) by A5,BINOP_1:def 1; then A6: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; <^o2,o1^> <> {} & n1 is iso by A1; then n in (the Arrows of AllIso C).(o1,o2) by A6,Def5; hence n in (the Arrows of AllIso C).i by A5,BINOP_1:def 1; end; end; then the Arrows of AllIso C = the Arrows of the AltCatStr of C by A2,PBOOLE :3; hence the AltCatStr of C = AllIso C by A2,ALTCAT_2:26; end; theorem Th50: for o1, o2 being object of AllMono C for m being Morphism of o1, o2 st <^o1,o2^> <> {} holds m is mono proof let o1, o2 be object of AllMono C, m be Morphism of o1, o2 such that A1: <^o1,o2^> <> {}; the carrier of AllMono C = the carrier of C by Def1; then reconsider p1 = o1, p2 = o2 as object of C; reconsider p = m as Morphism of p1, p2 by A1,ALTCAT_2:34; m in <^o1,o2^> by A1; then p in (the Arrows of AllMono C).(o1,o2) by ALTCAT_1:def 2; then <^p1,p2^> <> {} & p is mono by Def1; hence m is mono by A1,Th37; end; theorem Th51: for o1, o2 being object of AllEpi C for m being Morphism of o1, o2 st <^o1,o2^> <> {} holds m is epi proof let o1, o2 be object of AllEpi C, m be Morphism of o1, o2 such that A1: <^o1,o2^> <> {}; the carrier of AllEpi C = the carrier of C by Def2; then reconsider p1 = o1, p2 = o2 as object of C; reconsider p = m as Morphism of p1, p2 by A1,ALTCAT_2:34; m in <^o1,o2^> by A1; then p in (the Arrows of AllEpi C).(o1,o2) by ALTCAT_1:def 2; then <^p1,p2^> <> {} & p is epi by Def2; hence m is epi by A1,Th37; end; theorem Th52: for o1, o2 being object of AllIso C for m being Morphism of o1, o2 st <^o1,o2^> <> {} holds m is iso & m" in <^o2,o1^> proof let o1, o2 be object of AllIso C, m be Morphism of o1, o2 such that A1: <^o1,o2^> <> {}; the carrier of AllIso C = the carrier of C by Def5; then reconsider p1 = o1, p2 = o2 as object of C; reconsider p = m as Morphism of p1, p2 by A1,ALTCAT_2:34; m in <^o1,o2^> by A1; then p in (the Arrows of AllIso C).(o1,o2) by ALTCAT_1:def 2; then A2: <^p1,p2^> <> {} & <^p2,p1^> <> {} & p is iso by Def5; then p" is iso by Th3; then p" in (the Arrows of AllIso C).(p2,p1) by A2,Def5; then A3: p" in <^o2,o1^> by ALTCAT_1:def 2; then reconsider m1 = p" as Morphism of o2, o1 ; A4: m is retraction proof take m1; thus m * m1 = p * p" by A1,A3,ALTCAT_2:33 .= idm p2 by A2,ALTCAT_3:def 5 .= idm o2 by ALTCAT_2:35; end; m is coretraction proof take m1; thus m1 * m = p" * p by A1,A3,ALTCAT_2:33 .= idm p1 by A2,ALTCAT_3:def 5 .= idm o1 by ALTCAT_2:35; end; hence m is iso by A1,A3,A4,ALTCAT_3:6; thus m" in <^o2,o1^> by A3; end; theorem AllMono AllMono C = AllMono C proof A1: the carrier of AllMono AllMono C = the carrier of AllMono C by Def1; A2: the carrier of AllMono C = the carrier of C by Def1; A3: the Arrows of AllMono AllMono C cc= the Arrows of AllMono C by Def1; now let i be set; assume A4: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A5: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of AllMono C by A2,A5; thus (the Arrows of AllMono AllMono C).i = (the Arrows of AllMono C).i proof thus (the Arrows of AllMono AllMono C).i c= (the Arrows of AllMono C).i by A1,A2,A3,A4,ALTCAT_2:def 2; let n be set; assume n in (the Arrows of AllMono C).i; then n in (the Arrows of AllMono C).(o1,o2) by A5,BINOP_1:def 1; then A6: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; n1 is mono by A6,Th50; then n in (the Arrows of AllMono AllMono C).(o1,o2) by A6,Def1; hence n in (the Arrows of AllMono AllMono C).i by A5,BINOP_1:def 1; end; end; then the Arrows of AllMono AllMono C = the Arrows of AllMono C by A1,A2,PBOOLE:3; hence AllMono AllMono C = AllMono C by A1,ALTCAT_2:26; end; theorem AllEpi AllEpi C = AllEpi C proof A1: the carrier of AllEpi AllEpi C = the carrier of AllEpi C by Def2; A2: the carrier of AllEpi C = the carrier of C by Def2; A3: the Arrows of AllEpi AllEpi C cc= the Arrows of AllEpi C by Def2; now let i be set; assume A4: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A5: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of AllEpi C by A2,A5; thus (the Arrows of AllEpi AllEpi C).i = (the Arrows of AllEpi C).i proof thus (the Arrows of AllEpi AllEpi C).i c= (the Arrows of AllEpi C).i by A1,A2,A3,A4,ALTCAT_2:def 2; let n be set; assume n in (the Arrows of AllEpi C).i; then n in (the Arrows of AllEpi C).(o1,o2) by A5,BINOP_1:def 1; then A6: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; n1 is epi by A6,Th51; then n in (the Arrows of AllEpi AllEpi C).(o1,o2) by A6,Def2; hence n in (the Arrows of AllEpi AllEpi C).i by A5,BINOP_1:def 1; end; end; then the Arrows of AllEpi AllEpi C = the Arrows of AllEpi C by A1,A2,PBOOLE:3; hence AllEpi AllEpi C = AllEpi C by A1,ALTCAT_2:26; end; theorem AllIso AllIso C = AllIso C proof A1: the carrier of AllIso AllIso C = the carrier of AllIso C by Def5; A2: the carrier of AllIso C = the carrier of C by Def5; A3: the Arrows of AllIso AllIso C cc= the Arrows of AllIso C by Def5; now let i be set; assume A4: i in [:the carrier of C,the carrier of C:]; then consider o1, o2 being set such that A5: o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] by ZFMISC_1:103; reconsider o1, o2 as object of AllIso C by A2,A5; thus (the Arrows of AllIso AllIso C).i = (the Arrows of AllIso C).i proof thus (the Arrows of AllIso AllIso C).i c= (the Arrows of AllIso C).i by A1,A2,A3,A4,ALTCAT_2:def 2; let n be set; assume n in (the Arrows of AllIso C).i; then n in (the Arrows of AllIso C).(o1,o2) by A5,BINOP_1:def 1; then A6: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; A7: n1" in <^o2,o1^> by A6,Th52; n1 is iso by A6,Th52; then n in (the Arrows of AllIso AllIso C).(o1,o2) by A6,A7,Def5; hence n in (the Arrows of AllIso AllIso C).i by A5,BINOP_1:def 1; end; end; then the Arrows of AllIso AllIso C = the Arrows of AllIso C by A1,A2,PBOOLE:3; hence AllIso AllIso C = AllIso C by A1,ALTCAT_2:26; end; theorem AllIso AllMono C = AllIso C proof A1: the carrier of AllIso AllMono C = the carrier of AllMono C by Def5; A2: the carrier of AllIso C = the carrier of C by Def5; A3: the carrier of AllMono C = the carrier of C by Def1; A4: AllIso C is non empty subcategory of AllCoretr C by Th42; AllCoretr C is non empty subcategory of AllMono C by Th43; then A5: AllIso C is non empty subcategory of AllMono C by A4,Th36; now let i be set; assume A6: i in [:the carrier of C,the carrier of C:]; then 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, o2 as object of AllMono C by A3,A7; thus (the Arrows of AllIso AllMono C).i = (the Arrows of AllIso C).i proof thus (the Arrows of AllIso AllMono C).i c= (the Arrows of AllIso C).i proof let n be set such that A8: n in (the Arrows of AllIso AllMono C).i; reconsider q1 = o1, q2 = o2 as object of AllIso AllMono C by A1; A9: n in (the Arrows of AllIso AllMono C).(q1,q2) by A7,A8,BINOP_1:def 1; then A10: n in <^q1,q2^> by ALTCAT_1:def 2; 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 A10; reconsider r1 = o1, r2 = o2 as object of C by A3; A12: <^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 A10; <^q2,q1^> <> {} by A10,Th52; then A13: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A10,A11,XBOOLE_1:3; then A14: <^r1,r2^> <> {} & <^r2,r1^> <> {} by A12,XBOOLE_1:3; n2 is iso by A9,Def5; then n1 is iso by A13,Th40; then n in (the Arrows of AllIso C).(r1,r2) by A14,Def5; hence n in (the Arrows of AllIso C).i by A7,BINOP_1:def 1; end; let n be set such that A15: n in (the Arrows of AllIso C).i; reconsider p1 = o1, p2 = o2 as object of AllIso C by A2,A3; the Arrows of AllIso C cc= the Arrows of AllMono C by A5,ALTCAT_2:def 11; then (the Arrows of AllIso C).i c= (the Arrows of AllMono C).i by A2,A6,ALTCAT_2:def 2; then n in (the Arrows of AllMono C).i by A15; then n in (the Arrows of AllMono C).(o1,o2) by A7,BINOP_1:def 1; then A16: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; n in (the Arrows of AllIso C).(o1,o2) by A7,A15,BINOP_1:def 1; then A17: n in <^p1,p2^> by ALTCAT_1:def 2; then reconsider n2 = n as Morphism of p1, p2 ; A18: n2" in <^p2,p1^> by A17,Th52; A19: <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:32; n2 is iso by A17,Th52; then n1 is iso by A5,A17,A18,Th40; then n in (the Arrows of AllIso AllMono C).(o1,o2) by A16,A18,A19,Def5 ; hence n in (the Arrows of AllIso AllMono C).i by A7,BINOP_1:def 1; end; end; then A20: the Arrows of AllIso AllMono C = the Arrows of AllIso C by A1,A2,A3,PBOOLE:3; AllIso AllMono C is transitive non empty SubCatStr of C by ALTCAT_2:22; then AllIso AllMono C is SubCatStr of AllIso C by A1,A2,A3,A20,ALTCAT_2:25 ; hence AllIso AllMono C = AllIso C by A1,A2,A3,A20,ALTCAT_2:26; end; theorem AllIso AllEpi C = AllIso C proof 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; now let i be set; assume A6: i in [:the carrier of C,the carrier of C:]; then 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, o2 as object of AllEpi C by A3,A7; thus (the Arrows of AllIso AllEpi C).i = (the Arrows of AllIso C).i proof thus (the Arrows of AllIso AllEpi C).i c= (the Arrows of AllIso C).i proof let n be set such that A8: n in (the Arrows of AllIso AllEpi C).i; reconsider q1 = o1, q2 = o2 as object of AllIso AllEpi C by A1; A9: n in (the Arrows of AllIso AllEpi C).(q1,q2) by A7,A8,BINOP_1:def 1; then A10: n in <^q1,q2^> by ALTCAT_1:def 2; 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 A10; reconsider r1 = o1, r2 = o2 as object of C by A3; A12: <^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 A10; <^q2,q1^> <> {} by A10,Th52; then A13: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A10,A11,XBOOLE_1:3; then A14: <^r1,r2^> <> {} & <^r2,r1^> <> {} by A12,XBOOLE_1:3; n2 is iso by A9,Def5; then n1 is iso by A13,Th40; then n in (the Arrows of AllIso C).(r1,r2) by A14,Def5; hence n in (the Arrows of AllIso C).i by A7,BINOP_1:def 1; end; let n be set such that A15: n in (the Arrows of AllIso C).i; reconsider p1 = o1, p2 = o2 as object of AllIso C by A2,A3; the Arrows of AllIso C cc= the Arrows of AllEpi C by A5,ALTCAT_2:def 11; then (the Arrows of AllIso C).i c= (the Arrows of AllEpi C).i by A2,A6,ALTCAT_2:def 2; then n in (the Arrows of AllEpi C).i by A15; then n in (the Arrows of AllEpi C).(o1,o2) by A7,BINOP_1:def 1; then A16: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; n in (the Arrows of AllIso C).(o1,o2) by A7,A15,BINOP_1:def 1; then A17: n in <^p1,p2^> by ALTCAT_1:def 2; then reconsider n2 = n as Morphism of p1, p2 ; A18: n2" in <^p2,p1^> by A17,Th52; A19: <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:32; n2 is iso by A17,Th52; then n1 is iso by A5,A17,A18,Th40; then n in (the Arrows of AllIso AllEpi C).(o1,o2) by A16,A18,A19,Def5; hence n in (the Arrows of AllIso AllEpi C).i by A7,BINOP_1:def 1; end; end; then A20: the Arrows of AllIso AllEpi C = the Arrows of AllIso C by A1,A2,A3,PBOOLE:3; AllIso AllEpi C is transitive non empty SubCatStr of C by ALTCAT_2:22; then AllIso AllEpi C is SubCatStr of AllIso C by A1,A2,A3,A20,ALTCAT_2:25; hence AllIso AllEpi C = AllIso C by A1,A2,A3,A20,ALTCAT_2:26; end; theorem AllIso AllRetr C = AllIso C proof A1: the carrier of AllIso AllRetr C = the carrier of AllRetr C by Def5; A2: the carrier of AllIso C = the carrier of C by Def5; A3: the carrier of AllRetr C = the carrier of C by Def3; A4: AllIso C is non empty subcategory of AllRetr C by Th41; now let i be set; assume A5: i in [:the carrier of C,the carrier of C:]; then 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, o2 as object of AllRetr C by A3,A6; thus (the Arrows of AllIso AllRetr C).i = (the Arrows of AllIso C).i proof thus (the Arrows of AllIso AllRetr C).i c= (the Arrows of AllIso C).i proof let n be set such that A7: n in (the Arrows of AllIso AllRetr C).i; reconsider q1 = o1, q2 = o2 as object of AllIso AllRetr C by A1; A8: n in (the Arrows of AllIso AllRetr C).(q1,q2) by A6,A7,BINOP_1:def 1; then A9: n in <^q1,q2^> by ALTCAT_1:def 2; 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 A9; reconsider r1 = o1, r2 = o2 as object of C by A3; A11: <^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 A9; <^q2,q1^> <> {} by A9,Th52; then A12: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A9,A10,XBOOLE_1:3; then A13: <^r1,r2^> <> {} & <^r2,r1^> <> {} by A11,XBOOLE_1:3; n2 is iso by A8,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 A6,BINOP_1:def 1; end; let n be set such that A14: n in (the Arrows of AllIso C).i; reconsider p1 = o1, p2 = o2 as object of AllIso C by A2,A3; the Arrows of AllIso C cc= the Arrows of AllRetr C by A4,ALTCAT_2:def 11; then (the Arrows of AllIso C).i c= (the Arrows of AllRetr C).i by A2,A5,ALTCAT_2:def 2; then n in (the Arrows of AllRetr C).i by A14; then n in (the Arrows of AllRetr C).(o1,o2) by A6,BINOP_1:def 1; then A15: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; n in (the Arrows of AllIso C).(o1,o2) by A6,A14,BINOP_1:def 1; then A16: n in <^p1,p2^> by ALTCAT_1:def 2; then reconsider n2 = n as Morphism of p1, p2 ; A17: n2" in <^p2,p1^> by A16,Th52; A18: <^p2,p1^> c= <^o2,o1^> by A4,ALTCAT_2:32; n2 is iso by A16,Th52; then n1 is iso by A4,A16,A17,Th40; then n in (the Arrows of AllIso AllRetr C).(o1,o2) by A15,A17,A18,Def5 ; hence n in (the Arrows of AllIso AllRetr C).i by A6,BINOP_1:def 1; end; end; then A19: the Arrows of AllIso AllRetr C = the Arrows of AllIso C by A1,A2,A3,PBOOLE:3; AllIso AllRetr C is transitive non empty SubCatStr of C by ALTCAT_2:22; then AllIso AllRetr C is SubCatStr of AllIso C by A1,A2,A3,A19,ALTCAT_2:25 ; hence AllIso AllRetr C = AllIso C by A1,A2,A3,A19,ALTCAT_2:26; end; theorem AllIso AllCoretr C = AllIso C proof 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; now let i be set; assume A5: i in [:the carrier of C,the carrier of C:]; then 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, o2 as object of AllCoretr C by A3,A6; thus (the Arrows of AllIso AllCoretr C).i = (the Arrows of AllIso C).i proof thus (the Arrows of AllIso AllCoretr C).i c= (the Arrows of AllIso C).i proof let n be set such that A7: n in (the Arrows of AllIso AllCoretr C).i; reconsider q1 = o1, q2 = o2 as object of AllIso AllCoretr C by A1; A8: n in (the Arrows of AllIso AllCoretr C).(q1,q2) by A6,A7,BINOP_1:def 1; then A9: n in <^q1,q2^> by ALTCAT_1:def 2; 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 A9; reconsider r1 = o1, r2 = o2 as object of C by A3; A11: <^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 A9; <^q2,q1^> <> {} by A9,Th52; then A12: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A9,A10,XBOOLE_1:3; then A13: <^r1,r2^> <> {} & <^r2,r1^> <> {} by A11,XBOOLE_1:3; n2 is iso by A8,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 A6,BINOP_1:def 1; end; let n be set such that A14: n in (the Arrows of AllIso C).i; reconsider p1 = o1, p2 = o2 as object of AllIso C by A2,A3; the Arrows of AllIso C cc= the Arrows of AllCoretr C by A4,ALTCAT_2:def 11; then (the Arrows of AllIso C).i c= (the Arrows of AllCoretr C).i by A2,A5,ALTCAT_2:def 2; then n in (the Arrows of AllCoretr C).i by A14; then n in (the Arrows of AllCoretr C).(o1,o2) by A6,BINOP_1:def 1; then A15: n in <^o1,o2^> by ALTCAT_1:def 2; then reconsider n1 = n as Morphism of o1, o2 ; n in (the Arrows of AllIso C).(o1,o2) by A6,A14,BINOP_1:def 1; then A16: n in <^p1,p2^> by ALTCAT_1:def 2; then reconsider n2 = n as Morphism of p1, p2 ; A17: n2" in <^p2,p1^> by A16,Th52; A18: <^p2,p1^> c= <^o2,o1^> by A4,ALTCAT_2:32; n2 is iso by A16,Th52; then n1 is iso by A4,A16,A17,Th40; then n in (the Arrows of AllIso AllCoretr C).(o1,o2) by A15,A17,A18, Def5; hence n in (the Arrows of AllIso AllCoretr C).i by A6,BINOP_1:def 1; end; end; then A19: the Arrows of AllIso AllCoretr C = the Arrows of AllIso C by A1,A2,A3,PBOOLE:3; AllIso AllCoretr C is transitive non empty SubCatStr of C by ALTCAT_2:22; then AllIso AllCoretr C is SubCatStr of AllIso C by A1,A2,A3,A19,ALTCAT_2: 25; hence AllIso AllCoretr C = AllIso C by A1,A2,A3,A19,ALTCAT_2:26; end;

Back to top