let A be Category; :: thesis: for O being non empty Subset of the carrier of A
for M being non empty Subset of the carrier' of A
for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let O be non empty Subset of the carrier of A; :: thesis: for M being non empty Subset of the carrier' of A
for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let M be non empty Subset of the carrier' of A; :: thesis: for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let DOM, COD be Function of M,O; :: thesis: ( DOM = the Source of A | M & COD = the Target of A | M implies for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A )
assume A1:
( DOM = the Source of A | M & COD = the Target of A | M )
; :: thesis: for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let COMP be PartFunc of [:M,M:],M; :: thesis: ( COMP = the Comp of A || M implies for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A )
assume A2:
COMP = the Comp of A || M
; :: thesis: for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let ID be Function of O,M; :: thesis: ( ID = the Id of A | O implies CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A )
assume A3:
ID = the Id of A | O
; :: thesis: CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
set C = CatStr(# O,M,DOM,COD,COMP,ID #);
A4:
dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) c= dom the Comp of A
by A2, RELAT_1:89;
A5:
now let f be
Morphism of
A;
:: thesis: for g being Morphism of CatStr(# O,M,DOM,COD,COMP,ID #) st f = g holds
( the Source of A . f = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g & the Target of A . f = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g )let g be
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #);
:: thesis: ( f = g implies ( the Source of A . f = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g & the Target of A . f = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g ) )assume A6:
f = g
;
:: thesis: ( the Source of A . f = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g & the Target of A . f = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g )
dom the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
= the
carrier' of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
by FUNCT_2:def 1;
hence
the
Source of
A . f = the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g
by A1, A6, FUNCT_1:70;
:: thesis: the Target of A . f = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g
dom the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
= the
carrier' of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
by FUNCT_2:def 1;
hence
the
Target of
A . f = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g
by A1, A6, FUNCT_1:70;
:: thesis: verum end;
A7:
dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) = (dom the Comp of A) /\ [:the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #),the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #):]
by A2, RELAT_1:90;
A8:
now let f,
g be
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #);
:: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f implies [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) )reconsider g' =
g,
f' =
f as
Morphism of
A by TARSKI:def 3;
assume
the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f
;
:: thesis: [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #)then the
Source of
A . g' =
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f
by A5
.=
the
Target of
A . f'
by A5
;
then A9:
[g',f'] in dom the
Comp of
A
by CAT_1:def 8;
[g,f] in [:the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #),the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #):]
by ZFMISC_1:106;
hence
[g,f] in dom the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
by A7, A9, XBOOLE_0:def 4;
:: thesis: verum end;
CatStr(# O,M,DOM,COD,COMP,ID #) is Category-like
proof
thus
for
f,
g being
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #) holds
(
[g,f] in dom the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #) iff the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f )
:: according to CAT_1:def 8 :: thesis: ( ( for b1, b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 or ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,b1) = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,b1) = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 ) ) ) & ( for b1, b2, b3 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b3 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 or not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b3,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,b1) = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b3,b2),b1 ) ) & ( for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1),b2 = b2 ) ) & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b2 ) ) ) ) )proof
let f,
g be
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #);
:: thesis: ( [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) iff the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f )
reconsider g' =
g,
f' =
f as
Morphism of
A by TARSKI:def 3;
thus
(
[g,f] in dom the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #) implies the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f )
:: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f implies [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) )proof
assume A10:
[g,f] in dom the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
;
:: thesis: the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f
thus the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g =
the
Source of
A . g'
by A5
.=
the
Target of
A . f'
by A4, A10, CAT_1:def 8
.=
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f
by A5
;
:: thesis: verum
end;
thus
( the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f implies
[g,f] in dom the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #) )
by A8;
:: thesis: verum
end;
thus
for
f,
g being
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #) st the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f holds
( the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f & the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g )
:: thesis: ( ( for b1, b2, b3 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b3 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 or not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b3,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,b1) = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b3,b2),b1 ) ) & ( for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1),b2 = b2 ) ) & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b2 ) ) ) ) )proof
let f,
g be
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #);
:: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f implies ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . f & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g ) )
reconsider g' =
g,
f' =
f as
Morphism of
A by TARSKI:def 3;
assume A11:
the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f
;
:: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . f & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g )
then A12: the
Source of
A . g' =
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f
by A5
.=
the
Target of
A . f'
by A5
;
A13:
the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. [g,f] = the
Comp of
A . [g',f']
by A2, A8, A11, FUNCT_1:70;
A14:
the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. [g,f] is
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
by A8, A11, PARTFUN1:27;
then A15:
the
Comp of
A . [g',f'] is
Morphism of
A
by A13, TARSKI:def 3;
hence the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) =
the
Source of
A . (the Comp of A . g',f')
by A5, A13, A14
.=
the
Source of
A . f'
by A12, CAT_1:def 8
.=
the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f
by A5
;
:: thesis: the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g
thus the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) =
the
Target of
A . (the Comp of A . g',f')
by A5, A13, A14, A15
.=
the
Target of
A . g'
by A12, CAT_1:def 8
.=
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g
by A5
;
:: thesis: verum
end;
thus
for
f,
g,
h being
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #) st the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. h = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g & the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f holds
the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. h,
(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,g),
f
:: thesis: for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1),b2 = b2 ) ) & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b2 ) ) )proof
let f,
g,
h be
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #);
:: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . h = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g & the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f implies the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,g),f )
reconsider g' =
g,
f' =
f,
h' =
h as
Morphism of
A by TARSKI:def 3;
assume that A16:
the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. h = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g
and A17:
the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g = the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f
;
:: thesis: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,g),f
A18: the
Source of
A . h' =
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g
by A5, A16
.=
the
Target of
A . g'
by A5
;
A19: the
Source of
A . g' =
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f
by A5, A17
.=
the
Target of
A . f'
by A5
;
A20:
the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. [h,g] = the
Comp of
A . [h',g']
by A2, A8, A16, FUNCT_1:70;
A21:
the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. [g,f] = the
Comp of
A . [g',f']
by A2, A8, A17, FUNCT_1:70;
reconsider gf = the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. [g,f],
hg = the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. [h,g] as
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
by A8, A16, A17, PARTFUN1:27;
(
[g',f'] in dom the
Comp of
A &
[h',g'] in dom the
Comp of
A )
by A18, A19, CAT_1:def 8;
then reconsider gf' = the
Comp of
A . g',
f',
hg' = the
Comp of
A . h',
g' as
Morphism of
A by PARTFUN1:27;
A22: the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. h =
the
Target of
A . g'
by A5, A16
.=
the
Target of
A . gf'
by A19, CAT_1:def 8
.=
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. gf
by A5, A21
;
A23: the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. hg =
the
Source of
A . hg'
by A5, A20
.=
the
Source of
A . g'
by A18, CAT_1:def 8
.=
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f
by A5, A17
;
thus the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. h,
(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) =
the
Comp of
A . h',
(the Comp of A . g',f')
by A2, A8, A21, A22, FUNCT_1:70
.=
the
Comp of
A . (the Comp of A . h',g'),
f'
by A18, A19, CAT_1:def 8
.=
the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,g),
f
by A2, A8, A20, A23, FUNCT_1:70
;
:: thesis: verum
end;
let b be
Object of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #);
:: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),b1 = b1 ) ) & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b1,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b1 ) ) )
reconsider b' =
b as
Object of
A by TARSKI:def 3;
dom the
Id of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
= the
carrier of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
by FUNCT_2:def 1;
then A24:
the
Id of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. b = the
Id of
A . b'
by A3, FUNCT_1:70;
hence the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) =
the
Source of
A . (the Id of A . b')
by A5
.=
b
by CAT_1:def 8
;
:: thesis: ( the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),b1 = b1 ) ) & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b1,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b1 ) ) )
thus the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) =
the
Target of
A . (the Id of A . b')
by A5, A24
.=
b
by CAT_1:def 8
;
:: thesis: ( ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),b1 = b1 ) ) & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b1,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b1 ) ) )
thus
for
f being
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #) st the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f = b holds
the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),
f = f
:: thesis: for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b1,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b1 )proof
let f be
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #);
:: thesis: ( the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f = b implies the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),f = f )
assume A25:
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f = b
;
:: thesis: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),f = f
reconsider f' =
f as
Morphism of
A by TARSKI:def 3;
A26:
the
Target of
A . f' = b'
by A5, A25;
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. f =
the
Target of
A . f'
by A5
.=
the
Source of
A . (the Id of A . b')
by A26, CAT_1:def 8
.=
the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b)
by A5, A24
;
hence the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),
f =
the
Comp of
A . (the Id of A . b'),
f'
by A2, A8, A24, FUNCT_1:70
.=
f
by A26, CAT_1:def 8
;
:: thesis: verum
end;
let g be
Morphism of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #);
:: thesis: ( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = g )
assume A27:
the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g = b
;
:: thesis: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = g
reconsider g' =
g as
Morphism of
A by TARSKI:def 3;
A28:
the
Source of
A . g' = b'
by A5, A27;
the
Source of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g =
the
Source of
A . g'
by A5
.=
the
Target of
A . (the Id of A . b')
by A28, CAT_1:def 8
.=
the
Target of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b)
by A5, A24
;
hence the
Comp of
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #)
. g,
(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) =
the
Comp of
A . g',
(the Id of A . b')
by A2, A8, A24, FUNCT_1:70
.=
g
by A28, CAT_1:def 8
;
:: thesis: verum
end;
then reconsider C = CatStr(# O,M,DOM,COD,COMP,ID #) as Category ;
C is Subcategory of A
proof
thus
the
carrier of
C c= the
carrier of
A
;
:: according to CAT_2:def 4 :: thesis: ( ( for b1, b2 being Element of the carrier of C
for b3, b4 being Element of the carrier of A holds
( not b1 = b3 or not b2 = b4 or Hom b1,b2 c= Hom b3,b4 ) ) & the Comp of C c= the Comp of A & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )
thus
for
a,
b being
Object of
C for
a',
b' being
Object of
A st
a = a' &
b = b' holds
Hom a,
b c= Hom a',
b'
:: thesis: ( the Comp of C c= the Comp of A & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )proof
let a,
b be
Object of
C;
:: thesis: for a', b' being Object of A st a = a' & b = b' holds
Hom a,b c= Hom a',b'let a',
b' be
Object of
A;
:: thesis: ( a = a' & b = b' implies Hom a,b c= Hom a',b' )
assume A29:
(
a = a' &
b = b' )
;
:: thesis: Hom a,b c= Hom a',b'
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Hom a,b or x in Hom a',b' )
assume
x in Hom a,
b
;
:: thesis: x in Hom a',b'
then consider f being
Morphism of
C such that A30:
x = f
and A31:
(
dom f = a &
cod f = b )
;
reconsider f' =
f as
Morphism of
A by TARSKI:def 3;
A32:
dom f' = a'
by A5, A29, A31;
cod f' = b'
by A5, A29, A31;
hence
x in Hom a',
b'
by A30, A32;
:: thesis: verum
end;
thus
the
Comp of
C c= the
Comp of
A
by A2, RELAT_1:88;
:: thesis: for b1 being Element of the carrier of C
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 )
let a be
Object of
C;
:: thesis: for b1 being Element of the carrier of A holds
( not a = b1 or id a = id b1 )let a' be
Object of
A;
:: thesis: ( not a = a' or id a = id a' )
assume A33:
a = a'
;
:: thesis: id a = id a'
dom the
Id of
C = the
carrier of
C
by FUNCT_2:def 1;
hence
id a = id a'
by A3, A33, FUNCT_1:70;
:: thesis: verum
end;
hence
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
; :: thesis: verum