environ
vocabularies HIDDEN, ALTCAT_1, XBOOLE_0, CAT_1, RELAT_1, ALTCAT_3, CAT_3, RELAT_2, FUNCTOR0, FUNCT_1, FUNCT_2, ZFMISC_1, STRUCT_0, PBOOLE, MSUALG_3, MSUALG_6, ALTCAT_2, TARSKI, ALTCAT_4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, MULTOP_1, PBOOLE, STRUCT_0, MSUALG_3, ALTCAT_1, ALTCAT_2, ALTCAT_3, FUNCTOR0;
definitions ALTCAT_1, ALTCAT_3, FUNCTOR0, MSUALG_3, TARSKI, FUNCT_2, XBOOLE_0, PBOOLE, ALTCAT_2;
theorems ALTCAT_1, ALTCAT_2, ALTCAT_3, FUNCT_1, FUNCT_2, FUNCTOR0, MCART_1, MULTOP_1, FUNCTOR1, FUNCTOR2, PBOOLE, RELAT_1, ZFMISC_1, XBOOLE_0, XBOOLE_1, PARTFUN1, XTUPLE_0;
schemes PBOOLE, XBOOLE_0;
registrations SUBSET_1, RELSET_1, FUNCOP_1, STRUCT_0, FUNCT_1, RELAT_1, ALTCAT_1, ALTCAT_2, FUNCTOR0, FUNCTOR2, PBOOLE;
constructors HIDDEN, REALSET1, MSUALG_3, FUNCTOR0, ALTCAT_3, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities ALTCAT_1, FUNCTOR0, XBOOLE_0, BINOP_1, REALSET1;
expansions ALTCAT_3, FUNCTOR0, MSUALG_3, TARSKI, FUNCT_2, ALTCAT_2;
Lm1:
now for C being non empty transitive AltCatStr
for p1, p2, p3 being Object of C st the Arrows of C . (p1,p3) = {} holds
[:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {}
let C be non
empty transitive AltCatStr ;
for p1, p2, p3 being Object of C st the Arrows of C . (p1,p3) = {} holds
[:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {} let p1,
p2,
p3 be
Object of
C;
( the Arrows of C . (p1,p3) = {} implies [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {} )assume A1:
the
Arrows of
C . (
p1,
p3)
= {}
;
[:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {} thus
[:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {}
verum
proof
assume
[:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] <> {}
;
contradiction
then consider k being
object 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
object such that A3:
(
u1 in the
Arrows of
C . (
p2,
p3) &
u2 in the
Arrows of
C . (
p1,
p2) )
and
k = [u1,u2]
by A2, ZFMISC_1:def 2;
(
u1 in <^p2,p3^> &
u2 in <^p1,p2^> )
by A3;
then
<^p1,p3^> <> {}
by ALTCAT_1:def 2;
hence
contradiction
by A1;
verum
end;
end;
definition
let C be
category;
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) holds
b1 = b2
end;
definition
let C be
category;
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ) holds
b1 = b2
end;
definition
let C be
category;
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) holds
b1 = b2
end;
definition
let C be
category;
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) holds
b1 = b2
end;
definition
let C be
category;
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) holds
b1 = b2
end;