set DD = the Source of C1 | the carrier' of C2;
set CC = the Target of C1 | the carrier' of C2;
set Cm = the Comp of C1 || the carrier' of C2;
reconsider O = the carrier of C1 /\ the carrier of C2 as non empty set by A3, XBOOLE_0:def 4;
reconsider o2 = o1 as Object of C2 by A3;
reconsider o = o1 as Object of C by A1, CAT_2:6;
A4:
id o1 = id o
by A1, CAT_2:def 4;
id o2 = id o
by A2, CAT_2:def 4;
then reconsider M = the carrier' of C1 /\ the carrier' of C2 as non empty set by A4, XBOOLE_0:def 4;
A5:
dom the Source of C1 = the carrier' of C1
by FUNCT_2:def 1;
A6:
dom the Target of C1 = the carrier' of C1
by FUNCT_2:def 1;
A7:
dom ( the Source of C1 | the carrier' of C2) = M
by A5, RELAT_1:61;
A8:
dom ( the Target of C1 | the carrier' of C2) = M
by A6, RELAT_1:61;
rng ( the Source of C1 | the carrier' of C2) c= O
then reconsider DD = the Source of C1 | the carrier' of C2 as Function of M,O by A7, FUNCT_2:def 1, RELSET_1:4;
rng ( the Target of C1 | the carrier' of C2) c= O
then reconsider CC = the Target of C1 | the carrier' of C2 as Function of M,O by A8, FUNCT_2:def 1, RELSET_1:4;
A17:
dom ( the Comp of C1 || the carrier' of C2) = (dom the Comp of C1) /\ [: the carrier' of C2, the carrier' of C2:]
by RELAT_1:61;
then
dom ( the Comp of C1 || the carrier' of C2) c= [: the carrier' of C1, the carrier' of C1:] /\ [: the carrier' of C2, the carrier' of C2:]
by XBOOLE_1:26;
then A18:
dom ( the Comp of C1 || the carrier' of C2) c= [:M,M:]
by ZFMISC_1:100;
rng ( the Comp of C1 || the carrier' of C2) c= M
proof
let x be
object ;
TARSKI:def 3 ( not x in rng ( the Comp of C1 || the carrier' of C2) or x in M )
assume
x in rng ( the Comp of C1 || the carrier' of C2)
;
x in M
then consider m being
object such that A19:
m in dom ( the Comp of C1 || the carrier' of C2)
and A20:
x = ( the Comp of C1 || the carrier' of C2) . m
by FUNCT_1:def 3;
A21:
m `1 in M
by A18, A19, MCART_1:10;
A22:
m `2 in M
by A18, A19, MCART_1:10;
A23:
m = [(m `1),(m `2)]
by A17, A19, MCART_1:21;
reconsider m1 =
m `1 ,
m2 =
m `2 as
Morphism of
C1 by A21, A22, XBOOLE_0:def 4;
reconsider n1 =
m `1 ,
n2 =
m `2 as
Morphism of
C2 by A21, A22, XBOOLE_0:def 4;
reconsider mm =
m1,
n =
m2 as
Morphism of
C by A1, CAT_2:8;
A24:
m in dom the
Comp of
C1
by A17, A19, XBOOLE_0:def 4;
then A25:
dom m1 = cod m2
by A23, CAT_1:15;
A26:
x = the
Comp of
C1 . (
m1,
m2)
by A19, A20, A23, FUNCT_1:47;
A27:
dom m1 = dom mm
by A1, CAT_2:9;
A28:
dom n1 = dom mm
by A2, CAT_2:9;
A29:
cod m2 = cod n
by A1, CAT_2:9;
A30:
cod n2 = cod n
by A2, CAT_2:9;
A31:
x = m1 (*) m2
by A23, A24, A26, CAT_1:def 1;
A32:
m1 (*) m2 = mm (*) n
by A1, A25, CAT_2:11;
mm (*) n = n1 (*) n2
by A2, A25, A27, A28, A29, A30, CAT_2:11;
hence
x in M
by A31, A32, XBOOLE_0:def 4;
verum
end;
then reconsider Cm = the Comp of C1 || the carrier' of C2 as PartFunc of [:M,M:],M by A18, RELSET_1:4;
set CAT = CatStr(# O,M,DD,CC,Cm #);
A33:
CatStr(# O,M,DD,CC,Cm #) is Category-like
proof
let f,
g be
Morphism of
CatStr(#
O,
M,
DD,
CC,
Cm #);
CAT_1:def 6 ( ( not [g,f] in proj1 the Comp of CatStr(# O,M,DD,CC,Cm #) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DD,CC,Cm #) ) )
reconsider g9 =
g,
f9 =
f as
Morphism of
C1 by XBOOLE_0:def 4;
A34:
g in the
carrier' of
C2
by XBOOLE_0:def 4;
A35:
f in the
carrier' of
C2
by XBOOLE_0:def 4;
hereby ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DD,CC,Cm #) )
assume
[g,f] in dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
;
dom g = cod fthen A36:
[g,f] in dom the
Comp of
C1
by A17, XBOOLE_0:def 4;
thus dom g =
dom g9
by A34, FUNCT_1:49
.=
cod f9
by A36, CAT_1:def 6
.=
cod f
by A35, FUNCT_1:49
;
verum
end;
assume A37:
dom g = cod f
;
[g,f] in proj1 the Comp of CatStr(# O,M,DD,CC,Cm #)
A38:
dom g = dom g9
by A7, FUNCT_1:47;
A39:
dom g = cod f9
by A8, A37, FUNCT_1:47;
A40:
[g,f] in [: the carrier' of C2, the carrier' of C2:]
by A34, A35, ZFMISC_1:87;
[g,f] in dom the
Comp of
C1
by A38, A39, CAT_1:def 6;
hence
[g,f] in dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
by A17, A40, XBOOLE_0:def 4;
verum
end;
A41:
for f, g being Morphism of CatStr(# O,M,DD,CC,Cm #) holds
( [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) iff dom g = cod f )
by A33;
A42:
CatStr(# O,M,DD,CC,Cm #) is transitive
proof
let f,
g be
Morphism of
CatStr(#
O,
M,
DD,
CC,
Cm #);
CAT_1:def 7 ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
reconsider g9 =
g,
f9 =
f as
Morphism of
C1 by XBOOLE_0:def 4;
assume A43:
dom g = cod f
;
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
then A44:
[g,f] in dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
by A41;
A45:
dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
c= dom the
Comp of
C1
by RELAT_1:60;
reconsider h =
g (*) f as
Morphism of
CatStr(#
O,
M,
DD,
CC,
Cm #) ;
reconsider h9 =
h as
Morphism of
C1 by XBOOLE_0:def 4;
A46:
h =
the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
. (
g,
f)
by A44, CAT_1:def 1
.=
the
Comp of
C1 . (
g9,
f9)
by A44, FUNCT_1:47
.=
g9 (*) f9
by A45, A44, CAT_1:def 1
;
A47:
dom f = dom f9
by A7, FUNCT_1:47;
A48:
dom g = dom g9
by A7, FUNCT_1:47;
A49:
dom h = dom h9
by A7, FUNCT_1:47;
A50:
cod f = cod f9
by A8, FUNCT_1:47;
A51:
cod g = cod g9
by A8, FUNCT_1:47;
A52:
cod h = cod h9
by A8, FUNCT_1:47;
thus
dom (g (*) f) = dom f
by A43, A47, A48, A49, A50, A46, CAT_1:def 7;
cod (g (*) f) = cod g
thus
cod (g (*) f) = cod g
by A43, A46, A48, A50, A51, A52, CAT_1:def 7;
verum
end;
A53:
for f, g being Morphism of CatStr(# O,M,DD,CC,Cm #) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
by A42;
A54:
CatStr(# O,M,DD,CC,Cm #) is associative
proof
let f,
g,
h be
Morphism of
CatStr(#
O,
M,
DD,
CC,
Cm #);
CAT_1:def 8 ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
reconsider h9 =
h,
g9 =
g,
f9 =
f as
Morphism of
C1 by XBOOLE_0:def 4;
assume that A55:
dom h = cod g
and A56:
dom g = cod f
;
h (*) (g (*) f) = (h (*) g) (*) f
A57:
[h,g] in dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
by A41, A55;
A58:
[g,f] in dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
by A41, A56;
then reconsider hg = the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
. (
h,
g),
gf = the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
. (
g,
f) as
Morphism of
CatStr(#
O,
M,
DD,
CC,
Cm #)
by A57, PARTFUN1:4;
reconsider hg9 =
hg,
gf9 =
gf as
Morphism of
C1 by XBOOLE_0:def 4;
A59:
dom hg =
dom (h (*) g)
by A57, CAT_1:def 1
.=
dom g
by A53, A55
;
A60:
cod gf =
cod (g (*) f)
by A58, CAT_1:def 1
.=
cod g
by A53, A56
;
A61:
[hg,f] in dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
by A41, A56, A59;
A62:
[h,gf] in dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
by A41, A55, A60;
A63:
dom h9 = dom h
by A7, FUNCT_1:47;
A64:
cod g9 = cod g
by A8, FUNCT_1:47;
then A65:
h9 (*) g9 = the
Comp of
C1 . (
h9,
g9)
by A63, A55, CAT_1:16;
A66:
dom g9 = dom g
by A7, FUNCT_1:47;
A67:
cod f9 = cod f
by A8, FUNCT_1:47;
then A68:
g9 (*) f9 = the
Comp of
C1 . (
g9,
f9)
by A66, A56, CAT_1:16;
A69:
cod (g9 (*) f9) = cod g9
by A56, A66, A67, CAT_1:def 7;
A70:
dom (h9 (*) g9) = dom g9
by A55, A63, A64, CAT_1:def 7;
A71:
hg = h (*) g
by A57, CAT_1:def 1;
gf = g (*) f
by A58, CAT_1:def 1;
hence h (*) (g (*) f) =
the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
. (
h,
( the Comp of CatStr(# O,M,DD,CC,Cm #) . (g,f)))
by A62, CAT_1:def 1
.=
the
Comp of
C1 . [h9,gf9]
by A62, FUNCT_1:47
.=
the
Comp of
C1 . (
h9,
( the Comp of C1 . (g9,f9)))
by A58, FUNCT_1:47
.=
h9 (*) (g9 (*) f9)
by A69, A68, A55, A63, A64, CAT_1:16
.=
(h9 (*) g9) (*) f9
by A55, A56, A63, A64, A66, A67, CAT_1:def 8
.=
the
Comp of
C1 . (
( the Comp of C1 . (h9,g9)),
f9)
by A70, A65, A56, A66, A67, CAT_1:16
.=
the
Comp of
C1 . [hg9,f9]
by A57, FUNCT_1:47
.=
the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
. (
( the Comp of CatStr(# O,M,DD,CC,Cm #) . (h,g)),
f)
by A61, FUNCT_1:47
.=
(h (*) g) (*) f
by A71, A61, CAT_1:def 1
;
verum
end;
A72:
CatStr(# O,M,DD,CC,Cm #) is reflexive
proof
let b be
Object of
CatStr(#
O,
M,
DD,
CC,
Cm #);
CAT_1:def 9 not Hom (b,b) = {}
reconsider b1 =
b as
Object of
C1 by XBOOLE_0:def 4;
reconsider b2 =
b as
Object of
C2 by XBOOLE_0:def 4;
A73:
the
carrier of
C1 c= the
carrier of
C
by A1, CAT_2:def 4;
reconsider bb =
b1 as
Object of
C by A73;
A74:
id b1 =
id bb
by A1, CAT_2:def 4
.=
id b2
by A2, CAT_2:def 4
;
id b2 in the
carrier' of
C1 /\ the
carrier' of
C2
by A74, XBOOLE_0:def 4;
then
id b2 in M
;
then reconsider ii =
id b2 as
Morphism of
CatStr(#
O,
M,
DD,
CC,
Cm #) ;
A75:
dom ii =
dom (id b1)
by A74, FUNCT_1:49
.=
b
;
cod ii =
cod (id b1)
by A74, FUNCT_1:49
.=
b
;
then
ii in Hom (
b,
b)
by A75;
hence
Hom (
b,
b)
<> {}
;
verum
end;
CatStr(# O,M,DD,CC,Cm #) is with_identities
proof
let a be
Element of
CatStr(#
O,
M,
DD,
CC,
Cm #);
CAT_1:def 10 ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# O,M,DD,CC,Cm #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider a1 =
a as
Object of
C1 by XBOOLE_0:def 4;
reconsider a2 =
a as
Object of
C2 by XBOOLE_0:def 4;
A76:
the
carrier of
C1 c= the
carrier of
C
by A1, CAT_2:def 4;
reconsider aa =
a1 as
Object of
C by A76;
A77:
id a1 =
id aa
by A1, CAT_2:def 4
.=
id a2
by A2, CAT_2:def 4
;
id a2 in the
carrier' of
C1 /\ the
carrier' of
C2
by A77, XBOOLE_0:def 4;
then
id a2 in M
;
then reconsider ii =
id a2 as
Morphism of
CatStr(#
O,
M,
DD,
CC,
Cm #) ;
A78:
dom ii =
dom (id a1)
by A77, FUNCT_1:49
.=
a
;
cod ii =
cod (id a1)
by A77, FUNCT_1:49
.=
a
;
then
ii in Hom (
a,
a)
by A78;
then reconsider ii =
ii as
Morphism of
a,
a by CAT_1:def 5;
take
ii
;
for b1 being Element of the carrier of CatStr(# O,M,DD,CC,Cm #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be
Element of
CatStr(#
O,
M,
DD,
CC,
Cm #);
( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
thus
(
Hom (
a,
b)
<> {} implies for
g being
Morphism of
a,
b holds
g (*) ii = g )
( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )proof
assume A79:
Hom (
a,
b)
<> {}
;
for g being Morphism of a,b holds g (*) ii = g
let g be
Morphism of
a,
b;
g (*) ii = g
g in the
carrier' of
C1
by XBOOLE_0:def 4;
then reconsider gg =
g as
Morphism of
C1 ;
A80:
g in the
carrier' of
C2
by XBOOLE_0:def 4;
A81:
dom gg =
the
Source of
C1 . g
.=
( the Source of C1 | the carrier' of C2) . g
by A80, FUNCT_1:49
.=
dom g
.=
a1
by A79, CAT_1:5
;
A82:
cod (id a1) = a1
;
cod ii =
cod (id a1)
by A77, FUNCT_1:49
.=
dom g
by A79, CAT_1:5
;
then A83:
[g,ii] in dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
by A33;
hence g (*) ii =
Cm . (
g,
ii)
by CAT_1:def 1
.=
( the Comp of C1 || the carrier' of C2) . (
g,
ii)
.=
the
Comp of
C1 . (
gg,
(id a1))
by A77, A83, FUNCT_1:47
.=
gg (*) (id a1)
by A82, A81, CAT_1:16
.=
g
by A81, CAT_1:22
;
verum
end;
assume A84:
Hom (
b,
a)
<> {}
;
for b1 being Morphism of b,a holds ii (*) b1 = b1
let g be
Morphism of
b,
a;
ii (*) g = g
g in the
carrier' of
C1
by XBOOLE_0:def 4;
then reconsider gg =
g as
Morphism of
C1 ;
A85:
g in the
carrier' of
C2
by XBOOLE_0:def 4;
A86:
cod gg =
the
Target of
C1 . g
.=
( the Target of C1 | the carrier' of C2) . g
by A85, FUNCT_1:49
.=
cod g
.=
a1
by A84, CAT_1:5
;
A87:
dom (id a1) = a1
;
dom ii =
dom (id a1)
by A77, FUNCT_1:49
.=
cod g
by A84, CAT_1:5
;
then A88:
[ii,g] in dom the
Comp of
CatStr(#
O,
M,
DD,
CC,
Cm #)
by A33;
hence ii (*) g =
Cm . (
ii,
g)
by CAT_1:def 1
.=
( the Comp of C1 || the carrier' of C2) . (
ii,
g)
.=
the
Comp of
C1 . (
(id a1),
gg)
by A77, A88, FUNCT_1:47
.=
(id a1) (*) gg
by A87, A86, CAT_1:16
.=
g
by A86, CAT_1:21
;
verum
end;
hence
ex b1 being strict Category st
( the carrier of b1 = the carrier of C1 /\ the carrier of C2 & the carrier' of b1 = the carrier' of C1 /\ the carrier' of C2 & the Source of b1 = the Source of C1 | the carrier' of C2 & the Target of b1 = the Target of C1 | the carrier' of C2 & the Comp of b1 = the Comp of C1 || the carrier' of C2 )
by A33, A42, A54, A72; verum