set X = NAT ;
set comp = { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } ;
A1: for x, y1, y2 being object st [x,y1] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } & [x,y2] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } & [x,y2] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } implies y1 = y2 )
assume [x,y1] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } ; :: thesis: ( not [x,y2] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } or y1 = y2 )
then consider n11, n12, n13 being Element of NAT such that
A2: ( [x,y1] = [[n11,n12],n13] & ( n11 <> n12 implies n13 = n11 + n12 ) & ( n11 = n12 implies n13 = 0 ) ) ;
assume [x,y2] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } ; :: thesis: y1 = y2
then consider n21, n22, n23 being Element of NAT such that
A3: ( [x,y2] = [[n21,n22],n23] & ( n21 <> n22 implies n23 = n21 + n22 ) & ( n21 = n22 implies n23 = 0 ) ) ;
A4: ( x = [n11,n12] & y1 = n13 ) by A2, XTUPLE_0:1;
( x = [n21,n22] & y2 = n23 ) by A3, XTUPLE_0:1;
then A5: ( n11 = n21 & n12 = n22 ) by A4, XTUPLE_0:1;
per cases ( n11 <> n12 or n11 = n12 ) ;
suppose n11 <> n12 ; :: thesis: y1 = y2
thus y1 = y2 by A2, A3, A5, XTUPLE_0:1; :: thesis: verum
end;
suppose n11 = n12 ; :: thesis: y1 = y2
thus y1 = y2 by A2, A3, A5, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
for x being object st x in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } holds
x in [:[:NAT,NAT:],NAT:]
proof
let x be object ; :: thesis: ( x in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } implies x in [:[:NAT,NAT:],NAT:] )
assume x in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } ; :: thesis: x in [:[:NAT,NAT:],NAT:]
then consider n11, n12, n13 being Element of NAT such that
A6: ( x = [[n11,n12],n13] & ( n11 <> n12 implies n13 = n11 + n12 ) & ( n11 = n12 implies n13 = 0 ) ) ;
[n11,n12] in [:NAT,NAT:] by ZFMISC_1:def 2;
hence x in [:[:NAT,NAT:],NAT:] by A6, ZFMISC_1:def 2; :: thesis: verum
end;
then reconsider comp = { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } as PartFunc of [:NAT,NAT:],NAT by A1, TARSKI:def 3, FUNCT_1:def 1;
set C = CategoryStr(# NAT,comp #);
A7: for f1, f2 being morphism of CategoryStr(# NAT,comp #) holds f1 |> f2
proof
let f1, f2 be morphism of CategoryStr(# NAT,comp #); :: thesis: f1 |> f2
reconsider n1 = f1, n2 = f2 as Element of NAT ;
per cases ( n1 <> n2 or n1 = n2 ) ;
suppose A8: n1 <> n2 ; :: thesis: f1 |> f2
reconsider n3 = n1 + n2 as Element of NAT ;
[[n1,n2],n3] in the composition of CategoryStr(# NAT,comp #) by A8;
hence f1 |> f2 by FUNCT_1:1; :: thesis: verum
end;
suppose A9: n1 = n2 ; :: thesis: f1 |> f2
set n3 = 0 ;
[[n1,n2],0] in the composition of CategoryStr(# NAT,comp #) by A9;
hence f1 |> f2 by FUNCT_1:1; :: thesis: verum
end;
end;
end;
A10: for f1, f2 being morphism of CategoryStr(# NAT,comp #) st f1 = 0 holds
( f1 (*) f2 = f2 & f2 (*) f1 = f2 )
proof
let f1, f2 be morphism of CategoryStr(# NAT,comp #); :: thesis: ( f1 = 0 implies ( f1 (*) f2 = f2 & f2 (*) f1 = f2 ) )
assume A11: f1 = 0 ; :: thesis: ( f1 (*) f2 = f2 & f2 (*) f1 = f2 )
reconsider n2 = f2 as Element of NAT ;
[f1,f2] in dom the composition of CategoryStr(# NAT,comp #) by A7, Def2;
then consider y being object such that
A12: [[f1,f2],y] in the composition of CategoryStr(# NAT,comp #) by XTUPLE_0:def 12;
consider n1, n2, n3 being Element of NAT such that
A13: ( [[f1,f2],y] = [[n1,n2],n3] & ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) by A12;
( [f1,f2] = [n1,n2] & y = n3 ) by A13, XTUPLE_0:1;
then A14: ( f1 = n1 & f2 = n2 ) by XTUPLE_0:1;
thus f1 (*) f2 = the composition of CategoryStr(# NAT,comp #) . (f1,f2) by Def3, A7
.= the composition of CategoryStr(# NAT,comp #) . [f1,f2] by BINOP_1:def 1
.= f2 by FUNCT_1:1, A12, A13, A14, A11 ; :: thesis: f2 (*) f1 = f2
[f2,f1] in dom the composition of CategoryStr(# NAT,comp #) by A7, Def2;
then consider y being object such that
A15: [[f2,f1],y] in the composition of CategoryStr(# NAT,comp #) by XTUPLE_0:def 12;
consider n2, n1, n3 being Element of NAT such that
A16: ( [[f2,f1],y] = [[n2,n1],n3] & ( n2 <> n1 implies n3 = n2 + n1 ) & ( n2 = n1 implies n3 = 0 ) ) by A15;
( [f2,f1] = [n2,n1] & y = n3 ) by A16, XTUPLE_0:1;
then A17: ( f2 = n2 & f1 = n1 ) by XTUPLE_0:1;
thus f2 (*) f1 = the composition of CategoryStr(# NAT,comp #) . (f2,f1) by Def3, A7
.= the composition of CategoryStr(# NAT,comp #) . [f2,f1] by BINOP_1:def 1
.= f2 by FUNCT_1:1, A15, A16, A17, A11 ; :: thesis: verum
end;
A18: CategoryStr(# NAT,comp #) is left_composable by A7;
for f, f1, f2 being morphism of CategoryStr(# NAT,comp #) st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 ) by A7;
then A19: CategoryStr(# NAT,comp #) is composable by A18, Def9;
for f1 being morphism of CategoryStr(# NAT,comp #) st f1 in the carrier of CategoryStr(# NAT,comp #) holds
ex f being morphism of CategoryStr(# NAT,comp #) st
( f |> f1 & f is left_identity )
proof
let f1 be morphism of CategoryStr(# NAT,comp #); :: thesis: ( f1 in the carrier of CategoryStr(# NAT,comp #) implies ex f being morphism of CategoryStr(# NAT,comp #) st
( f |> f1 & f is left_identity ) )
assume f1 in the carrier of CategoryStr(# NAT,comp #) ; :: thesis: ex f being morphism of CategoryStr(# NAT,comp #) st
( f |> f1 & f is left_identity )
reconsider f = 0 as morphism of CategoryStr(# NAT,comp #) ;
take f ; :: thesis: ( f |> f1 & f is left_identity )
thus f |> f1 by A7; :: thesis: f is left_identity
thus f is left_identity by A10; :: thesis: verum
end;
then A20: CategoryStr(# NAT,comp #) is with_left_identities ;
for f1 being morphism of CategoryStr(# NAT,comp #) st f1 in the carrier of CategoryStr(# NAT,comp #) holds
ex f being morphism of CategoryStr(# NAT,comp #) st
( f1 |> f & f is right_identity )
proof
let f1 be morphism of CategoryStr(# NAT,comp #); :: thesis: ( f1 in the carrier of CategoryStr(# NAT,comp #) implies ex f being morphism of CategoryStr(# NAT,comp #) st
( f1 |> f & f is right_identity ) )
assume f1 in the carrier of CategoryStr(# NAT,comp #) ; :: thesis: ex f being morphism of CategoryStr(# NAT,comp #) st
( f1 |> f & f is right_identity )
reconsider f = 0 as morphism of CategoryStr(# NAT,comp #) ;
take f ; :: thesis: ( f1 |> f & f is right_identity )
thus f1 |> f by A7; :: thesis: f is right_identity
thus f is right_identity by A10; :: thesis: verum
end;
then A21: CategoryStr(# NAT,comp #) is with_identities by A20, Def7;
A22: for f1, f2 being morphism of CategoryStr(# NAT,comp #)
for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n1 = n2 holds
f1 (*) f2 = 0
proof
let f1, f2 be morphism of CategoryStr(# NAT,comp #); :: thesis: for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n1 = n2 holds
f1 (*) f2 = 0
let n1, n2 be Element of NAT ; :: thesis: ( f1 = n1 & f2 = n2 & n1 = n2 implies f1 (*) f2 = 0 )
assume A23: ( f1 = n1 & f2 = n2 ) ; :: thesis: ( not n1 = n2 or f1 (*) f2 = 0 )
assume A24: n1 = n2 ; :: thesis: f1 (*) f2 = 0
[f1,f2] in dom the composition of CategoryStr(# NAT,comp #) by A7, Def2;
then consider y being object such that
A25: [[f1,f2],y] in the composition of CategoryStr(# NAT,comp #) by XTUPLE_0:def 12;
consider n11, n22, n33 being Element of NAT such that
A26: ( [[f1,f2],y] = [[n11,n22],n33] & ( n11 <> n22 implies n33 = n11 + n22 ) & ( n11 = n22 implies n33 = 0 ) ) by A25;
( [f1,f2] = [n11,n22] & y = n33 ) by A26, XTUPLE_0:1;
then A27: ( f1 = n11 & f2 = n22 ) by XTUPLE_0:1;
thus f1 (*) f2 = the composition of CategoryStr(# NAT,comp #) . (f1,f2) by Def3, A7
.= the composition of CategoryStr(# NAT,comp #) . [f1,f2] by BINOP_1:def 1
.= 0 by A27, FUNCT_1:1, A25, A26, A24, A23 ; :: thesis: verum
end;
A28: for f1, f2 being morphism of CategoryStr(# NAT,comp #)
for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n1 <> n2 holds
f1 (*) f2 = n1 + n2
proof
let f1, f2 be morphism of CategoryStr(# NAT,comp #); :: thesis: for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n1 <> n2 holds
f1 (*) f2 = n1 + n2
let n1, n2 be Element of NAT ; :: thesis: ( f1 = n1 & f2 = n2 & n1 <> n2 implies f1 (*) f2 = n1 + n2 )
assume A29: ( f1 = n1 & f2 = n2 ) ; :: thesis: ( not n1 <> n2 or f1 (*) f2 = n1 + n2 )
assume A30: n1 <> n2 ; :: thesis: f1 (*) f2 = n1 + n2
[f1,f2] in dom the composition of CategoryStr(# NAT,comp #) by A7, Def2;
then consider y being object such that
A31: [[f1,f2],y] in the composition of CategoryStr(# NAT,comp #) by XTUPLE_0:def 12;
consider n11, n22, n33 being Element of NAT such that
A32: ( [[f1,f2],y] = [[n11,n22],n33] & ( n11 <> n22 implies n33 = n11 + n22 ) & ( n11 = n22 implies n33 = 0 ) ) by A31;
( [f1,f2] = [n11,n22] & y = n33 ) by A32, XTUPLE_0:1;
then A33: ( f1 = n11 & f2 = n22 ) by XTUPLE_0:1;
thus f1 (*) f2 = the composition of CategoryStr(# NAT,comp #) . (f1,f2) by Def3, A7
.= the composition of CategoryStr(# NAT,comp #) . [f1,f2] by BINOP_1:def 1
.= n1 + n2 by A33, FUNCT_1:1, A31, A32, A30, A29 ; :: thesis: verum
end;
ex f1, f2, f3 being morphism of CategoryStr(# NAT,comp #) st
( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 & not f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
proof
reconsider f1 = 1, f2 = 2, f3 = 3 as morphism of CategoryStr(# NAT,comp #) ;
take f1 ; :: thesis: ex f2, f3 being morphism of CategoryStr(# NAT,comp #) st
( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 & not f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
take f2 ; :: thesis: ex f3 being morphism of CategoryStr(# NAT,comp #) st
( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 & not f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
take f3 ; :: thesis: ( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 & not f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
thus ( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 ) by A7; :: thesis: not f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
A34: ( f1 (*) f2 = 1 + 2 & f2 (*) f3 = 2 + 3 ) by A28;
reconsider f12 = 3, f23 = 5 as morphism of CategoryStr(# NAT,comp #) ;
( f1 (*) f23 = 1 + 5 & f12 (*) f3 = 0 ) by A22, A28;
hence not f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 by A34; :: thesis: verum
end;
hence ex b1 being CategoryStr st
( not b1 is associative & b1 is composable & b1 is with_identities ) by A19, A21, Def10; :: thesis: verum