defpred S1[ object , object ] means ex D2 being set st
( D2 = $2 & ( for x being set holds
( x in D2 iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st
( $1 = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi ) ) ) );
set I = the carrier of C;
A1:
for i being object st i in [: the carrier of C, the carrier of C:] holds
ex X being object st S1[i,X]
proof
let i be
object ;
( i in [: the carrier of C, the carrier of C:] implies ex X being object st S1[i,X] )
assume
i in [: the carrier of C, the carrier of C:]
;
ex X being object st S1[i,X]
then consider o1,
o2 being
object such that A2:
(
o1 in the
carrier of
C &
o2 in the
carrier of
C )
and A3:
i = [o1,o2]
by ZFMISC_1:84;
reconsider o1 =
o1,
o2 =
o2 as
Object of
C by A2;
defpred S2[
object ]
means ex
m being
Morphism of
o1,
o2 st
(
<^o1,o2^> <> {} &
m = $1 &
m is
epi );
consider X being
set such that A4:
for
x being
object holds
(
x in X iff (
x in the
Arrows of
C . (
o1,
o2) &
S2[
x] ) )
from XBOOLE_0:sch 1();
take
X
;
S1[i,X]
take
X
;
( X = X & ( for x being set holds
( x in X iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st
( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi ) ) ) )
thus
X = X
;
for x being set holds
( x in X iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st
( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi ) )
let x be
set ;
( x in X iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st
( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi ) )
thus
(
x in X implies ex
o1,
o2 being
Object of
C ex
m being
Morphism of
o1,
o2 st
(
i = [o1,o2] &
<^o1,o2^> <> {} &
x = m &
m is
epi ) )
( ex o1, o2 being Object of C ex m being Morphism of o1,o2 st
( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi ) implies x in X )proof
assume
x in X
;
ex o1, o2 being Object of C ex m being Morphism of o1,o2 st
( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi )
then consider m being
Morphism of
o1,
o2 such that A5:
(
<^o1,o2^> <> {} &
m = x &
m is
epi )
by A4;
take
o1
;
ex o2 being Object of C ex m being Morphism of o1,o2 st
( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi )
take
o2
;
ex m being Morphism of o1,o2 st
( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi )
take
m
;
( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi )
thus
(
i = [o1,o2] &
<^o1,o2^> <> {} &
x = m &
m is
epi )
by A3, A5;
verum
end;
given p1,
p2 being
Object of
C,
m being
Morphism of
p1,
p2 such that A6:
i = [p1,p2]
and A7:
(
<^p1,p2^> <> {} &
x = m &
m is
epi )
;
x in X
(
o1 = p1 &
o2 = p2 )
by A3, A6, XTUPLE_0:1;
hence
x in X
by A4, A7;
verum
end;
consider Ar being ManySortedSet of [: the carrier of C, the carrier of C:] such that
A8:
for i being object st i in [: the carrier of C, the carrier of C:] holds
S1[i,Ar . i]
from PBOOLE:sch 3(A1);
defpred S2[ object , object ] 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)):] );
A9:
for i being object st i in [: the carrier of C, the carrier of C, the carrier of C:] holds
ex j being object st S2[i,j]
proof
let i be
object ;
( i in [: the carrier of C, the carrier of C, the carrier of C:] implies ex j being object st S2[i,j] )
assume
i in [: the carrier of C, the carrier of C, the carrier of C:]
;
ex j being object st S2[i,j]
then consider p1,
p2,
p3 being
object such that A10:
(
p1 in the
carrier of
C &
p2 in the
carrier of
C &
p3 in the
carrier of
C )
and A11:
i = [p1,p2,p3]
by MCART_1:68;
reconsider p1 =
p1,
p2 =
p2,
p3 =
p3 as
Object of
C by A10;
take
( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):]
;
S2[i,( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):]]
take
p1
;
ex p2, p3 being Object of C st
( i = [p1,p2,p3] & ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] )
take
p2
;
ex p3 being Object of C st
( i = [p1,p2,p3] & ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] )
take
p3
;
( i = [p1,p2,p3] & ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] )
thus
i = [p1,p2,p3]
by A11;
( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):]
thus
( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):]
;
verum
end;
consider Co being ManySortedSet of [: the carrier of C, the carrier of C, the carrier of C:] such that
A12:
for i being object st i in [: the carrier of C, the carrier of C, the carrier of C:] holds
S2[i,Co . i]
from PBOOLE:sch 3(A9);
A13:
Ar cc= the Arrows of C
proof
thus
[: the carrier of C, the carrier of C:] c= [: the carrier of C, the carrier of C:]
;
ALTCAT_2:def 2 for b1 being set holds
( not b1 in [: the carrier of C, the carrier of C:] or Ar . b1 c= the Arrows of C . b1 )
let i be
set ;
( not i in [: the carrier of C, the carrier of C:] or Ar . i c= the Arrows of C . i )
assume A14:
i in [: the carrier of C, the carrier of C:]
;
Ar . i c= the Arrows of C . i
let q be
object ;
TARSKI:def 3 ( not q in Ar . i or q in the Arrows of C . i )
assume A15:
q in Ar . i
;
q in the Arrows of C . i
S1[
i,
Ar . i]
by A8, A14;
then
ex
p1,
p2 being
Object of
C ex
m being
Morphism of
p1,
p2 st
(
i = [p1,p2] &
<^p1,p2^> <> {} &
q = m &
m is
epi )
by A15;
hence
q in the
Arrows of
C . i
;
verum
end;
Co is ManySortedFunction of {|Ar,Ar|},{|Ar|}
proof
let i be
object ;
PBOOLE:def 15 ( not i in [: the carrier of C, the carrier of C, the carrier of C:] or Co . i is M3( bool [:({|Ar,Ar|} . i),({|Ar|} . i):]) )
assume
i in [: the carrier of C, the carrier of C, the carrier of C:]
;
Co . i is M3( bool [:({|Ar,Ar|} . i),({|Ar|} . i):])
then consider p1,
p2,
p3 being
Object of
C such that A16:
i = [p1,p2,p3]
and A17:
Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):]
by A12;
A18:
[p1,p2] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
then A19:
Ar . [p1,p2] c= the
Arrows of
C . (
p1,
p2)
by A13;
A20:
[p2,p3] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
then
Ar . [p2,p3] c= the
Arrows of
C . (
p2,
p3)
by A13;
then A21:
[:(Ar . (p2,p3)),(Ar . (p1,p2)):] c= [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):]
by A19, ZFMISC_1:96;
( the
Arrows of
C . (
p1,
p3)
= {} implies
[:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {} )
by Lm1;
then reconsider f =
Co . i as
Function of
[:(Ar . (p2,p3)),(Ar . (p1,p2)):],
( the Arrows of C . (p1,p3)) by A17, A21, FUNCT_2:32;
A22:
Ar . [p1,p2] c= the
Arrows of
C . [p1,p2]
by A13, A18;
A23:
Ar . [p2,p3] c= the
Arrows of
C . [p2,p3]
by A13, A20;
A24:
( the
Arrows of
C . (
p1,
p3)
= {} implies
[:(Ar . (p2,p3)),(Ar . (p1,p2)):] = {} )
proof
assume A25:
the
Arrows of
C . (
p1,
p3)
= {}
;
[:(Ar . (p2,p3)),(Ar . (p1,p2)):] = {}
assume
[:(Ar . (p2,p3)),(Ar . (p1,p2)):] <> {}
;
contradiction
then consider k being
object such that A26:
k in [:(Ar . (p2,p3)),(Ar . (p1,p2)):]
by XBOOLE_0:def 1;
consider u1,
u2 being
object such that A27:
(
u1 in Ar . (
p2,
p3) &
u2 in Ar . (
p1,
p2) )
and
k = [u1,u2]
by A26, ZFMISC_1:def 2;
(
u1 in <^p2,p3^> &
u2 in <^p1,p2^> )
by A23, A22, A27;
then
<^p1,p3^> <> {}
by ALTCAT_1:def 2;
hence
contradiction
by A25;
verum
end;
A28:
{|Ar|} . (
p1,
p2,
p3)
= Ar . (
p1,
p3)
by ALTCAT_1:def 3;
A29:
rng f c= {|Ar|} . i
proof
let q be
object ;
TARSKI:def 3 ( not q in rng f or q in {|Ar|} . i )
assume
q in rng f
;
q in {|Ar|} . i
then consider x being
object such that A30:
x in dom f
and A31:
q = f . x
by FUNCT_1:def 3;
A32:
dom f = [:(Ar . (p2,p3)),(Ar . (p1,p2)):]
by A24, FUNCT_2:def 1;
then consider m1,
m2 being
object such that A33:
m1 in Ar . (
p2,
p3)
and A34:
m2 in Ar . (
p1,
p2)
and A35:
x = [m1,m2]
by A30, ZFMISC_1:84;
[p2,p3] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
then
S1[
[p2,p3],
Ar . [p2,p3]]
by A8;
then consider q2,
q3 being
Object of
C,
qq being
Morphism of
q2,
q3 such that A36:
[p2,p3] = [q2,q3]
and A37:
<^q2,q3^> <> {}
and A38:
m1 = qq
and A39:
qq is
epi
by A33;
[p1,p2] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
then
S1[
[p1,p2],
Ar . [p1,p2]]
by A8;
then consider r1,
r2 being
Object of
C,
rr being
Morphism of
r1,
r2 such that A40:
[p1,p2] = [r1,r2]
and A41:
<^r1,r2^> <> {}
and A42:
m2 = rr
and A43:
rr is
epi
by A34;
A44:
ex
o1,
o3 being
Object of
C ex
m being
Morphism of
o1,
o3 st
(
[p1,p3] = [o1,o3] &
<^o1,o3^> <> {} &
q = m &
m is
epi )
proof
A45:
p2 = q2
by A36, XTUPLE_0:1;
then reconsider mm =
qq as
Morphism of
r2,
q3 by A40, XTUPLE_0:1;
take
r1
;
ex o3 being Object of C ex m being Morphism of r1,o3 st
( [p1,p3] = [r1,o3] & <^r1,o3^> <> {} & q = m & m is epi )
take
q3
;
ex m being Morphism of r1,q3 st
( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & q = m & m is epi )
take
mm * rr
;
( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & q = mm * rr & mm * rr is epi )
A46:
p1 = r1
by A40, XTUPLE_0:1;
hence
[p1,p3] = [r1,q3]
by A36, XTUPLE_0:1;
( <^r1,q3^> <> {} & q = mm * rr & mm * rr is epi )
A47:
r2 = p2
by A40, XTUPLE_0:1;
hence
<^r1,q3^> <> {}
by A37, A41, A45, ALTCAT_1:def 2;
( q = mm * rr & mm * rr is epi )
A48:
p3 = q3
by A36, XTUPLE_0:1;
thus q =
( the Comp of C . (p1,p2,p3)) . (
mm,
rr)
by A17, A30, A31, A32, A35, A38, A42, FUNCT_1:49
.=
mm * rr
by A36, A37, A41, A47, A46, A48, ALTCAT_1:def 8
;
mm * rr is epi
thus
mm * rr is
epi
by A37, A39, A41, A43, A47, A45, ALTCAT_3:10;
verum
end;
[p1,p3] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
then
S1[
[p1,p3],
Ar . [p1,p3]]
by A8;
then
q in Ar . [p1,p3]
by A44;
hence
q in {|Ar|} . i
by A16, A28, MULTOP_1:def 1;
verum
end;
{|Ar,Ar|} . (
p1,
p2,
p3)
= [:(Ar . (p2,p3)),(Ar . (p1,p2)):]
by ALTCAT_1:def 4;
then
[:(Ar . (p2,p3)),(Ar . (p1,p2)):] = {|Ar,Ar|} . i
by A16, MULTOP_1:def 1;
hence
Co . i is
M3(
bool [:({|Ar,Ar|} . i),({|Ar|} . i):])
by A24, A29, FUNCT_2:6;
verum
end;
then reconsider Co = Co as BinComp of Ar ;
set IT = AltCatStr(# the carrier of C,Ar,Co #);
set J = the carrier of AltCatStr(# the carrier of C,Ar,Co #);
AltCatStr(# the carrier of C,Ar,Co #) is SubCatStr of C
proof
thus
the
carrier of
AltCatStr(# the
carrier of
C,
Ar,
Co #)
c= the
carrier of
C
;
ALTCAT_2:def 11 ( the Arrows of AltCatStr(# the carrier of C,Ar,Co #) cc= the Arrows of C & the Comp of AltCatStr(# the carrier of C,Ar,Co #) cc= the Comp of C )
thus
the
Arrows of
AltCatStr(# the
carrier of
C,
Ar,
Co #)
cc= the
Arrows of
C
by A13;
the Comp of AltCatStr(# the carrier of C,Ar,Co #) cc= the Comp of C
thus
[: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] c= [: the carrier of C, the carrier of C, the carrier of C:]
;
ALTCAT_2:def 2 for b1 being set holds
( not b1 in [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] or the Comp of AltCatStr(# the carrier of C,Ar,Co #) . b1 c= the Comp of C . b1 )
let i be
set ;
( not i in [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] or the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i c= the Comp of C . i )
assume
i in [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):]
;
the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i c= the Comp of C . i
then consider p1,
p2,
p3 being
Object of
C such that A49:
i = [p1,p2,p3]
and A50:
Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):]
by A12;
A51:
( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] c= the
Comp of
C . (
p1,
p2,
p3)
by RELAT_1:59;
let q be
object ;
TARSKI:def 3 ( not q in the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i or q in the Comp of C . i )
assume
q in the
Comp of
AltCatStr(# the
carrier of
C,
Ar,
Co #)
. i
;
q in the Comp of C . i
then
q in the
Comp of
C . (
p1,
p2,
p3)
by A50, A51;
hence
q in the
Comp of
C . i
by A49, MULTOP_1:def 1;
verum
end;
then reconsider IT = AltCatStr(# the carrier of C,Ar,Co #) as non empty strict SubCatStr of C ;
IT is transitive
proof
let p1,
p2,
p3 be
Object of
IT;
ALTCAT_1:def 2 ( <^p1,p2^> = {} or <^p2,p3^> = {} or not <^p1,p3^> = {} )
assume that A52:
<^p1,p2^> <> {}
and A53:
<^p2,p3^> <> {}
;
not <^p1,p3^> = {}
consider m2 being
object such that A54:
m2 in <^p1,p2^>
by A52, XBOOLE_0:def 1;
consider m1 being
object such that A55:
m1 in <^p2,p3^>
by A53, XBOOLE_0:def 1;
[p2,p3] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
then
S1[
[p2,p3],
Ar . [p2,p3]]
by A8;
then consider q2,
q3 being
Object of
C,
qq being
Morphism of
q2,
q3 such that A56:
[p2,p3] = [q2,q3]
and A57:
<^q2,q3^> <> {}
and
m1 = qq
and A58:
qq is
epi
by A55;
[p1,p2] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
then
S1[
[p1,p2],
Ar . [p1,p2]]
by A8;
then consider r1,
r2 being
Object of
C,
rr being
Morphism of
r1,
r2 such that A59:
[p1,p2] = [r1,r2]
and A60:
<^r1,r2^> <> {}
and
m2 = rr
and A61:
rr is
epi
by A54;
A62:
p2 = q2
by A56, XTUPLE_0:1;
then reconsider mm =
qq as
Morphism of
r2,
q3 by A59, XTUPLE_0:1;
A63:
r2 = p2
by A59, XTUPLE_0:1;
A64:
ex
o1,
o3 being
Object of
C ex
m being
Morphism of
o1,
o3 st
(
[p1,p3] = [o1,o3] &
<^o1,o3^> <> {} &
mm * rr = m &
m is
epi )
proof
take
r1
;
ex o3 being Object of C ex m being Morphism of r1,o3 st
( [p1,p3] = [r1,o3] & <^r1,o3^> <> {} & mm * rr = m & m is epi )
take
q3
;
ex m being Morphism of r1,q3 st
( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & mm * rr = m & m is epi )
take
mm * rr
;
( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & mm * rr = mm * rr & mm * rr is epi )
p1 = r1
by A59, XTUPLE_0:1;
hence
[p1,p3] = [r1,q3]
by A56, XTUPLE_0:1;
( <^r1,q3^> <> {} & mm * rr = mm * rr & mm * rr is epi )
thus
<^r1,q3^> <> {}
by A57, A60, A63, A62, ALTCAT_1:def 2;
( mm * rr = mm * rr & mm * rr is epi )
thus
mm * rr = mm * rr
;
mm * rr is epi
thus
mm * rr is
epi
by A57, A58, A60, A61, A63, A62, ALTCAT_3:10;
verum
end;
[p1,p3] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
then
S1[
[p1,p3],
Ar . [p1,p3]]
by A8;
hence
not
<^p1,p3^> = {}
by A64;
verum
end;
then reconsider IT = IT as non empty transitive strict SubCatStr of C ;
take
IT
; ( the carrier of IT = the carrier of C & the Arrows of IT 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 IT . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ) )
thus
the carrier of IT = the carrier of C
; ( the Arrows of IT 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 IT . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ) )
thus
the Arrows of IT cc= the Arrows of C
by A13; for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) )
let o1, o2 be Object of C; for m being Morphism of o1,o2 holds
( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) )
let m be Morphism of o1,o2; ( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) )
A65:
[o1,o2] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
thus
( m in the Arrows of IT . (o1,o2) implies ( <^o1,o2^> <> {} & m is epi ) )
( <^o1,o2^> <> {} & m is epi implies m in the Arrows of IT . (o1,o2) )proof
assume A66:
m in the
Arrows of
IT . (
o1,
o2)
;
( <^o1,o2^> <> {} & m is epi )
S1[
[o1,o2],
Ar . [o1,o2]]
by A8, A65;
then consider p1,
p2 being
Object of
C,
n being
Morphism of
p1,
p2 such that A67:
[o1,o2] = [p1,p2]
and A68:
(
<^p1,p2^> <> {} &
m = n &
n is
epi )
by A66;
(
o1 = p1 &
o2 = p2 )
by A67, XTUPLE_0:1;
hence
(
<^o1,o2^> <> {} &
m is
epi )
by A68;
verum
end;
assume A69:
( <^o1,o2^> <> {} & m is epi )
; m in the Arrows of IT . (o1,o2)
S1[[o1,o2],Ar . [o1,o2]]
by A8, A65;
hence
m in the Arrows of IT . (o1,o2)
by A69; verum