:: ALTCAT_2 semantic presentation
begin
theorem :: ALTCAT_2:1
for X1, X2, a1, a2 being set holds [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]
proof
let X1, X2 be set ; ::_thesis: for a1, a2 being set holds [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]
let a1, a2 be set ; ::_thesis: [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]
A1: ( dom (X1 --> a1) = X1 & dom (X2 --> a2) = X2 ) by FUNCOP_1:13;
then A2: dom ([:X1,X2:] --> [a1,a2]) = [:(dom (X1 --> a1)),(dom (X2 --> a2)):] by FUNCOP_1:13;
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_(X1_-->_a1)_&_y_in_dom_(X2_-->_a2)_holds_
([:X1,X2:]_-->_[a1,a2])_._(x,y)_=_[((X1_-->_a1)_._x),((X2_-->_a2)_._y)]
let x, y be set ; ::_thesis: ( x in dom (X1 --> a1) & y in dom (X2 --> a2) implies ([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)] )
assume A3: ( x in dom (X1 --> a1) & y in dom (X2 --> a2) ) ; ::_thesis: ([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)]
then [x,y] in dom ([:X1,X2:] --> [a1,a2]) by A2, ZFMISC_1:87;
then A4: [x,y] in [:X1,X2:] by FUNCOP_1:13;
( (X1 --> a1) . x = a1 & (X2 --> a2) . y = a2 ) by A1, A3, FUNCOP_1:7;
hence ([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)] by A4, FUNCOP_1:7; ::_thesis: verum
end;
hence [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2] by A2, FUNCT_3:def_8; ::_thesis: verum
end;
registration
let I be set ;
cluster [[0]] I -> Function-yielding ;
coherence
[[0]] I is Function-yielding ;
end;
theorem :: ALTCAT_2:2
for f, g being Function holds ~ (g * f) = g * (~ f)
proof
let f, g be Function; ::_thesis: ~ (g * f) = g * (~ f)
A1: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(g_*_(~_f))_implies_ex_y1,_z1_being_set_st_
(_x_=_[z1,y1]_&_[y1,z1]_in_dom_(g_*_f)_)_)_&_(_ex_y,_z_being_set_st_
(_x_=_[z,y]_&_[y,z]_in_dom_(g_*_f)_)_implies_x_in_dom_(g_*_(~_f))_)_)
let x be set ; ::_thesis: ( ( x in dom (g * (~ f)) implies ex y1, z1 being set st
( x = [z1,y1] & [y1,z1] in dom (g * f) ) ) & ( ex y, z being set st
( x = [z,y] & [y,z] in dom (g * f) ) implies x in dom (g * (~ f)) ) )
hereby ::_thesis: ( ex y, z being set st
( x = [z,y] & [y,z] in dom (g * f) ) implies x in dom (g * (~ f)) )
assume A2: x in dom (g * (~ f)) ; ::_thesis: ex y1, z1 being set st
( x = [z1,y1] & [y1,z1] in dom (g * f) )
then x in dom (~ f) by FUNCT_1:11;
then consider y1, z1 being set such that
A3: x = [z1,y1] and
A4: [y1,z1] in dom f by FUNCT_4:def_2;
take y1 = y1; ::_thesis: ex z1 being set st
( x = [z1,y1] & [y1,z1] in dom (g * f) )
take z1 = z1; ::_thesis: ( x = [z1,y1] & [y1,z1] in dom (g * f) )
thus x = [z1,y1] by A3; ::_thesis: [y1,z1] in dom (g * f)
(~ f) . (z1,y1) in dom g by A2, A3, FUNCT_1:11;
then f . (y1,z1) in dom g by A4, FUNCT_4:def_2;
hence [y1,z1] in dom (g * f) by A4, FUNCT_1:11; ::_thesis: verum
end;
given y, z being set such that A5: x = [z,y] and
A6: [y,z] in dom (g * f) ; ::_thesis: x in dom (g * (~ f))
A7: [y,z] in dom f by A6, FUNCT_1:11;
then A8: x in dom (~ f) by A5, FUNCT_4:def_2;
f . (y,z) in dom g by A6, FUNCT_1:11;
then (~ f) . (z,y) in dom g by A7, FUNCT_4:def_2;
hence x in dom (g * (~ f)) by A5, A8, FUNCT_1:11; ::_thesis: verum
end;
now__::_thesis:_for_y,_z_being_set_st_[y,z]_in_dom_(g_*_f)_holds_
(g_*_(~_f))_._(z,y)_=_(g_*_f)_._(y,z)
let y, z be set ; ::_thesis: ( [y,z] in dom (g * f) implies (g * (~ f)) . (z,y) = (g * f) . (y,z) )
assume A9: [y,z] in dom (g * f) ; ::_thesis: (g * (~ f)) . (z,y) = (g * f) . (y,z)
then [y,z] in dom f by FUNCT_1:11;
then A10: [z,y] in dom (~ f) by FUNCT_4:42;
hence (g * (~ f)) . (z,y) = g . ((~ f) . (z,y)) by FUNCT_1:13
.= g . (f . (y,z)) by A10, FUNCT_4:43
.= (g * f) . (y,z) by A9, FUNCT_1:12 ;
::_thesis: verum
end;
hence ~ (g * f) = g * (~ f) by A1, FUNCT_4:def_2; ::_thesis: verum
end;
theorem :: ALTCAT_2:3
for f, g, h being Function holds ~ (f * [:g,h:]) = (~ f) * [:h,g:]
proof
let f, g, h be Function; ::_thesis: ~ (f * [:g,h:]) = (~ f) * [:h,g:]
A1: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_((~_f)_*_[:h,g:])_implies_ex_z1,_y1_being_set_st_
(_x_=_[y1,z1]_&_[z1,y1]_in_dom_(f_*_[:g,h:])_)_)_&_(_ex_y,_z_being_set_st_
(_x_=_[z,y]_&_[y,z]_in_dom_(f_*_[:g,h:])_)_implies_x_in_dom_((~_f)_*_[:h,g:])_)_)
let x be set ; ::_thesis: ( ( x in dom ((~ f) * [:h,g:]) implies ex z1, y1 being set st
( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) ) & ( ex y, z being set st
( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) ) )
hereby ::_thesis: ( ex y, z being set st
( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) )
assume A2: x in dom ((~ f) * [:h,g:]) ; ::_thesis: ex z1, y1 being set st
( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )
then x in dom [:h,g:] by FUNCT_1:11;
then x in [:(dom h),(dom g):] by FUNCT_3:def_8;
then consider y1, z1 being set such that
A3: ( y1 in dom h & z1 in dom g ) and
A4: x = [y1,z1] by ZFMISC_1:84;
A5: ( [:h,g:] . (y1,z1) = [(h . y1),(g . z1)] & [:g,h:] . (z1,y1) = [(g . z1),(h . y1)] ) by A3, FUNCT_3:def_8;
[:h,g:] . (y1,z1) in dom (~ f) by A2, A4, FUNCT_1:11;
then A6: [:g,h:] . (z1,y1) in dom f by A5, FUNCT_4:42;
take z1 = z1; ::_thesis: ex y1 being set st
( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )
take y1 = y1; ::_thesis: ( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )
thus x = [y1,z1] by A4; ::_thesis: [z1,y1] in dom (f * [:g,h:])
dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def_8;
then [z1,y1] in dom [:g,h:] by A3, ZFMISC_1:87;
hence [z1,y1] in dom (f * [:g,h:]) by A6, FUNCT_1:11; ::_thesis: verum
end;
given y, z being set such that A7: x = [z,y] and
A8: [y,z] in dom (f * [:g,h:]) ; ::_thesis: x in dom ((~ f) * [:h,g:])
A9: [:g,h:] . (y,z) in dom f by A8, FUNCT_1:11;
A10: dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def_8;
[y,z] in dom [:g,h:] by A8, FUNCT_1:11;
then A11: ( y in dom g & z in dom h ) by A10, ZFMISC_1:87;
then ( [:g,h:] . (y,z) = [(g . y),(h . z)] & [:h,g:] . (z,y) = [(h . z),(g . y)] ) by FUNCT_3:def_8;
then A12: [:h,g:] . x in dom (~ f) by A7, A9, FUNCT_4:42;
dom [:h,g:] = [:(dom h),(dom g):] by FUNCT_3:def_8;
then x in dom [:h,g:] by A7, A11, ZFMISC_1:87;
hence x in dom ((~ f) * [:h,g:]) by A12, FUNCT_1:11; ::_thesis: verum
end;
now__::_thesis:_for_y,_z_being_set_st_[y,z]_in_dom_(f_*_[:g,h:])_holds_
((~_f)_*_[:h,g:])_._(z,y)_=_(f_*_[:g,h:])_._(y,z)
let y, z be set ; ::_thesis: ( [y,z] in dom (f * [:g,h:]) implies ((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z) )
assume A13: [y,z] in dom (f * [:g,h:]) ; ::_thesis: ((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z)
then [y,z] in dom [:g,h:] by FUNCT_1:11;
then [y,z] in [:(dom g),(dom h):] by FUNCT_3:def_8;
then A14: ( y in dom g & z in dom h ) by ZFMISC_1:87;
[:g,h:] . (y,z) in dom f by A13, FUNCT_1:11;
then A15: [(g . y),(h . z)] in dom f by A14, FUNCT_3:def_8;
[z,y] in [:(dom h),(dom g):] by A14, ZFMISC_1:87;
then [z,y] in dom [:h,g:] by FUNCT_3:def_8;
hence ((~ f) * [:h,g:]) . (z,y) = (~ f) . ([:h,g:] . (z,y)) by FUNCT_1:13
.= (~ f) . ((h . z),(g . y)) by A14, FUNCT_3:def_8
.= f . ((g . y),(h . z)) by A15, FUNCT_4:def_2
.= f . ([:g,h:] . (y,z)) by A14, FUNCT_3:def_8
.= (f * [:g,h:]) . (y,z) by A13, FUNCT_1:12 ;
::_thesis: verum
end;
hence ~ (f * [:g,h:]) = (~ f) * [:h,g:] by A1, FUNCT_4:def_2; ::_thesis: verum
end;
registration
let f be Function-yielding Function;
cluster ~ f -> Function-yielding ;
coherence
~ f is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom (~ f) or (~ f) . x is set )
assume x in dom (~ f) ; ::_thesis: (~ f) . x is set
then consider z, y being set such that
A1: x = [y,z] and
A2: [z,y] in dom f by FUNCT_4:def_2;
f . (z,y) = (~ f) . (y,z) by A2, FUNCT_4:def_2;
hence (~ f) . x is set by A1; ::_thesis: verum
end;
end;
theorem :: ALTCAT_2:4
for I being set
for A, B, C being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C
proof
let I be set ; ::_thesis: for A, B, C being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C
let A, B, C be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C )
assume A1: A is_transformable_to B ; ::_thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C
let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C
let G be ManySortedFunction of B,C; ::_thesis: G ** F is ManySortedFunction of A,C
reconsider GF = G ** F as ManySortedFunction of I by MSSUBFAM:15;
GF is ManySortedFunction of A,C
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or GF . i is Element of bool [:(A . i),(C . i):] )
assume A2: i in I ; ::_thesis: GF . i is Element of bool [:(A . i),(C . i):]
then reconsider Gi = G . i as Function of (B . i),(C . i) by PBOOLE:def_15;
reconsider Fi = F . i as Function of (A . i),(B . i) by A2, PBOOLE:def_15;
i in dom GF by A2, PARTFUN1:def_2;
then A3: (G ** F) . i = Gi * Fi by PBOOLE:def_19;
( B . i = {} implies A . i = {} ) by A1, A2, PZFMISC1:def_3;
hence GF . i is Element of bool [:(A . i),(C . i):] by A3, FUNCT_2:13; ::_thesis: verum
end;
hence G ** F is ManySortedFunction of A,C ; ::_thesis: verum
end;
registration
let I be set ;
let A be ManySortedSet of [:I,I:];
cluster ~ A -> [:I,I:] -defined ;
coherence
~ A is [:I,I:] -defined ;
end;
registration
let I be set ;
let A be ManySortedSet of [:I,I:];
cluster ~ A -> [:I,I:] -defined total for [:I,I:] -defined Function;
coherence
for b1 being [:I,I:] -defined Function st b1 = ~ A holds
b1 is total ;
end;
theorem :: ALTCAT_2:5
for I1 being set
for I2 being non empty set
for f being Function of I1,I2
for B, C being ManySortedSet of I2
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
proof
let I1 be set ; ::_thesis: for I2 being non empty set
for f being Function of I1,I2
for B, C being ManySortedSet of I2
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
let I2 be non empty set ; ::_thesis: for f being Function of I1,I2
for B, C being ManySortedSet of I2
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
let f be Function of I1,I2; ::_thesis: for B, C being ManySortedSet of I2
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
let B, C be ManySortedSet of I2; ::_thesis: for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
let G be ManySortedFunction of B,C; ::_thesis: G * f is ManySortedFunction of B * f,C * f
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I1 or (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):] )
assume A1: i in I1 ; ::_thesis: (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):]
then A2: G . (f . i) is Function of (B . (f . i)),(C . (f . i)) by FUNCT_2:5, PBOOLE:def_15;
A3: i in dom f by A1, FUNCT_2:def_1;
then ( B . (f . i) = (B * f) . i & C . (f . i) = (C * f) . i ) by FUNCT_1:13;
hence (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):] by A3, A2, FUNCT_1:13; ::_thesis: verum
end;
definition
let I be set ;
let A, B be ManySortedSet of [:I,I:];
let F be ManySortedFunction of A,B;
:: original: ~
redefine func ~ F -> ManySortedFunction of ~ A, ~ B;
coherence
~ F is ManySortedFunction of ~ A, ~ B
proof
reconsider G = ~ F as ManySortedSet of [:I,I:] ;
G is ManySortedFunction of ~ A, ~ B
proof
let ii be set ; :: according to PBOOLE:def_15 ::_thesis: ( not ii in [:I,I:] or G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):] )
assume ii in [:I,I:] ; ::_thesis: G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):]
then consider i1, i2 being set such that
A1: ( i1 in I & i2 in I ) and
A2: ii = [i1,i2] by ZFMISC_1:84;
A3: [i2,i1] in [:I,I:] by A1, ZFMISC_1:87;
dom B = [:I,I:] by PARTFUN1:def_2;
then A4: B . (i2,i1) = (~ B) . (i1,i2) by A3, FUNCT_4:def_2;
dom A = [:I,I:] by PARTFUN1:def_2;
then A5: A . (i2,i1) = (~ A) . (i1,i2) by A3, FUNCT_4:def_2;
dom F = [:I,I:] by PARTFUN1:def_2;
then F . (i2,i1) = G . (i1,i2) by A3, FUNCT_4:def_2;
hence G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):] by A2, A3, A5, A4, PBOOLE:def_15; ::_thesis: verum
end;
hence ~ F is ManySortedFunction of ~ A, ~ B ; ::_thesis: verum
end;
end;
theorem :: ALTCAT_2:6
for I1, I2 being non empty set
for M being ManySortedSet of [:I1,I2:]
for o1 being Element of I1
for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2)
proof
let I1, I2 be non empty set ; ::_thesis: for M being ManySortedSet of [:I1,I2:]
for o1 being Element of I1
for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2)
let M be ManySortedSet of [:I1,I2:]; ::_thesis: for o1 being Element of I1
for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2)
let o1 be Element of I1; ::_thesis: for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2)
let o2 be Element of I2; ::_thesis: (~ M) . (o2,o1) = M . (o1,o2)
[o1,o2] in [:I1,I2:] ;
then [o1,o2] in dom M by PARTFUN1:def_2;
hence (~ M) . (o2,o1) = M . (o1,o2) by FUNCT_4:def_2; ::_thesis: verum
end;
registration
let I1 be set ;
let f, g be ManySortedFunction of I1;
clusterg ** f -> I1 -defined ;
coherence
g ** f is I1 -defined
proof
A1: ( dom f = I1 & dom g = I1 ) by PARTFUN1:def_2;
dom (g ** f) = (dom g) /\ (dom f) by PBOOLE:def_19
.= I1 by A1 ;
hence g ** f is I1 -defined by RELAT_1:def_18; ::_thesis: verum
end;
end;
registration
let I1 be set ;
let f, g be ManySortedFunction of I1;
clusterg ** f -> total ;
coherence
g ** f is total
proof
A1: ( dom f = I1 & dom g = I1 ) by PARTFUN1:def_2;
dom (g ** f) = (dom g) /\ (dom f) by PBOOLE:def_19
.= I1 by A1 ;
hence g ** f is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
begin
definition
let f, g be Function;
predf cc= g means :Def1: :: ALTCAT_2:def 1
( dom f c= dom g & ( for i being set st i in dom f holds
f . i c= g . i ) );
reflexivity
for f being Function holds
( dom f c= dom f & ( for i being set st i in dom f holds
f . i c= f . i ) ) ;
end;
:: deftheorem Def1 defines cc= ALTCAT_2:def_1_:_
for f, g being Function holds
( f cc= g iff ( dom f c= dom g & ( for i being set st i in dom f holds
f . i c= g . i ) ) );
definition
let I, J be set ;
let A be ManySortedSet of I;
let B be ManySortedSet of J;
:: original: cc=
redefine predA cc= B means :Def2: :: ALTCAT_2:def 2
( I c= J & ( for i being set st i in I holds
A . i c= B . i ) );
compatibility
( A cc= B iff ( I c= J & ( for i being set st i in I holds
A . i c= B . i ) ) )
proof
A1: dom A = I by PARTFUN1:def_2;
dom B = J by PARTFUN1:def_2;
hence ( A cc= B implies ( I c= J & ( for i being set st i in I holds
A . i c= B . i ) ) ) by A1, Def1; ::_thesis: ( I c= J & ( for i being set st i in I holds
A . i c= B . i ) implies A cc= B )
assume that
A2: I c= J and
A3: for i being set st i in I holds
A . i c= B . i ; ::_thesis: A cc= B
thus dom A c= dom B by A1, A2, PARTFUN1:def_2; :: according to ALTCAT_2:def_1 ::_thesis: for i being set st i in dom A holds
A . i c= B . i
let i be set ; ::_thesis: ( i in dom A implies A . i c= B . i )
assume i in dom A ; ::_thesis: A . i c= B . i
hence A . i c= B . i by A1, A3; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines cc= ALTCAT_2:def_2_:_
for I, J being set
for A being ManySortedSet of I
for B being ManySortedSet of J holds
( A cc= B iff ( I c= J & ( for i being set st i in I holds
A . i c= B . i ) ) );
theorem Th7: :: ALTCAT_2:7
for I, J being set
for A being ManySortedSet of I
for B being ManySortedSet of J st A cc= B & B cc= A holds
A = B
proof
let I, J be set ; ::_thesis: for A being ManySortedSet of I
for B being ManySortedSet of J st A cc= B & B cc= A holds
A = B
let A be ManySortedSet of I; ::_thesis: for B being ManySortedSet of J st A cc= B & B cc= A holds
A = B
let B be ManySortedSet of J; ::_thesis: ( A cc= B & B cc= A implies A = B )
assume that
A1: A cc= B and
A2: B cc= A ; ::_thesis: A = B
A3: I c= J by A1, Def2;
J c= I by A2, Def2;
then I = J by A3, XBOOLE_0:def_10;
then reconsider B9 = B as ManySortedSet of I ;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
A_._i_=_B9_._i
let i be set ; ::_thesis: ( i in I implies A . i = B9 . i )
assume i in I ; ::_thesis: A . i = B9 . i
then ( A . i c= B . i & B . i c= A . i ) by A1, A2, A3, Def2;
hence A . i = B9 . i by XBOOLE_0:def_10; ::_thesis: verum
end;
hence A = B by PBOOLE:3; ::_thesis: verum
end;
theorem Th8: :: ALTCAT_2:8
for I, J, K being set
for A being ManySortedSet of I
for B being ManySortedSet of J
for C being ManySortedSet of K st A cc= B & B cc= C holds
A cc= C
proof
let I, J, K be set ; ::_thesis: for A being ManySortedSet of I
for B being ManySortedSet of J
for C being ManySortedSet of K st A cc= B & B cc= C holds
A cc= C
let A be ManySortedSet of I; ::_thesis: for B being ManySortedSet of J
for C being ManySortedSet of K st A cc= B & B cc= C holds
A cc= C
let B be ManySortedSet of J; ::_thesis: for C being ManySortedSet of K st A cc= B & B cc= C holds
A cc= C
let C be ManySortedSet of K; ::_thesis: ( A cc= B & B cc= C implies A cc= C )
assume that
A1: A cc= B and
A2: B cc= C ; ::_thesis: A cc= C
A3: I c= J by A1, Def2;
J c= K by A2, Def2;
hence I c= K by A3, XBOOLE_1:1; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in I holds
A . i c= C . i
let i be set ; ::_thesis: ( i in I implies A . i c= C . i )
assume A4: i in I ; ::_thesis: A . i c= C . i
then A5: A . i c= B . i by A1, Def2;
B . i c= C . i by A2, A3, A4, Def2;
hence A . i c= C . i by A5, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: ALTCAT_2:9
for I being set
for A, B being ManySortedSet of I holds
( A cc= B iff A c= B )
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds
( A cc= B iff A c= B )
let A, B be ManySortedSet of I; ::_thesis: ( A cc= B iff A c= B )
thus ( A cc= B implies A c= B ) ::_thesis: ( A c= B implies A cc= B )
proof
assume A1: A cc= B ; ::_thesis: A c= B
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= B . i )
thus ( not i in I or A . i c= B . i ) by A1, Def2; ::_thesis: verum
end;
assume A2: A c= B ; ::_thesis: A cc= B
thus I c= I ; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in I holds
A . i c= B . i
thus for i being set st i in I holds
A . i c= B . i by A2, PBOOLE:def_2; ::_thesis: verum
end;
begin
scheme :: ALTCAT_2:sch 1
OnSingletons{ F1() -> non empty set , F2( set ) -> set , P1[ set ] } :
{ [o,F2(o)] where o is Element of F1() : P1[o] } is Function
proof
set f = { [o,F2(o)] where o is Element of F1() : P1[o] } ;
A1: { [o,F2(o)] where o is Element of F1() : P1[o] } is Function-like
proof
let x, y1, y2 be set ; :: according to FUNCT_1:def_1 ::_thesis: ( not [x,y1] in { [o,F2(o)] where o is Element of F1() : P1[o] } or not [x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] } or y1 = y2 )
assume [x,y1] in { [o,F2(o)] where o is Element of F1() : P1[o] } ; ::_thesis: ( not [x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] } or y1 = y2 )
then consider o1 being Element of F1() such that
A2: [x,y1] = [o1,F2(o1)] and
P1[o1] ;
A3: o1 = x by A2, XTUPLE_0:1;
assume [x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] } ; ::_thesis: y1 = y2
then consider o2 being Element of F1() such that
A4: [x,y2] = [o2,F2(o2)] and
P1[o2] ;
o2 = x by A4, XTUPLE_0:1;
hence y1 = y2 by A2, A4, A3, XTUPLE_0:1; ::_thesis: verum
end;
{ [o,F2(o)] where o is Element of F1() : P1[o] } is Relation-like
proof
let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( not x in { [o,F2(o)] where o is Element of F1() : P1[o] } or ex b1, b2 being set st x = [b1,b2] )
assume x in { [o,F2(o)] where o is Element of F1() : P1[o] } ; ::_thesis: ex b1, b2 being set st x = [b1,b2]
then consider o being Element of F1() such that
A5: x = [o,F2(o)] and
P1[o] ;
take o ; ::_thesis: ex b1 being set st x = [o,b1]
take F2(o) ; ::_thesis: x = [o,F2(o)]
thus x = [o,F2(o)] by A5; ::_thesis: verum
end;
hence { [o,F2(o)] where o is Element of F1() : P1[o] } is Function by A1; ::_thesis: verum
end;
scheme :: ALTCAT_2:sch 2
DomOnSingletons{ F1() -> non empty set , F2() -> Function, F3( set ) -> set , P1[ set ] } :
dom F2() = { o where o is Element of F1() : P1[o] }
provided
A1: F2() = { [o,F3(o)] where o is Element of F1() : P1[o] }
proof
set A = { o where o is Element of F1() : P1[o] } ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in__{__o_where_o_is_Element_of_F1()_:_P1[o]__}__implies_ex_y_being_set_st_[x,y]_in_F2()_)_&_(_ex_y_being_set_st_[x,y]_in_F2()_implies_x_in__{__o_where_o_is_Element_of_F1()_:_P1[o]__}__)_)
let x be set ; ::_thesis: ( ( x in { o where o is Element of F1() : P1[o] } implies ex y being set st [x,y] in F2() ) & ( ex y being set st [x,y] in F2() implies x in { o where o is Element of F1() : P1[o] } ) )
hereby ::_thesis: ( ex y being set st [x,y] in F2() implies x in { o where o is Element of F1() : P1[o] } )
assume x in { o where o is Element of F1() : P1[o] } ; ::_thesis: ex y being set st [x,y] in F2()
then consider o being Element of F1() such that
A2: ( x = o & P1[o] ) ;
take y = F3(o); ::_thesis: [x,y] in F2()
thus [x,y] in F2() by A1, A2; ::_thesis: verum
end;
given y being set such that A3: [x,y] in F2() ; ::_thesis: x in { o where o is Element of F1() : P1[o] }
consider o being Element of F1() such that
A4: [x,y] = [o,F3(o)] and
A5: P1[o] by A1, A3;
x = o by A4, XTUPLE_0:1;
hence x in { o where o is Element of F1() : P1[o] } by A5; ::_thesis: verum
end;
hence dom F2() = { o where o is Element of F1() : P1[o] } by XTUPLE_0:def_12; ::_thesis: verum
end;
scheme :: ALTCAT_2:sch 3
ValOnSingletons{ F1() -> non empty set , F2() -> Function, F3() -> Element of F1(), F4( set ) -> set , P1[ set ] } :
F2() . F3() = F4(F3())
provided
A1: F2() = { [o,F4(o)] where o is Element of F1() : P1[o] } and
A2: P1[F3()]
proof
A3: F2() = { [o,F4(o)] where o is Element of F1() : P1[o] } by A1;
dom F2() = { o where o is Element of F1() : P1[o] } from ALTCAT_2:sch_2(A3);
then A4: F3() in dom F2() by A2;
[F3(),F4(F3())] in { [o,F4(o)] where o is Element of F1() : P1[o] } by A2;
hence F2() . F3() = F4(F3()) by A1, A4, FUNCT_1:def_2; ::_thesis: verum
end;
begin
theorem Th10: :: ALTCAT_2:10
for C being Category
for i, j, k being Object of C holds [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C
proof
let C be Category; ::_thesis: for i, j, k being Object of C holds [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C
let i, j, k be Object of C; ::_thesis: [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in [:(Hom (j,k)),(Hom (i,j)):] or e in dom the Comp of C )
assume A1: e in [:(Hom (j,k)),(Hom (i,j)):] ; ::_thesis: e in dom the Comp of C
then reconsider y = e `1 , x = e `2 as Morphism of C by MCART_1:10;
A2: e `2 in Hom (i,j) by A1, MCART_1:10;
A3: e = [y,x] by A1, MCART_1:21;
e `1 in Hom (j,k) by A1, MCART_1:10;
then dom y = j by CAT_1:1
.= cod x by A2, CAT_1:1 ;
hence e in dom the Comp of C by A3, CAT_1:15; ::_thesis: verum
end;
theorem Th11: :: ALTCAT_2:11
for C being Category
for i, j, k being Object of C holds the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)
proof
let C be Category; ::_thesis: for i, j, k being Object of C holds the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)
let i, j, k be Object of C; ::_thesis: the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] or e in Hom (i,k) )
assume e in the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] ; ::_thesis: e in Hom (i,k)
then consider x being set such that
A1: x in dom the Comp of C and
A2: x in [:(Hom (j,k)),(Hom (i,j)):] and
A3: e = the Comp of C . x by FUNCT_1:def_6;
reconsider y = x `1 , z = x `2 as Morphism of C by A2, MCART_1:10;
A4: ( x = [y,z] & e = the Comp of C . (y,z) ) by A2, A3, MCART_1:21;
A5: x `2 in Hom (i,j) by A2, MCART_1:10;
then A6: z is Morphism of i,j by CAT_1:def_5;
A7: x `1 in Hom (j,k) by A2, MCART_1:10;
then y is Morphism of j,k by CAT_1:def_5;
then y (*) z in Hom (i,k) by A7, A5, A6, CAT_1:23;
hence e in Hom (i,k) by A1, A4, CAT_1:def_1; ::_thesis: verum
end;
definition
let C be non empty non void CatStr ;
func the_hom_sets_of C -> ManySortedSet of [: the carrier of C, the carrier of C:] means :Def3: :: ALTCAT_2:def 3
for i, j being Object of C holds it . (i,j) = Hom (i,j);
existence
ex b1 being ManySortedSet of [: the carrier of C, the carrier of C:] st
for i, j being Object of C holds b1 . (i,j) = Hom (i,j)
proof
deffunc H1( Object of C, Object of C) -> Element of bool the carrier' of C = Hom ($1,$2);
thus ex M being ManySortedSet of [: the carrier of C, the carrier of C:] st
for i, j being Object of C holds M . (i,j) = H1(i,j) from ALTCAT_1:sch_2(); ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of [: the carrier of C, the carrier of C:] st ( for i, j being Object of C holds b1 . (i,j) = Hom (i,j) ) & ( for i, j being Object of C holds b2 . (i,j) = Hom (i,j) ) holds
b1 = b2
proof
let M1, M2 be ManySortedSet of [: the carrier of C, the carrier of C:]; ::_thesis: ( ( for i, j being Object of C holds M1 . (i,j) = Hom (i,j) ) & ( for i, j being Object of C holds M2 . (i,j) = Hom (i,j) ) implies M1 = M2 )
assume that
A1: for i, j being Object of C holds M1 . (i,j) = Hom (i,j) and
A2: for i, j being Object of C holds M2 . (i,j) = Hom (i,j) ; ::_thesis: M1 = M2
now__::_thesis:_for_i,_j_being_Object_of_C_holds_M1_._(i,j)_=_M2_._(i,j)
let i, j be Object of C; ::_thesis: M1 . (i,j) = M2 . (i,j)
thus M1 . (i,j) = Hom (i,j) by A1
.= M2 . (i,j) by A2 ; ::_thesis: verum
end;
hence M1 = M2 by ALTCAT_1:7; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines the_hom_sets_of ALTCAT_2:def_3_:_
for C being non empty non void CatStr
for b2 being ManySortedSet of [: the carrier of C, the carrier of C:] holds
( b2 = the_hom_sets_of C iff for i, j being Object of C holds b2 . (i,j) = Hom (i,j) );
theorem Th12: :: ALTCAT_2:12
for C being Category
for i being Object of C holds id i in (the_hom_sets_of C) . (i,i)
proof
let C be Category; ::_thesis: for i being Object of C holds id i in (the_hom_sets_of C) . (i,i)
let i be Object of C; ::_thesis: id i in (the_hom_sets_of C) . (i,i)
id i in Hom (i,i) by CAT_1:27;
hence id i in (the_hom_sets_of C) . (i,i) by Def3; ::_thesis: verum
end;
definition
let C be Category;
func the_comps_of C -> BinComp of (the_hom_sets_of C) means :Def4: :: ALTCAT_2:def 4
for i, j, k being Object of C holds it . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):];
existence
ex b1 being BinComp of (the_hom_sets_of C) st
for i, j, k being Object of C holds b1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]
proof
deffunc H1( set ) -> Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] = the Comp of C | [:((the_hom_sets_of C) . ((($1 `1) `2),($1 `2))),((the_hom_sets_of C) . ((($1 `1) `1),(($1 `1) `2))):];
set Ob3 = [: the carrier of C, the carrier of C, the carrier of C:];
set G = the_hom_sets_of C;
consider o being Function such that
A1: dom o = [: the carrier of C, the carrier of C, the carrier of C:] and
A2: for e being set st e in [: the carrier of C, the carrier of C, the carrier of C:] holds
o . e = H1(e) from FUNCT_1:sch_3();
reconsider o = o as ManySortedSet of [: the carrier of C, the carrier of C, the carrier of C:] by A1, PARTFUN1:def_2, RELAT_1:def_18;
now__::_thesis:_for_e_being_set_st_e_in_dom_o_holds_
o_._e_is_Function
let e be set ; ::_thesis: ( e in dom o implies o . e is Function )
assume e in dom o ; ::_thesis: o . e is Function
then o . e = the Comp of C | [:((the_hom_sets_of C) . (((e `1) `2),(e `2))),((the_hom_sets_of C) . (((e `1) `1),((e `1) `2))):] by A1, A2;
hence o . e is Function ; ::_thesis: verum
end;
then reconsider o = o as ManySortedFunction of [: the carrier of C, the carrier of C, the carrier of C:] by FUNCOP_1:def_6;
now__::_thesis:_for_e_being_set_st_e_in_[:_the_carrier_of_C,_the_carrier_of_C,_the_carrier_of_C:]_holds_
o_._e_is_Function_of_({|(the_hom_sets_of_C),(the_hom_sets_of_C)|}_._e),({|(the_hom_sets_of_C)|}_._e)
let e be set ; ::_thesis: ( e in [: the carrier of C, the carrier of C, the carrier of C:] implies o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e) )
reconsider f = o . e as Function ;
assume A3: e in [: the carrier of C, the carrier of C, the carrier of C:] ; ::_thesis: o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e)
then consider i, j, k being Object of C such that
A4: e = [i,j,k] by DOMAIN_1:3;
reconsider e9 = e as Element of [: the carrier of C, the carrier of C, the carrier of C:] by A3;
A5: ([i,j,k] `1) `2 = e9 `2_3 by A4
.= j by A4, MCART_1:def_6 ;
A6: [i,j,k] `2 = e9 `3_3 by A4
.= k by A4, MCART_1:def_7 ;
([i,j,k] `1) `1 = e9 `1_3 by A4
.= i by A4, MCART_1:def_5 ;
then A7: f = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A2, A4, A5, A6;
A8: ( (the_hom_sets_of C) . (i,j) = Hom (i,j) & (the_hom_sets_of C) . (j,k) = Hom (j,k) ) by Def3;
A9: {|(the_hom_sets_of C)|} . e = {|(the_hom_sets_of C)|} . (i,j,k) by A4, MULTOP_1:def_1
.= (the_hom_sets_of C) . (i,k) by ALTCAT_1:def_3
.= Hom (i,k) by Def3 ;
A10: {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e = {|(the_hom_sets_of C),(the_hom_sets_of C)|} . (i,j,k) by A4, MULTOP_1:def_1
.= [:(Hom (j,k)),(Hom (i,j)):] by A8, ALTCAT_1:def_4 ;
the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k) by Th11;
then A11: rng f c= {|(the_hom_sets_of C)|} . e by A8, A7, A9, RELAT_1:115;
[:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C by Th10;
then dom f = {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e by A8, A7, A10, RELAT_1:62;
hence o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e) by A11, FUNCT_2:2; ::_thesis: verum
end;
then reconsider o = o as BinComp of (the_hom_sets_of C) by PBOOLE:def_15;
take o ; ::_thesis: for i, j, k being Object of C holds o . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]
let i, j, k be Object of C; ::_thesis: o . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]
reconsider e = [i,j,k] as Element of [: the carrier of C, the carrier of C, the carrier of C:] ;
A12: ([i,j,k] `1) `1 = e `1_3
.= i by MCART_1:def_5 ;
A13: ([i,j,k] `1) `2 = e `2_3
.= j by MCART_1:def_6 ;
A14: [i,j,k] `2 = e `3_3
.= k by MCART_1:def_7 ;
thus o . (i,j,k) = o . [i,j,k] by MULTOP_1:def_1
.= the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A2, A12, A13, A14 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinComp of (the_hom_sets_of C) st ( for i, j, k being Object of C holds b1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) & ( for i, j, k being Object of C holds b2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) holds
b1 = b2
proof
let o1, o2 be BinComp of (the_hom_sets_of C); ::_thesis: ( ( for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) & ( for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) implies o1 = o2 )
assume that
A15: for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] and
A16: for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ; ::_thesis: o1 = o2
now__::_thesis:_for_a_being_set_st_a_in_[:_the_carrier_of_C,_the_carrier_of_C,_the_carrier_of_C:]_holds_
o1_._a_=_o2_._a
let a be set ; ::_thesis: ( a in [: the carrier of C, the carrier of C, the carrier of C:] implies o1 . a = o2 . a )
assume a in [: the carrier of C, the carrier of C, the carrier of C:] ; ::_thesis: o1 . a = o2 . a
then consider i, j, k being Object of C such that
A17: a = [i,j,k] by DOMAIN_1:3;
thus o1 . a = o1 . (i,j,k) by A17, MULTOP_1:def_1
.= the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A15
.= o2 . (i,j,k) by A16
.= o2 . a by A17, MULTOP_1:def_1 ; ::_thesis: verum
end;
hence o1 = o2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines the_comps_of ALTCAT_2:def_4_:_
for C being Category
for b2 being BinComp of (the_hom_sets_of C) holds
( b2 = the_comps_of C iff for i, j, k being Object of C holds b2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] );
theorem Th13: :: ALTCAT_2:13
for C being Category
for i, j, k being Object of C st Hom (i,j) <> {} & Hom (j,k) <> {} holds
for f being Morphism of i,j
for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f
proof
let C be Category; ::_thesis: for i, j, k being Object of C st Hom (i,j) <> {} & Hom (j,k) <> {} holds
for f being Morphism of i,j
for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f
let i, j, k be Object of C; ::_thesis: ( Hom (i,j) <> {} & Hom (j,k) <> {} implies for f being Morphism of i,j
for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f )
assume that
A1: Hom (i,j) <> {} and
A2: Hom (j,k) <> {} ; ::_thesis: for f being Morphism of i,j
for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f
let f be Morphism of i,j; ::_thesis: for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f
let g be Morphism of j,k; ::_thesis: ((the_comps_of C) . (i,j,k)) . (g,f) = g * f
A3: g in Hom (j,k) by A2, CAT_1:def_5;
then A4: g in (the_hom_sets_of C) . (j,k) by Def3;
A5: f in Hom (i,j) by A1, CAT_1:def_5;
then f in (the_hom_sets_of C) . (i,j) by Def3;
then A6: [g,f] in [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A4, ZFMISC_1:87;
A7: dom g = j by A3, CAT_1:1
.= cod f by A5, CAT_1:1 ;
thus ((the_comps_of C) . (i,j,k)) . (g,f) = ( the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]) . [g,f] by Def4
.= the Comp of C . (g,f) by A6, FUNCT_1:49
.= g (*) f by A7, CAT_1:16
.= g * f by A1, A2, CAT_1:def_13 ; ::_thesis: verum
end;
theorem Th14: :: ALTCAT_2:14
for C being Category holds the_comps_of C is associative
proof
let C be Category; ::_thesis: the_comps_of C is associative
let i, j, k, l be Object of C; :: according to ALTCAT_1:def_5 ::_thesis: for b1, b2, b3 being set holds
( not b1 in (the_hom_sets_of C) . (i,j) or not b2 in (the_hom_sets_of C) . (j,k) or not b3 in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (b3,(((the_comps_of C) . (i,j,k)) . (b2,b1))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (b3,b2)),b1) )
let f, g, h be set ; ::_thesis: ( not f in (the_hom_sets_of C) . (i,j) or not g in (the_hom_sets_of C) . (j,k) or not h in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) )
assume f in (the_hom_sets_of C) . (i,j) ; ::_thesis: ( not g in (the_hom_sets_of C) . (j,k) or not h in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) )
then A1: f in Hom (i,j) by Def3;
then reconsider f9 = f as Morphism of i,j by CAT_1:def_5;
assume g in (the_hom_sets_of C) . (j,k) ; ::_thesis: ( not h in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) )
then A2: g in Hom (j,k) by Def3;
then reconsider g9 = g as Morphism of j,k by CAT_1:def_5;
assume h in (the_hom_sets_of C) . (k,l) ; ::_thesis: ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f)
then A3: h in Hom (k,l) by Def3;
then reconsider h9 = h as Morphism of k,l by CAT_1:def_5;
A4: ( Hom (j,l) <> {} & ((the_comps_of C) . (j,k,l)) . (h,g) = h9 * g9 ) by A2, A3, Th13, CAT_1:24;
( Hom (i,k) <> {} & ((the_comps_of C) . (i,j,k)) . (g,f) = g9 * f9 ) by A1, A2, Th13, CAT_1:24;
hence ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = h9 * (g9 * f9) by A3, Th13
.= (h9 * g9) * f9 by A1, A2, A3, CAT_1:25
.= ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) by A1, A4, Th13 ;
::_thesis: verum
end;
theorem Th15: :: ALTCAT_2:15
for C being Category holds
( the_comps_of C is with_left_units & the_comps_of C is with_right_units )
proof
let C be Category; ::_thesis: ( the_comps_of C is with_left_units & the_comps_of C is with_right_units )
thus the_comps_of C is with_left_units ::_thesis: the_comps_of C is with_right_units
proof
let i be Object of C; :: according to ALTCAT_1:def_7 ::_thesis: ex b1 being set st
( b1 in (the_hom_sets_of C) . (i,i) & ( for b2 being Element of the carrier of C
for b3 being set holds
( not b3 in (the_hom_sets_of C) . (b2,i) or ((the_comps_of C) . (b2,i,i)) . (b1,b3) = b3 ) ) )
take id i ; ::_thesis: ( id i in (the_hom_sets_of C) . (i,i) & ( for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in (the_hom_sets_of C) . (b1,i) or ((the_comps_of C) . (b1,i,i)) . ((id i),b2) = b2 ) ) )
thus id i in (the_hom_sets_of C) . (i,i) by Th12; ::_thesis: for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in (the_hom_sets_of C) . (b1,i) or ((the_comps_of C) . (b1,i,i)) . ((id i),b2) = b2 )
let j be Object of C; ::_thesis: for b1 being set holds
( not b1 in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,i,i)) . ((id i),b1) = b1 )
let f be set ; ::_thesis: ( not f in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,i,i)) . ((id i),f) = f )
assume f in (the_hom_sets_of C) . (j,i) ; ::_thesis: ((the_comps_of C) . (j,i,i)) . ((id i),f) = f
then A1: f in Hom (j,i) by Def3;
then reconsider m = f as Morphism of j,i by CAT_1:def_5;
Hom (i,i) <> {} ;
hence ((the_comps_of C) . (j,i,i)) . ((id i),f) = (id i) * m by A1, Th13
.= f by A1, CAT_1:28 ;
::_thesis: verum
end;
let j be Object of C; :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st
( b1 in (the_hom_sets_of C) . (j,j) & ( for b2 being Element of the carrier of C
for b3 being set holds
( not b3 in (the_hom_sets_of C) . (j,b2) or ((the_comps_of C) . (j,j,b2)) . (b3,b1) = b3 ) ) )
take id j ; ::_thesis: ( id j in (the_hom_sets_of C) . (j,j) & ( for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in (the_hom_sets_of C) . (j,b1) or ((the_comps_of C) . (j,j,b1)) . (b2,(id j)) = b2 ) ) )
thus id j in (the_hom_sets_of C) . (j,j) by Th12; ::_thesis: for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in (the_hom_sets_of C) . (j,b1) or ((the_comps_of C) . (j,j,b1)) . (b2,(id j)) = b2 )
let i be Object of C; ::_thesis: for b1 being set holds
( not b1 in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,j,i)) . (b1,(id j)) = b1 )
let f be set ; ::_thesis: ( not f in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,j,i)) . (f,(id j)) = f )
assume f in (the_hom_sets_of C) . (j,i) ; ::_thesis: ((the_comps_of C) . (j,j,i)) . (f,(id j)) = f
then A2: f in Hom (j,i) by Def3;
then reconsider m = f as Morphism of j,i by CAT_1:def_5;
Hom (j,j) <> {} ;
hence ((the_comps_of C) . (j,j,i)) . (f,(id j)) = m * (id j) by A2, Th13
.= f by A2, CAT_1:29 ;
::_thesis: verum
end;
begin
definition
let C be Category;
func Alter C -> non empty strict AltCatStr equals :: ALTCAT_2:def 5
AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #);
correctness
coherence
AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #) is non empty strict AltCatStr ;
;
end;
:: deftheorem defines Alter ALTCAT_2:def_5_:_
for C being Category holds Alter C = AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #);
theorem Th16: :: ALTCAT_2:16
for C being Category holds Alter C is associative
proof
let C be Category; ::_thesis: Alter C is associative
thus the Comp of (Alter C) is associative by Th14; :: according to ALTCAT_1:def_15 ::_thesis: verum
end;
theorem Th17: :: ALTCAT_2:17
for C being Category holds Alter C is with_units
proof
let C be Category; ::_thesis: Alter C is with_units
thus ( the Comp of (Alter C) is with_left_units & the Comp of (Alter C) is with_right_units ) by Th15; :: according to ALTCAT_1:def_16 ::_thesis: verum
end;
theorem Th18: :: ALTCAT_2:18
for C being Category holds Alter C is transitive
proof
let C be Category; ::_thesis: Alter C is transitive
let o1, o2, o3 be object of (Alter C); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: not <^o1,o3^> = {}
reconsider x1 = o1, x2 = o2, x3 = o3 as Object of C ;
A2: <^o1,o3^> = Hom (x1,x3) by Def3;
( <^o1,o2^> = Hom (x1,x2) & <^o2,o3^> = Hom (x2,x3) ) by Def3;
hence not <^o1,o3^> = {} by A1, A2, CAT_1:24; ::_thesis: verum
end;
registration
let C be Category;
cluster Alter C -> non empty transitive strict associative with_units ;
coherence
( Alter C is transitive & Alter C is associative & Alter C is with_units ) by Th16, Th17, Th18;
end;
begin
registration
cluster non empty strict for AltGraph ;
existence
ex b1 being AltGraph st
( not b1 is empty & b1 is strict )
proof
set M = the ManySortedSet of [:1,1:];
take A = AltGraph(# 1, the ManySortedSet of [:1,1:] #); ::_thesis: ( not A is empty & A is strict )
thus not the carrier of A is empty ; :: according to STRUCT_0:def_1 ::_thesis: A is strict
thus A is strict ; ::_thesis: verum
end;
end;
definition
let C be AltGraph ;
attrC is reflexive means :Def6: :: ALTCAT_2:def 6
for x being set st x in the carrier of C holds
the Arrows of C . (x,x) <> {} ;
end;
:: deftheorem Def6 defines reflexive ALTCAT_2:def_6_:_
for C being AltGraph holds
( C is reflexive iff for x being set st x in the carrier of C holds
the Arrows of C . (x,x) <> {} );
definition
let C be non empty AltGraph ;
redefine attr C is reflexive means :: ALTCAT_2:def 7
for o being object of C holds <^o,o^> <> {} ;
compatibility
( C is reflexive iff for o being object of C holds <^o,o^> <> {} )
proof
thus ( C is reflexive implies for o being object of C holds <^o,o^> <> {} ) by Def6; ::_thesis: ( ( for o being object of C holds <^o,o^> <> {} ) implies C is reflexive )
assume A1: for o being object of C holds <^o,o^> <> {} ; ::_thesis: C is reflexive
let x be set ; :: according to ALTCAT_2:def_6 ::_thesis: ( x in the carrier of C implies the Arrows of C . (x,x) <> {} )
assume x in the carrier of C ; ::_thesis: the Arrows of C . (x,x) <> {}
then reconsider o = x as object of C ;
the Arrows of C . (x,x) = <^o,o^> ;
hence the Arrows of C . (x,x) <> {} by A1; ::_thesis: verum
end;
end;
:: deftheorem defines reflexive ALTCAT_2:def_7_:_
for C being non empty AltGraph holds
( C is reflexive iff for o being object of C holds <^o,o^> <> {} );
definition
let C be non empty transitive AltCatStr ;
redefine attr C is associative means :Def8: :: ALTCAT_2:def 8
for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f);
compatibility
( C is associative iff for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) )
proof
thus ( C is associative implies for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) ) by ALTCAT_1:21; ::_thesis: ( ( for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) ) implies C is associative )
assume A1: for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) ; ::_thesis: C is associative
let i, j, k, l be Element of C; :: according to ALTCAT_1:def_5,ALTCAT_1:def_15 ::_thesis: for b1, b2, b3 being set holds
( not b1 in the Arrows of C . (i,j) or not b2 in the Arrows of C . (j,k) or not b3 in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (b3,(( the Comp of C . (i,j,k)) . (b2,b1))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (b3,b2)),b1) )
reconsider o1 = i, o2 = j, o3 = k, o4 = l as object of C ;
let f, g, h be set ; ::_thesis: ( not f in the Arrows of C . (i,j) or not g in the Arrows of C . (j,k) or not h in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) )
assume A2: f in the Arrows of C . (i,j) ; ::_thesis: ( not g in the Arrows of C . (j,k) or not h in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) )
then reconsider ff = f as Morphism of o1,o2 ;
assume A3: g in the Arrows of C . (j,k) ; ::_thesis: ( not h in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) )
then A4: g in <^o2,o3^> ;
f in <^o1,o2^> by A2;
then A5: <^o1,o3^> <> {} by A4, ALTCAT_1:def_2;
reconsider gg = g as Morphism of o2,o3 by A3;
assume A6: h in the Arrows of C . (k,l) ; ::_thesis: ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f)
then reconsider hh = h as Morphism of o3,o4 ;
A7: ( the Comp of C . (j,k,l)) . (h,g) = hh * gg by A3, A6, ALTCAT_1:def_8;
h in <^o3,o4^> by A6;
then A8: <^o2,o4^> <> {} by A4, ALTCAT_1:def_2;
( the Comp of C . (i,j,k)) . (g,f) = gg * ff by A2, A3, ALTCAT_1:def_8;
hence ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = hh * (gg * ff) by A6, A5, ALTCAT_1:def_8
.= (hh * gg) * ff by A1, A2, A3, A6
.= ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) by A2, A8, A7, ALTCAT_1:def_8 ;
::_thesis: verum
end;
end;
:: deftheorem Def8 defines associative ALTCAT_2:def_8_:_
for C being non empty transitive AltCatStr holds
( C is associative iff for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) );
definition
let C be non empty AltCatStr ;
redefine attr C is with_units means :: ALTCAT_2:def 9
for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) );
compatibility
( C is with_units iff for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) )
proof
hereby ::_thesis: ( ( for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) ) implies C is with_units )
assume A1: C is with_units ; ::_thesis: for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) )
then reconsider C9 = C as non empty with_units AltCatStr ;
let o be object of C; ::_thesis: ( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) )
thus <^o,o^> <> {} by A1, ALTCAT_1:18; ::_thesis: ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
reconsider p = o as object of C9 ;
reconsider i = idm p as Morphism of o,o ;
take i = i; ::_thesis: for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
let o9 be object of C; ::_thesis: for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
let m9 be Morphism of o9,o; ::_thesis: for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
let m99 be Morphism of o,o9; ::_thesis: ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
thus ( <^o9,o^> <> {} implies i * m9 = m9 ) by ALTCAT_1:20; ::_thesis: ( <^o,o9^> <> {} implies m99 * i = m99 )
thus ( <^o,o9^> <> {} implies m99 * i = m99 ) by ALTCAT_1:def_17; ::_thesis: verum
end;
assume A2: for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) ; ::_thesis: C is with_units
hereby :: according to ALTCAT_1:def_7,ALTCAT_1:def_16 ::_thesis: the Comp of C is with_right_units
let j be Element of C; ::_thesis: ex e being set st
( e in the Arrows of C . (j,j) & ( for i being Element of C
for f being set st f in the Arrows of C . (i,j) holds
( the Comp of C . (i,j,j)) . (e,f) = f ) )
reconsider o = j as object of C ;
consider m being Morphism of o,o such that
A3: for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies m * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * m = m99 ) ) by A2;
reconsider e = m as set ;
take e = e; ::_thesis: ( e in the Arrows of C . (j,j) & ( for i being Element of C
for f being set st f in the Arrows of C . (i,j) holds
( the Comp of C . (i,j,j)) . (e,f) = f ) )
A4: <^o,o^> <> {} by A2;
hence e in the Arrows of C . (j,j) ; ::_thesis: for i being Element of C
for f being set st f in the Arrows of C . (i,j) holds
( the Comp of C . (i,j,j)) . (e,f) = f
let i be Element of C; ::_thesis: for f being set st f in the Arrows of C . (i,j) holds
( the Comp of C . (i,j,j)) . (e,f) = f
let f be set ; ::_thesis: ( f in the Arrows of C . (i,j) implies ( the Comp of C . (i,j,j)) . (e,f) = f )
assume A5: f in the Arrows of C . (i,j) ; ::_thesis: ( the Comp of C . (i,j,j)) . (e,f) = f
reconsider o9 = i as object of C ;
reconsider m9 = f as Morphism of o9,o by A5;
thus ( the Comp of C . (i,j,j)) . (e,f) = m * m9 by A4, A5, ALTCAT_1:def_8
.= f by A3, A5 ; ::_thesis: verum
end;
let i be Element of C; :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st
( b1 in the Arrows of C . (i,i) & ( for b2 being Element of the carrier of C
for b3 being set holds
( not b3 in the Arrows of C . (i,b2) or ( the Comp of C . (i,i,b2)) . (b3,b1) = b3 ) ) )
reconsider o = i as object of C ;
consider m being Morphism of o,o such that
A6: for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies m * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * m = m99 ) ) by A2;
take e = m; ::_thesis: ( e in the Arrows of C . (i,i) & ( for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in the Arrows of C . (i,b1) or ( the Comp of C . (i,i,b1)) . (b2,e) = b2 ) ) )
A7: <^o,o^> <> {} by A2;
hence e in the Arrows of C . (i,i) ; ::_thesis: for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in the Arrows of C . (i,b1) or ( the Comp of C . (i,i,b1)) . (b2,e) = b2 )
let j be Element of C; ::_thesis: for b1 being set holds
( not b1 in the Arrows of C . (i,j) or ( the Comp of C . (i,i,j)) . (b1,e) = b1 )
let f be set ; ::_thesis: ( not f in the Arrows of C . (i,j) or ( the Comp of C . (i,i,j)) . (f,e) = f )
assume A8: f in the Arrows of C . (i,j) ; ::_thesis: ( the Comp of C . (i,i,j)) . (f,e) = f
reconsider o9 = j as object of C ;
reconsider m9 = f as Morphism of o,o9 by A8;
thus ( the Comp of C . (i,i,j)) . (f,e) = m9 * m by A7, A8, ALTCAT_1:def_8
.= f by A6, A8 ; ::_thesis: verum
end;
end;
:: deftheorem defines with_units ALTCAT_2:def_9_:_
for C being non empty AltCatStr holds
( C is with_units iff for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) );
registration
cluster non empty with_units -> non empty reflexive for AltCatStr ;
coherence
for b1 being non empty AltCatStr st b1 is with_units holds
b1 is reflexive
proof
let C be non empty AltCatStr ; ::_thesis: ( C is with_units implies C is reflexive )
assume A1: C is with_units ; ::_thesis: C is reflexive
let o be object of C; :: according to ALTCAT_2:def_7 ::_thesis: <^o,o^> <> {}
thus <^o,o^> <> {} by A1, ALTCAT_1:18; ::_thesis: verum
end;
end;
registration
cluster non empty reflexive for AltGraph ;
existence
ex b1 being AltGraph st
( not b1 is empty & b1 is reflexive )
proof
set C = the non empty with_units AltCatStr ;
take the non empty with_units AltCatStr ; ::_thesis: ( not the non empty with_units AltCatStr is empty & the non empty with_units AltCatStr is reflexive )
thus ( not the non empty with_units AltCatStr is empty & the non empty with_units AltCatStr is reflexive ) ; ::_thesis: verum
end;
end;
registration
cluster non empty reflexive for AltCatStr ;
existence
ex b1 being AltCatStr st
( not b1 is empty & b1 is reflexive )
proof
set C = the category;
take the category ; ::_thesis: ( not the category is empty & the category is reflexive )
thus ( not the category is empty & the category is reflexive ) ; ::_thesis: verum
end;
end;
begin
Lm1: for E1, E2 being strict AltCatStr st the carrier of E1 is empty & the carrier of E2 is empty holds
E1 = E2
proof
let E1, E2 be strict AltCatStr ; ::_thesis: ( the carrier of E1 is empty & the carrier of E2 is empty implies E1 = E2 )
set C1 = the carrier of E1;
set C2 = the carrier of E2;
assume that
A1: the carrier of E1 is empty and
A2: the carrier of E2 is empty ; ::_thesis: E1 = E2
A3: [: the carrier of E2, the carrier of E2, the carrier of E2:] = {} by A2, MCART_1:31;
[: the carrier of E1, the carrier of E1, the carrier of E1:] = {} by A1, MCART_1:31;
then A4: the Comp of E1 = {}
.= the Comp of E2 by A3 ;
A5: [: the carrier of E2, the carrier of E2:] = {} by A2, ZFMISC_1:90;
[: the carrier of E1, the carrier of E1:] = {} by A1, ZFMISC_1:90;
then the Arrows of E1 = {}
.= the Arrows of E2 by A5 ;
hence E1 = E2 by A1, A2, A4; ::_thesis: verum
end;
definition
func the_empty_category -> strict AltCatStr means :Def10: :: ALTCAT_2:def 10
the carrier of it is empty ;
existence
ex b1 being strict AltCatStr st the carrier of b1 is empty
proof
reconsider a = {} as set ;
set m = the ManySortedSet of [:a,a:];
set c = the BinComp of the ManySortedSet of [:a,a:];
take AltCatStr(# a, the ManySortedSet of [:a,a:], the BinComp of the ManySortedSet of [:a,a:] #) ; ::_thesis: the carrier of AltCatStr(# a, the ManySortedSet of [:a,a:], the BinComp of the ManySortedSet of [:a,a:] #) is empty
thus the carrier of AltCatStr(# a, the ManySortedSet of [:a,a:], the BinComp of the ManySortedSet of [:a,a:] #) is empty ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict AltCatStr st the carrier of b1 is empty & the carrier of b2 is empty holds
b1 = b2 by Lm1;
end;
:: deftheorem Def10 defines the_empty_category ALTCAT_2:def_10_:_
for b1 being strict AltCatStr holds
( b1 = the_empty_category iff the carrier of b1 is empty );
registration
cluster the_empty_category -> empty strict ;
coherence
the_empty_category is empty by Def10;
end;
registration
cluster empty strict for AltCatStr ;
existence
ex b1 being AltCatStr st
( b1 is empty & b1 is strict )
proof
take the_empty_category ; ::_thesis: ( the_empty_category is empty & the_empty_category is strict )
thus ( the_empty_category is empty & the_empty_category is strict ) ; ::_thesis: verum
end;
end;
theorem :: ALTCAT_2:19
for E being empty strict AltCatStr holds E = the_empty_category by Lm1;
begin
definition
let C be AltCatStr ;
mode SubCatStr of C -> AltCatStr means :Def11: :: ALTCAT_2:def 11
( the carrier of it c= the carrier of C & the Arrows of it cc= the Arrows of C & the Comp of it cc= the Comp of C );
existence
ex b1 being AltCatStr st
( the carrier of b1 c= the carrier of C & the Arrows of b1 cc= the Arrows of C & the Comp of b1 cc= the Comp of C ) ;
end;
:: deftheorem Def11 defines SubCatStr ALTCAT_2:def_11_:_
for C, b2 being AltCatStr holds
( b2 is SubCatStr of C iff ( the carrier of b2 c= the carrier of C & the Arrows of b2 cc= the Arrows of C & the Comp of b2 cc= the Comp of C ) );
theorem Th20: :: ALTCAT_2:20
for C being AltCatStr holds C is SubCatStr of C
proof
let C be AltCatStr ; ::_thesis: C is SubCatStr of C
thus the carrier of C c= the carrier of C ; :: according to ALTCAT_2:def_11 ::_thesis: ( the Arrows of C cc= the Arrows of C & the Comp of C cc= the Comp of C )
thus ( the Arrows of C cc= the Arrows of C & the Comp of C cc= the Comp of C ) ; ::_thesis: verum
end;
theorem :: ALTCAT_2:21
for C1, C2, C3 being AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C3 holds
C1 is SubCatStr of C3
proof
let C1, C2, C3 be AltCatStr ; ::_thesis: ( C1 is SubCatStr of C2 & C2 is SubCatStr of C3 implies C1 is SubCatStr of C3 )
assume ( the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 & the Comp of C1 cc= the Comp of C2 & the carrier of C2 c= the carrier of C3 & the Arrows of C2 cc= the Arrows of C3 & the Comp of C2 cc= the Comp of C3 ) ; :: according to ALTCAT_2:def_11 ::_thesis: C1 is SubCatStr of C3
hence ( the carrier of C1 c= the carrier of C3 & the Arrows of C1 cc= the Arrows of C3 & the Comp of C1 cc= the Comp of C3 ) by Th8, XBOOLE_1:1; :: according to ALTCAT_2:def_11 ::_thesis: verum
end;
theorem Th22: :: ALTCAT_2:22
for C1, C2 being AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C1 holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
proof
let C1, C2 be AltCatStr ; ::_thesis: ( C1 is SubCatStr of C2 & C2 is SubCatStr of C1 implies AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) )
assume that
A1: ( the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 ) and
A2: the Comp of C1 cc= the Comp of C2 and
A3: ( the carrier of C2 c= the carrier of C1 & the Arrows of C2 cc= the Arrows of C1 ) and
A4: the Comp of C2 cc= the Comp of C1 ; :: according to ALTCAT_2:def_11 ::_thesis: AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
( the carrier of C1 = the carrier of C2 & the Arrows of C1 = the Arrows of C2 ) by A1, A3, Th7, XBOOLE_0:def_10;
hence AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) by A2, A4, Th7; ::_thesis: verum
end;
registration
let C be AltCatStr ;
cluster strict for SubCatStr of C;
existence
ex b1 being SubCatStr of C st b1 is strict
proof
set D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #);
reconsider D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) as SubCatStr of C by Def11;
take D ; ::_thesis: D is strict
thus D is strict ; ::_thesis: verum
end;
end;
definition
let C be non empty AltCatStr ;
let o be object of C;
func ObCat o -> strict SubCatStr of C means :Def12: :: ALTCAT_2:def 12
( the carrier of it = {o} & the Arrows of it = (o,o) :-> <^o,o^> & the Comp of it = [o,o,o] .--> ( the Comp of C . (o,o,o)) );
existence
ex b1 being strict SubCatStr of C st
( the carrier of b1 = {o} & the Arrows of b1 = (o,o) :-> <^o,o^> & the Comp of b1 = [o,o,o] .--> ( the Comp of C . (o,o,o)) )
proof
set m = [o,o,o] .--> ( the Comp of C . (o,o,o));
dom ([o,o,o] .--> ( the Comp of C . (o,o,o))) = {[o,o,o]} by FUNCOP_1:13
.= [:{o},{o},{o}:] by MCART_1:35 ;
then reconsider m = [o,o,o] .--> ( the Comp of C . (o,o,o)) as ManySortedSet of [:{o},{o},{o}:] by PARTFUN1:def_2, RELAT_1:def_18;
set a = (o,o) :-> <^o,o^>;
dom ((o,o) :-> <^o,o^>) = [:{o},{o}:] by FUNCT_2:def_1;
then reconsider a = (o,o) :-> <^o,o^> as ManySortedSet of [:{o},{o}:] by PARTFUN1:def_2;
A1: a . (o,o) = the Arrows of C . (o,o) by ALTCAT_1:10;
m is ManySortedFunction of {|a,a|},{|a|}
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in [:{o},{o},{o}:] or m . i is Element of bool [:({|a,a|} . i),({|a|} . i):] )
A2: o in {o} by TARSKI:def_1;
assume i in [:{o},{o},{o}:] ; ::_thesis: m . i is Element of bool [:({|a,a|} . i),({|a|} . i):]
then i in {[o,o,o]} by MCART_1:35;
then A3: i = [o,o,o] by TARSKI:def_1;
then A4: {|a|} . i = {|a|} . (o,o,o) by MULTOP_1:def_1
.= the Arrows of C . (o,o) by A1, A2, ALTCAT_1:def_3 ;
{|a,a|} . i = {|a,a|} . (o,o,o) by A3, MULTOP_1:def_1
.= [:( the Arrows of C . (o,o)),( the Arrows of C . (o,o)):] by A1, A2, ALTCAT_1:def_4 ;
hence m . i is Element of bool [:({|a,a|} . i),({|a|} . i):] by A3, A4, FUNCOP_1:72; ::_thesis: verum
end;
then reconsider m = m as BinComp of a ;
set D = AltCatStr(# {o},a,m #);
AltCatStr(# {o},a,m #) is SubCatStr of C
proof
thus the carrier of AltCatStr(# {o},a,m #) c= the carrier of C ; :: according to ALTCAT_2:def_11 ::_thesis: ( the Arrows of AltCatStr(# {o},a,m #) cc= the Arrows of C & the Comp of AltCatStr(# {o},a,m #) cc= the Comp of C )
thus the Arrows of AltCatStr(# {o},a,m #) cc= the Arrows of C ::_thesis: the Comp of AltCatStr(# {o},a,m #) cc= the Comp of C
proof
thus [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] c= [: the carrier of C, the carrier of C:] ; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] holds
the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i
let i be set ; ::_thesis: ( i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] implies the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i )
assume i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] ; ::_thesis: the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i
then i in {[o,o]} by ZFMISC_1:29;
then i = [o,o] by TARSKI:def_1;
hence the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i by A1; ::_thesis: verum
end;
thus [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] c= [: the carrier of C, the carrier of C, the carrier of C:] ; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] holds
the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i
let i be set ; ::_thesis: ( i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] implies the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i )
assume i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] ; ::_thesis: the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i
then i in {[o,o,o]} by MCART_1:35;
then A5: i = [o,o,o] by TARSKI:def_1;
then the Comp of AltCatStr(# {o},a,m #) . i = the Comp of C . (o,o,o) by FUNCOP_1:72
.= the Comp of C . i by A5, MULTOP_1:def_1 ;
hence the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i ; ::_thesis: verum
end;
then reconsider D = AltCatStr(# {o},a,m #) as strict SubCatStr of C ;
take D ; ::_thesis: ( the carrier of D = {o} & the Arrows of D = (o,o) :-> <^o,o^> & the Comp of D = [o,o,o] .--> ( the Comp of C . (o,o,o)) )
thus ( the carrier of D = {o} & the Arrows of D = (o,o) :-> <^o,o^> & the Comp of D = [o,o,o] .--> ( the Comp of C . (o,o,o)) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict SubCatStr of C st the carrier of b1 = {o} & the Arrows of b1 = (o,o) :-> <^o,o^> & the Comp of b1 = [o,o,o] .--> ( the Comp of C . (o,o,o)) & the carrier of b2 = {o} & the Arrows of b2 = (o,o) :-> <^o,o^> & the Comp of b2 = [o,o,o] .--> ( the Comp of C . (o,o,o)) holds
b1 = b2 ;
end;
:: deftheorem Def12 defines ObCat ALTCAT_2:def_12_:_
for C being non empty AltCatStr
for o being object of C
for b3 being strict SubCatStr of C holds
( b3 = ObCat o iff ( the carrier of b3 = {o} & the Arrows of b3 = (o,o) :-> <^o,o^> & the Comp of b3 = [o,o,o] .--> ( the Comp of C . (o,o,o)) ) );
theorem Th23: :: ALTCAT_2:23
for C being non empty AltCatStr
for o being object of C
for o9 being object of (ObCat o) holds o9 = o
proof
let C be non empty AltCatStr ; ::_thesis: for o being object of C
for o9 being object of (ObCat o) holds o9 = o
let o be object of C; ::_thesis: for o9 being object of (ObCat o) holds o9 = o
let o9 be object of (ObCat o); ::_thesis: o9 = o
the carrier of (ObCat o) = {o} by Def12;
hence o9 = o by TARSKI:def_1; ::_thesis: verum
end;
registration
let C be non empty AltCatStr ;
let o be object of C;
cluster ObCat o -> non empty transitive strict ;
coherence
( ObCat o is transitive & not ObCat o is empty )
proof
thus ObCat o is transitive ::_thesis: not ObCat o is empty
proof
let o1, o2, o3 be object of (ObCat o); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume that
<^o1,o2^> <> {} and
A1: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {}
o1 = o by Th23;
hence not <^o1,o3^> = {} by A1, Th23; ::_thesis: verum
end;
the carrier of (ObCat o) = {o} by Def12;
hence not the carrier of (ObCat o) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
registration
let C be non empty AltCatStr ;
cluster non empty transitive strict for SubCatStr of C;
existence
ex b1 being SubCatStr of C st
( b1 is transitive & not b1 is empty & b1 is strict )
proof
set o = the object of C;
take ObCat the object of C ; ::_thesis: ( ObCat the object of C is transitive & not ObCat the object of C is empty & ObCat the object of C is strict )
thus ( ObCat the object of C is transitive & not ObCat the object of C is empty & ObCat the object of C is strict ) ; ::_thesis: verum
end;
end;
theorem Th24: :: ALTCAT_2:24
for C being non empty transitive AltCatStr
for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 holds
D1 is SubCatStr of D2
proof
let C be non empty transitive AltCatStr ; ::_thesis: for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 holds
D1 is SubCatStr of D2
let D1, D2 be non empty transitive SubCatStr of C; ::_thesis: ( the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 implies D1 is SubCatStr of D2 )
assume that
A1: the carrier of D1 c= the carrier of D2 and
A2: the Arrows of D1 cc= the Arrows of D2 ; ::_thesis: D1 is SubCatStr of D2
thus the carrier of D1 c= the carrier of D2 by A1; :: according to ALTCAT_2:def_11 ::_thesis: ( the Arrows of D1 cc= the Arrows of D2 & the Comp of D1 cc= the Comp of D2 )
thus the Arrows of D1 cc= the Arrows of D2 by A2; ::_thesis: the Comp of D1 cc= the Comp of D2
thus [: the carrier of D1, the carrier of D1, the carrier of D1:] c= [: the carrier of D2, the carrier of D2, the carrier of D2:] by A1, MCART_1:73; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in [: the carrier of D1, the carrier of D1, the carrier of D1:] holds
the Comp of D1 . i c= the Comp of D2 . i
let x be set ; ::_thesis: ( x in [: the carrier of D1, the carrier of D1, the carrier of D1:] implies the Comp of D1 . x c= the Comp of D2 . x )
assume A3: x in [: the carrier of D1, the carrier of D1, the carrier of D1:] ; ::_thesis: the Comp of D1 . x c= the Comp of D2 . x
then consider i1, i2, i3 being set such that
A4: ( i1 in the carrier of D1 & i2 in the carrier of D1 & i3 in the carrier of D1 ) and
A5: x = [i1,i2,i3] by MCART_1:68;
reconsider i1 = i1, i2 = i2, i3 = i3 as object of D1 by A4;
reconsider j1 = i1, j2 = i2, j3 = i3 as object of D2 by A1, A4;
[i2,i3] in [: the carrier of D1, the carrier of D1:] ;
then A6: <^i2,i3^> c= <^j2,j3^> by A2, Def2;
reconsider c2 = the Comp of D2 . (j1,j2,j3) as Function of [:<^j2,j3^>,<^j1,j2^>:],<^j1,j3^> ;
reconsider c1 = the Comp of D1 . (i1,i2,i3) as Function of [:<^i2,i3^>,<^i1,i2^>:],<^i1,i3^> ;
( not <^i1,i3^> = {} or <^i2,i3^> = {} or <^i1,i2^> = {} ) by ALTCAT_1:def_2;
then ( <^i1,i3^> = {} implies [:<^i2,i3^>,<^i1,i2^>:] = {} ) by ZFMISC_1:90;
then A7: dom c1 = [:<^i2,i3^>,<^i1,i2^>:] by FUNCT_2:def_1;
( not <^j1,j3^> = {} or <^j2,j3^> = {} or <^j1,j2^> = {} ) by ALTCAT_1:def_2;
then ( <^j1,j3^> = {} implies [:<^j2,j3^>,<^j1,j2^>:] = {} ) by ZFMISC_1:90;
then A8: dom c2 = [:<^j2,j3^>,<^j1,j2^>:] by FUNCT_2:def_1;
[i1,i2] in [: the carrier of D1, the carrier of D1:] ;
then <^i1,i2^> c= <^j1,j2^> by A2, Def2;
then A9: dom c1 c= dom c2 by A7, A6, A8, ZFMISC_1:96;
A10: now__::_thesis:_for_y_being_set_st_y_in_dom_c1_holds_
c1_._y_=_c2_._y
the carrier of D1 c= the carrier of C by Def11;
then reconsider o1 = i1, o2 = i2, o3 = i3 as object of C by A4;
reconsider c = the Comp of C . (o1,o2,o3) as Function of [:<^o2,o3^>,<^o1,o2^>:],<^o1,o3^> ;
let y be set ; ::_thesis: ( y in dom c1 implies c1 . y = c2 . y )
A11: c = the Comp of C . [o1,o2,o3] by MULTOP_1:def_1;
A12: c2 = the Comp of D2 . [o1,o2,o3] by MULTOP_1:def_1;
( [o1,o2,o3] in [: the carrier of D2, the carrier of D2, the carrier of D2:] & the Comp of D2 cc= the Comp of C ) by A1, A4, Def11, MCART_1:69;
then A13: c2 c= c by A11, A12, Def2;
assume A14: y in dom c1 ; ::_thesis: c1 . y = c2 . y
( the Comp of D1 cc= the Comp of C & c1 = the Comp of D1 . [o1,o2,o3] ) by Def11, MULTOP_1:def_1;
then c1 c= c by A3, A5, A11, Def2;
hence c1 . y = c . y by A14, GRFUNC_1:2
.= c2 . y by A9, A14, A13, GRFUNC_1:2 ;
::_thesis: verum
end;
( c1 = the Comp of D1 . x & c2 = the Comp of D2 . x ) by A5, MULTOP_1:def_1;
hence the Comp of D1 . x c= the Comp of D2 . x by A9, A10, GRFUNC_1:2; ::_thesis: verum
end;
definition
let C be AltCatStr ;
let D be SubCatStr of C;
attrD is full means :Def13: :: ALTCAT_2:def 13
the Arrows of D = the Arrows of C || the carrier of D;
end;
:: deftheorem Def13 defines full ALTCAT_2:def_13_:_
for C being AltCatStr
for D being SubCatStr of C holds
( D is full iff the Arrows of D = the Arrows of C || the carrier of D );
definition
let C be non empty with_units AltCatStr ;
let D be SubCatStr of C;
attrD is id-inheriting means :Def14: :: ALTCAT_2:def 14
for o being object of D
for o9 being object of C st o = o9 holds
idm o9 in <^o,o^> if not D is empty
otherwise verum;
consistency
verum ;
end;
:: deftheorem Def14 defines id-inheriting ALTCAT_2:def_14_:_
for C being non empty with_units AltCatStr
for D being SubCatStr of C holds
( ( not D is empty implies ( D is id-inheriting iff for o being object of D
for o9 being object of C st o = o9 holds
idm o9 in <^o,o^> ) ) & ( D is empty implies ( D is id-inheriting iff verum ) ) );
registration
let C be AltCatStr ;
cluster strict full for SubCatStr of C;
existence
ex b1 being SubCatStr of C st
( b1 is full & b1 is strict )
proof
set D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #);
reconsider D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) as SubCatStr of C by Def11;
take D ; ::_thesis: ( D is full & D is strict )
dom the Arrows of C = [: the carrier of D, the carrier of D:] by PARTFUN1:def_2;
hence the Arrows of D = the Arrows of C || the carrier of D by RELAT_1:69; :: according to ALTCAT_2:def_13 ::_thesis: D is strict
thus D is strict ; ::_thesis: verum
end;
end;
registration
let C be non empty AltCatStr ;
cluster non empty strict full for SubCatStr of C;
existence
ex b1 being SubCatStr of C st
( b1 is full & not b1 is empty & b1 is strict )
proof
set D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #);
reconsider D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) as SubCatStr of C by Def11;
take D ; ::_thesis: ( D is full & not D is empty & D is strict )
dom the Arrows of C = [: the carrier of D, the carrier of D:] by PARTFUN1:def_2;
hence the Arrows of D = the Arrows of C || the carrier of D by RELAT_1:69; :: according to ALTCAT_2:def_13 ::_thesis: ( not D is empty & D is strict )
thus not the carrier of D is empty ; :: according to STRUCT_0:def_1 ::_thesis: D is strict
thus D is strict ; ::_thesis: verum
end;
end;
registration
let C be category;
let o be object of C;
cluster ObCat o -> strict full id-inheriting ;
coherence
( ObCat o is full & ObCat o is id-inheriting )
proof
A1: the carrier of (ObCat o) = {o} by Def12;
the Arrows of (ObCat o) = (o,o) :-> <^o,o^> by Def12
.= the Arrows of C || the carrier of (ObCat o) by A1, FUNCT_7:8 ;
hence ObCat o is full by Def13; ::_thesis: ObCat o is id-inheriting
now__::_thesis:_for_o1_being_object_of_(ObCat_o)
for_o2_being_object_of_C_st_o1_=_o2_holds_
idm_o2_in_<^o1,o1^>
let o1 be object of (ObCat o); ::_thesis: for o2 being object of C st o1 = o2 holds
idm o2 in <^o1,o1^>
let o2 be object of C; ::_thesis: ( o1 = o2 implies idm o2 in <^o1,o1^> )
assume A2: o1 = o2 ; ::_thesis: idm o2 in <^o1,o1^>
A3: o1 = o by Th23;
then <^o1,o1^> = ((o,o) :-> <^o,o^>) . (o,o) by Def12
.= <^o2,o2^> by A3, A2, ALTCAT_1:10 ;
hence idm o2 in <^o1,o1^> by ALTCAT_1:19; ::_thesis: verum
end;
hence ObCat o is id-inheriting by Def14; ::_thesis: verum
end;
end;
registration
let C be category;
cluster non empty strict full id-inheriting for SubCatStr of C;
existence
ex b1 being SubCatStr of C st
( b1 is full & b1 is id-inheriting & not b1 is empty & b1 is strict )
proof
set o = the object of C;
take ObCat the object of C ; ::_thesis: ( ObCat the object of C is full & ObCat the object of C is id-inheriting & not ObCat the object of C is empty & ObCat the object of C is strict )
thus ( ObCat the object of C is full & ObCat the object of C is id-inheriting & not ObCat the object of C is empty & ObCat the object of C is strict ) ; ::_thesis: verum
end;
end;
theorem Th25: :: ALTCAT_2:25
for C being non empty transitive AltCatStr
for D being SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
proof
let C be non empty transitive AltCatStr ; ::_thesis: for D being SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
let D be SubCatStr of C; ::_thesis: ( the carrier of D = the carrier of C & the Arrows of D = the Arrows of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) )
assume that
A1: the carrier of D = the carrier of C and
A2: the Arrows of D = the Arrows of C ; ::_thesis: AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
A3: D is transitive
proof
let o1, o2, o3 be object of D; :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider p1 = o1, p2 = o2, p3 = o3 as object of C by A1;
assume A4: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: not <^o1,o3^> = {}
A5: <^o1,o3^> = <^p1,p3^> by A2;
( <^o1,o2^> = <^p1,p2^> & <^o2,o3^> = <^p2,p3^> ) by A2;
hence not <^o1,o3^> = {} by A5, A4, ALTCAT_1:def_2; ::_thesis: verum
end;
A6: C is SubCatStr of C by Th20;
not D is empty by A1;
then C is SubCatStr of D by A1, A2, A3, A6, Th24;
hence AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by Th22; ::_thesis: verum
end;
theorem Th26: :: ALTCAT_2:26
for C being non empty transitive AltCatStr
for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 holds
AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
proof
let C be non empty transitive AltCatStr ; ::_thesis: for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 holds
AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
let D1, D2 be non empty transitive SubCatStr of C; ::_thesis: ( the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 implies AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) )
assume ( the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 ) ; ::_thesis: AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
then ( D1 is SubCatStr of D2 & D2 is SubCatStr of D1 ) by Th24;
hence AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) by Th22; ::_thesis: verum
end;
theorem :: ALTCAT_2:27
for C being non empty transitive AltCatStr
for D being full SubCatStr of C st the carrier of D = the carrier of C holds
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
proof
let C be non empty transitive AltCatStr ; ::_thesis: for D being full SubCatStr of C st the carrier of D = the carrier of C holds
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
let D be full SubCatStr of C; ::_thesis: ( the carrier of D = the carrier of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) )
assume A1: the carrier of D = the carrier of C ; ::_thesis: AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
A2: dom the Arrows of C = [: the carrier of C, the carrier of C:] by PARTFUN1:def_2;
the Arrows of D = the Arrows of C || the carrier of D by Def13
.= the Arrows of C by A1, A2, RELAT_1:69 ;
hence AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by A1, Th25; ::_thesis: verum
end;
theorem Th28: :: ALTCAT_2:28
for C being non empty AltCatStr
for D being non empty full SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^o1,o2^> = <^p1,p2^>
proof
let C be non empty AltCatStr ; ::_thesis: for D being non empty full SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^o1,o2^> = <^p1,p2^>
let D be non empty full SubCatStr of C; ::_thesis: for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^o1,o2^> = <^p1,p2^>
let o1, o2 be object of C; ::_thesis: for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^o1,o2^> = <^p1,p2^>
let p1, p2 be object of D; ::_thesis: ( o1 = p1 & o2 = p2 implies <^o1,o2^> = <^p1,p2^> )
assume A1: ( o1 = p1 & o2 = p2 ) ; ::_thesis: <^o1,o2^> = <^p1,p2^>
[p1,p2] in [: the carrier of D, the carrier of D:] ;
hence <^o1,o2^> = ( the Arrows of C || the carrier of D) . (p1,p2) by A1, FUNCT_1:49
.= <^p1,p2^> by Def13 ;
::_thesis: verum
end;
theorem Th29: :: ALTCAT_2:29
for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o being object of D holds o is object of C
proof
let C be non empty AltCatStr ; ::_thesis: for D being non empty SubCatStr of C
for o being object of D holds o is object of C
let D be non empty SubCatStr of C; ::_thesis: for o being object of D holds o is object of C
let o be object of D; ::_thesis: o is object of C
( o in the carrier of D & the carrier of D c= the carrier of C ) by Def11;
hence o is object of C ; ::_thesis: verum
end;
registration
let C be non empty transitive AltCatStr ;
cluster non empty full -> transitive for SubCatStr of C;
coherence
for b1 being SubCatStr of C st b1 is full & not b1 is empty holds
b1 is transitive
proof
let D be SubCatStr of C; ::_thesis: ( D is full & not D is empty implies D is transitive )
assume A1: ( D is full & not D is empty ) ; ::_thesis: D is transitive
let o1, o2, o3 be object of D; :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume A2: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: not <^o1,o3^> = {}
reconsider p1 = o1, p2 = o2, p3 = o3 as object of C by A1, Th29;
( <^p1,p2^> <> {} & <^p2,p3^> <> {} ) by A1, A2, Th28;
then <^p1,p3^> <> {} by ALTCAT_1:def_2;
hence not <^o1,o3^> = {} by A1, Th28; ::_thesis: verum
end;
end;
theorem :: ALTCAT_2:30
for C being non empty transitive AltCatStr
for D1, D2 being non empty full SubCatStr of C st the carrier of D1 = the carrier of D2 holds
AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
proof
let C be non empty transitive AltCatStr ; ::_thesis: for D1, D2 being non empty full SubCatStr of C st the carrier of D1 = the carrier of D2 holds
AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
let D1, D2 be non empty full SubCatStr of C; ::_thesis: ( the carrier of D1 = the carrier of D2 implies AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) )
assume A1: the carrier of D1 = the carrier of D2 ; ::_thesis: AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
then the Arrows of D1 = the Arrows of C || the carrier of D2 by Def13
.= the Arrows of D2 by Def13 ;
hence AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) by A1, Th26; ::_thesis: verum
end;
theorem Th31: :: ALTCAT_2:31
for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>
proof
let C be non empty AltCatStr ; ::_thesis: for D being non empty SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>
let D be non empty SubCatStr of C; ::_thesis: for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>
let o1, o2 be object of C; ::_thesis: for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>
let p1, p2 be object of D; ::_thesis: ( o1 = p1 & o2 = p2 implies <^p1,p2^> c= <^o1,o2^> )
assume A1: ( o1 = p1 & o2 = p2 ) ; ::_thesis: <^p1,p2^> c= <^o1,o2^>
( [p1,p2] in [: the carrier of D, the carrier of D:] & the Arrows of D cc= the Arrows of C ) by Def11;
hence <^p1,p2^> c= <^o1,o2^> by A1, Def2; ::_thesis: verum
end;
theorem Th32: :: ALTCAT_2:32
for C being non empty transitive AltCatStr
for D being non empty transitive SubCatStr of C
for p1, p2, p3 being object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds
for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
proof
let C be non empty transitive AltCatStr ; ::_thesis: for D being non empty transitive SubCatStr of C
for p1, p2, p3 being object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds
for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let D be non empty transitive SubCatStr of C; ::_thesis: for p1, p2, p3 being object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds
for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let p1, p2, p3 be object of D; ::_thesis: ( <^p1,p2^> <> {} & <^p2,p3^> <> {} implies for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff )
assume A1: ( <^p1,p2^> <> {} & <^p2,p3^> <> {} ) ; ::_thesis: for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let o1, o2, o3 be object of C; ::_thesis: ( o1 = p1 & o2 = p2 & o3 = p3 implies for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff )
assume A2: ( o1 = p1 & o2 = p2 & o3 = p3 ) ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let g be Morphism of o2,o3; ::_thesis: for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let ff be Morphism of p1,p2; ::_thesis: for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let gg be Morphism of p2,p3; ::_thesis: ( f = ff & g = gg implies g * f = gg * ff )
assume A3: ( f = ff & g = gg ) ; ::_thesis: g * f = gg * ff
<^p1,p3^> <> {} by A1, ALTCAT_1:def_2;
then dom ( the Comp of D . (p1,p2,p3)) = [:<^p2,p3^>,<^p1,p2^>:] by FUNCT_2:def_1;
then A4: [gg,ff] in dom ( the Comp of D . (p1,p2,p3)) by A1, ZFMISC_1:87;
A5: the Comp of D cc= the Comp of C by Def11;
( the Comp of D . (p1,p2,p3) = the Comp of D . [p1,p2,p3] & the Comp of C . (o1,o2,o3) = the Comp of C . [o1,o2,o3] ) by MULTOP_1:def_1;
then A6: the Comp of D . (p1,p2,p3) c= the Comp of C . (o1,o2,o3) by A2, A5, Def2;
( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) by A1, A2, Th31, XBOOLE_1:3;
hence g * f = ( the Comp of C . (o1,o2,o3)) . (g,f) by ALTCAT_1:def_8
.= ( the Comp of D . (p1,p2,p3)) . (gg,ff) by A3, A4, A6, GRFUNC_1:2
.= gg * ff by A1, ALTCAT_1:def_8 ;
::_thesis: verum
end;
registration
let C be non empty transitive associative AltCatStr ;
cluster non empty transitive -> non empty associative for SubCatStr of C;
coherence
for b1 being non empty SubCatStr of C st b1 is transitive holds
b1 is associative
proof
let D be non empty SubCatStr of C; ::_thesis: ( D is transitive implies D is associative )
assume D is transitive ; ::_thesis: D is associative
then reconsider D = D as non empty transitive SubCatStr of C ;
D is associative
proof
let o1, o2, o3, o4 be object of D; :: according to ALTCAT_2:def_8 ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f)
A1: ( o1 in the carrier of D & o2 in the carrier of D ) ;
A2: ( o3 in the carrier of D & o4 in the carrier of D ) ;
the carrier of D c= the carrier of C by Def11;
then reconsider p1 = o1, p2 = o2, p3 = o3, p4 = o4 as object of C by A1, A2;
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f)
let g be Morphism of o2,o3; ::_thesis: for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f)
let h be Morphism of o3,o4; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} implies (h * g) * f = h * (g * f) )
assume that
A3: <^o1,o2^> <> {} and
A4: <^o2,o3^> <> {} and
A5: <^o3,o4^> <> {} ; ::_thesis: (h * g) * f = h * (g * f)
A6: <^o2,o3^> c= <^p2,p3^> by Th31;
g in <^o2,o3^> by A4;
then reconsider gg = g as Morphism of p2,p3 by A6;
A7: <^o1,o2^> c= <^p1,p2^> by Th31;
f in <^o1,o2^> by A3;
then reconsider ff = f as Morphism of p1,p2 by A7;
A8: ( <^o1,o3^> <> {} & g * f = gg * ff ) by A3, A4, Th32, ALTCAT_1:def_2;
A9: <^o3,o4^> c= <^p3,p4^> by Th31;
h in <^o3,o4^> by A5;
then reconsider hh = h as Morphism of p3,p4 by A9;
A10: <^p3,p4^> <> {} by A5, Th31, XBOOLE_1:3;
A11: ( <^p1,p2^> <> {} & <^p2,p3^> <> {} ) by A3, A4, Th31, XBOOLE_1:3;
( <^o2,o4^> <> {} & h * g = hh * gg ) by A4, A5, Th32, ALTCAT_1:def_2;
hence (h * g) * f = (hh * gg) * ff by A3, Th32
.= hh * (gg * ff) by A11, A10, Def8
.= h * (g * f) by A5, A8, Th32 ;
::_thesis: verum
end;
hence D is associative ; ::_thesis: verum
end;
end;
theorem Th33: :: ALTCAT_2:33
for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds
for n being Morphism of p1,p2 holds n is Morphism of o1,o2
proof
let C be non empty AltCatStr ; ::_thesis: for D being non empty SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds
for n being Morphism of p1,p2 holds n is Morphism of o1,o2
let D be non empty SubCatStr of C; ::_thesis: for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds
for n being Morphism of p1,p2 holds n is Morphism of o1,o2
let o1, o2 be object of C; ::_thesis: for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds
for n being Morphism of p1,p2 holds n is Morphism of o1,o2
let p1, p2 be object of D; ::_thesis: ( o1 = p1 & o2 = p2 & <^p1,p2^> <> {} implies for n being Morphism of p1,p2 holds n is Morphism of o1,o2 )
assume A1: ( o1 = p1 & o2 = p2 & <^p1,p2^> <> {} ) ; ::_thesis: for n being Morphism of p1,p2 holds n is Morphism of o1,o2
let n be Morphism of p1,p2; ::_thesis: n is Morphism of o1,o2
( n in <^p1,p2^> & <^p1,p2^> c= <^o1,o2^> ) by A1, Th31;
hence n is Morphism of o1,o2 ; ::_thesis: verum
end;
registration
let C be non empty transitive with_units AltCatStr ;
cluster non empty transitive id-inheriting -> non empty with_units for SubCatStr of C;
coherence
for b1 being non empty SubCatStr of C st b1 is id-inheriting & b1 is transitive holds
b1 is with_units
proof
let D be non empty SubCatStr of C; ::_thesis: ( D is id-inheriting & D is transitive implies D is with_units )
assume that
A1: D is id-inheriting and
A2: D is transitive ; ::_thesis: D is with_units
let o be object of D; :: according to ALTCAT_2:def_9 ::_thesis: ( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being object of D
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) )
reconsider p = o as object of C by Th29;
reconsider i = idm p as Morphism of o,o by A1, Def14;
A3: idm p in <^o,o^> by A1, Def14;
hence <^o,o^> <> {} ; ::_thesis: ex i being Morphism of o,o st
for o9 being object of D
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
take i ; ::_thesis: for o9 being object of D
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
let o9 be object of D; ::_thesis: for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
let m9 be Morphism of o9,o; ::_thesis: for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
let m99 be Morphism of o,o9; ::_thesis: ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
hereby ::_thesis: ( <^o,o9^> <> {} implies m99 * i = m99 )
reconsider p9 = o9 as object of C by Th29;
assume A4: <^o9,o^> <> {} ; ::_thesis: i * m9 = m9
then A5: <^p9,p^> <> {} by Th31, XBOOLE_1:3;
reconsider n9 = m9 as Morphism of p9,p by A4, Th33;
thus i * m9 = (idm p) * n9 by A2, A3, A4, Th32
.= m9 by A5, ALTCAT_1:20 ; ::_thesis: verum
end;
reconsider p9 = o9 as object of C by Th29;
assume A6: <^o,o9^> <> {} ; ::_thesis: m99 * i = m99
then A7: <^p,p9^> <> {} by Th31, XBOOLE_1:3;
reconsider n99 = m99 as Morphism of p,p9 by A6, Th33;
thus m99 * i = n99 * (idm p) by A2, A3, A6, Th32
.= m99 by A7, ALTCAT_1:def_17 ; ::_thesis: verum
end;
end;
registration
let C be category;
cluster non empty transitive id-inheriting for SubCatStr of C;
existence
ex b1 being non empty SubCatStr of C st
( b1 is id-inheriting & b1 is transitive )
proof
set o = the object of C;
take ObCat the object of C ; ::_thesis: ( ObCat the object of C is id-inheriting & ObCat the object of C is transitive )
thus ( ObCat the object of C is id-inheriting & ObCat the object of C is transitive ) ; ::_thesis: verum
end;
end;
definition
let C be category;
mode subcategory of C is transitive id-inheriting SubCatStr of C;
end;
theorem :: ALTCAT_2:34
for C being category
for D being non empty subcategory of C
for o being object of D
for o9 being object of C st o = o9 holds
idm o = idm o9
proof
let C be category; ::_thesis: for D being non empty subcategory of C
for o being object of D
for o9 being object of C st o = o9 holds
idm o = idm o9
let D be non empty subcategory of C; ::_thesis: for o being object of D
for o9 being object of C st o = o9 holds
idm o = idm o9
let o be object of D; ::_thesis: for o9 being object of C st o = o9 holds
idm o = idm o9
let o9 be object of C; ::_thesis: ( o = o9 implies idm o = idm o9 )
assume A1: o = o9 ; ::_thesis: idm o = idm o9
then reconsider m = idm o9 as Morphism of o,o by Def14;
A2: idm o9 in <^o,o^> by A1, Def14;
now__::_thesis:_for_p_being_object_of_D_st_<^o,p^>_<>_{}_holds_
for_a_being_Morphism_of_o,p_holds_a_*_m_=_a
let p be object of D; ::_thesis: ( <^o,p^> <> {} implies for a being Morphism of o,p holds a * m = a )
assume A3: <^o,p^> <> {} ; ::_thesis: for a being Morphism of o,p holds a * m = a
reconsider p9 = p as object of C by Th29;
A4: <^o9,p9^> <> {} by A1, A3, Th31, XBOOLE_1:3;
let a be Morphism of o,p; ::_thesis: a * m = a
reconsider n = a as Morphism of o9,p9 by A1, A3, Th33;
thus a * m = n * (idm o9) by A1, A2, A3, Th32
.= a by A4, ALTCAT_1:def_17 ; ::_thesis: verum
end;
hence idm o = idm o9 by ALTCAT_1:def_17; ::_thesis: verum
end;