set C = the non empty category;
reconsider X = {0,1} as set ;
set comp = {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]};
A1: for x being object holds
( x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} iff ( x = [[0,0],0] or x = [[1,1],1] or x = [[0,1],1] or x = [[1,0],1] ) )
proof
let x be object ; :: thesis: ( x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} iff ( x = [[0,0],0] or x = [[1,1],1] or x = [[0,1],1] or x = [[1,0],1] ) )
thus ( not x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} or x = [[0,0],0] or x = [[1,1],1] or x = [[0,1],1] or x = [[1,0],1] ) :: thesis: ( ( x = [[0,0],0] or x = [[1,1],1] or x = [[0,1],1] or x = [[1,0],1] ) implies x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} )
proof
assume x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} ; :: thesis: ( x = [[0,0],0] or x = [[1,1],1] or x = [[0,1],1] or x = [[1,0],1] )
then ( x in {[[0,0],0],[[1,1],1]} or x in {[[0,1],1],[[1,0],1]} ) by XBOOLE_0:def 3;
hence ( x = [[0,0],0] or x = [[1,1],1] or x = [[0,1],1] or x = [[1,0],1] ) by TARSKI:def 2; :: thesis: verum
end;
assume ( x = [[0,0],0] or x = [[1,1],1] or x = [[0,1],1] or x = [[1,0],1] ) ; :: thesis: x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]}
then ( x in {[[0,0],0],[[1,1],1]} or x in {[[0,1],1],[[1,0],1]} ) by TARSKI:def 2;
hence x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} by XBOOLE_0:def 3; :: thesis: verum
end;
A2: for x, y1, y2 being object st [x,y1] in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} & [x,y2] in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( [x,y1] in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} & [x,y2] in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} implies y1 = y2 )
assume A3: [x,y1] in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} ; :: thesis: ( not [x,y2] in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} or y1 = y2 )
assume A4: [x,y2] in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} ; :: thesis: y1 = y2
per cases ( [x,y1] = [[0,0],0] or [x,y1] = [[1,1],1] or [x,y1] = [[0,1],1] or [x,y1] = [[1,0],1] ) by A3, A1;
suppose A5: [x,y1] = [[0,0],0] ; :: thesis: y1 = y2
then A6: ( x = [0,0] & y1 = 0 ) by XTUPLE_0:1;
per cases ( [x,y2] = [[0,0],0] or [x,y2] = [[1,1],1] or [x,y2] = [[0,1],1] or [x,y2] = [[1,0],1] ) by A4, A1;
suppose [x,y2] = [[0,0],0] ; :: thesis: y1 = y2
hence y1 = y2 by A5, XTUPLE_0:1; :: thesis: verum
end;
suppose [x,y2] = [[1,1],1] ; :: thesis: y1 = y2
then ( x = [1,1] & y2 = 1 ) by XTUPLE_0:1;
hence y1 = y2 by A6, XTUPLE_0:1; :: thesis: verum
end;
suppose [x,y2] = [[0,1],1] ; :: thesis: y1 = y2
then ( x = [0,1] & y2 = 1 ) by XTUPLE_0:1;
hence y1 = y2 by A6, XTUPLE_0:1; :: thesis: verum
end;
suppose [x,y2] = [[1,0],1] ; :: thesis: y1 = y2
then ( x = [1,0] & y2 = 1 ) by XTUPLE_0:1;
hence y1 = y2 by A6, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose [x,y1] = [[1,1],1] ; :: thesis: y1 = y2
then A7: ( x = [1,1] & y1 = 1 ) by XTUPLE_0:1;
per cases ( [x,y2] = [[0,0],0] or [x,y2] = [[1,1],1] or [x,y2] = [[0,1],1] or [x,y2] = [[1,0],1] ) by A4, A1;
suppose [x,y2] = [[0,0],0] ; :: thesis: y1 = y2
then ( x = [0,0] & y2 = 0 ) by XTUPLE_0:1;
hence y1 = y2 by A7, XTUPLE_0:1; :: thesis: verum
end;
suppose ( [x,y2] = [[1,1],1] or [x,y2] = [[0,1],1] or [x,y2] = [[1,0],1] ) ; :: thesis: y1 = y2
hence y1 = y2 by A7, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose [x,y1] = [[0,1],1] ; :: thesis: y1 = y2
then A8: ( x = [0,1] & y1 = 1 ) by XTUPLE_0:1;
per cases ( [x,y2] = [[0,0],0] or [x,y2] = [[1,1],1] or [x,y2] = [[0,1],1] or [x,y2] = [[1,0],1] ) by A4, A1;
suppose [x,y2] = [[0,0],0] ; :: thesis: y1 = y2
then ( x = [0,0] & y2 = 0 ) by XTUPLE_0:1;
hence y1 = y2 by A8, XTUPLE_0:1; :: thesis: verum
end;
suppose ( [x,y2] = [[1,1],1] or [x,y2] = [[0,1],1] or [x,y2] = [[1,0],1] ) ; :: thesis: y1 = y2
hence y1 = y2 by A8, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose [x,y1] = [[1,0],1] ; :: thesis: y1 = y2
then A9: ( x = [1,0] & y1 = 1 ) by XTUPLE_0:1;
per cases ( [x,y2] = [[0,0],0] or [x,y2] = [[1,1],1] or [x,y2] = [[0,1],1] or [x,y2] = [[1,0],1] ) by A4, A1;
suppose [x,y2] = [[0,0],0] ; :: thesis: y1 = y2
then ( x = [0,0] & y2 = 0 ) by XTUPLE_0:1;
hence y1 = y2 by A9, XTUPLE_0:1; :: thesis: verum
end;
suppose ( [x,y2] = [[1,1],1] or [x,y2] = [[0,1],1] or [x,y2] = [[1,0],1] ) ; :: thesis: y1 = y2
hence y1 = y2 by A9, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
end;
end;
for x being object st x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} holds
x in [:[:X,X:],X:]
proof
let x be object ; :: thesis: ( x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} implies x in [:[:X,X:],X:] )
assume A10: x in {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} ; :: thesis: x in [:[:X,X:],X:]
per cases ( x = [[0,0],0] or x = [[1,1],1] or x = [[0,1],1] or x = [[1,0],1] ) by A10, A1;
end;
end;
then reconsider comp = {[[0,0],0],[[1,1],1]} \/ {[[0,1],1],[[1,0],1]} as PartFunc of [:X,X:],X by A2, TARSKI:def 3, FUNCT_1:def 1;
set D = CategoryStr(# X,comp #);
A19: for f1, f2 being morphism of CategoryStr(# X,comp #) holds
( not f1 |> f2 or ( f1 = 0 & f2 = 0 & f1 (*) f2 = 0 ) or ( f1 = 1 & f2 = 1 & f1 (*) f2 = 1 ) or ( f1 = 0 & f2 = 1 & f1 (*) f2 = 1 ) or ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 ) )
proof
let f1, f2 be morphism of CategoryStr(# X,comp #); :: thesis: ( not f1 |> f2 or ( f1 = 0 & f2 = 0 & f1 (*) f2 = 0 ) or ( f1 = 1 & f2 = 1 & f1 (*) f2 = 1 ) or ( f1 = 0 & f2 = 1 & f1 (*) f2 = 1 ) or ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 ) )
assume A20: f1 |> f2 ; :: thesis: ( ( f1 = 0 & f2 = 0 & f1 (*) f2 = 0 ) or ( f1 = 1 & f2 = 1 & f1 (*) f2 = 1 ) or ( f1 = 0 & f2 = 1 & f1 (*) f2 = 1 ) or ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 ) )
assume A21: ( ( not f1 = 0 or not f2 = 0 or not f1 (*) f2 = 0 ) & ( not f1 = 1 or not f2 = 1 or not f1 (*) f2 = 1 ) & ( not f1 = 0 or not f2 = 1 or not f1 (*) f2 = 1 ) ) ; :: thesis: ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 )
consider y being object such that
A22: [[f1,f2],y] in the composition of CategoryStr(# X,comp #) by A20, XTUPLE_0:def 12;
A23: f1 (*) f2 = the composition of CategoryStr(# X,comp #) . (f1,f2) by Def3, A20
.= the composition of CategoryStr(# X,comp #) . [f1,f2] by BINOP_1:def 1
.= y by A22, FUNCT_1:1 ;
per cases ( [[f1,f2],y] = [[0,0],0] or [[f1,f2],y] = [[1,1],1] or [[f1,f2],y] = [[0,1],1] or [[f1,f2],y] = [[1,0],1] ) by A22, A1;
suppose [[f1,f2],y] = [[0,0],0] ; :: thesis: ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 )
then ( [f1,f2] = [0,0] & y = 0 ) by XTUPLE_0:1;
hence ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 ) by A23, A21, XTUPLE_0:1; :: thesis: verum
end;
suppose [[f1,f2],y] = [[1,1],1] ; :: thesis: ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 )
then ( [f1,f2] = [1,1] & y = 1 ) by XTUPLE_0:1;
hence ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 ) by A21, A23, XTUPLE_0:1; :: thesis: verum
end;
suppose [[f1,f2],y] = [[0,1],1] ; :: thesis: ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 )
then ( [f1,f2] = [0,1] & y = 1 ) by XTUPLE_0:1;
hence ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 ) by A21, A23, XTUPLE_0:1; :: thesis: verum
end;
suppose [[f1,f2],y] = [[1,0],1] ; :: thesis: ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 )
then ( [f1,f2] = [1,0] & y = 1 ) by XTUPLE_0:1;
hence ( f1 = 1 & f2 = 0 & f1 (*) f2 = 1 ) by A23, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
A24: for f1, f2 being morphism of CategoryStr(# X,comp #) holds f1 |> f2
proof
let f1, f2 be morphism of CategoryStr(# X,comp #); :: thesis: f1 |> f2
per cases ( ( f1 = 0 & f2 = 0 ) or ( f1 = 1 & f2 = 1 ) or ( f1 = 0 & f2 = 1 ) or ( f1 = 1 & f2 = 0 ) ) by TARSKI:def 2;
suppose ( ( f1 = 0 & f2 = 0 ) or ( f1 = 1 & f2 = 1 ) or ( f1 = 0 & f2 = 1 ) ) ; :: thesis: f1 |> f2
then [[f1,f2],f2] in the composition of CategoryStr(# X,comp #) by A1;
hence f1 |> f2 by FUNCT_1:1; :: thesis: verum
end;
suppose ( f1 = 1 & f2 = 0 ) ; :: thesis: f1 |> f2
then [[f1,f2],f1] in the composition of CategoryStr(# X,comp #) by A1;
hence f1 |> f2 by FUNCT_1:1; :: thesis: verum
end;
end;
end;
A25: CategoryStr(# X,comp #) is left_composable by A24;
A26: for f, f1, f2 being morphism of CategoryStr(# X,comp #) st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 ) by A24;
A27: for f1 being morphism of CategoryStr(# X,comp #) st f1 in the carrier of CategoryStr(# X,comp #) holds
ex f being morphism of CategoryStr(# X,comp #) st
( f |> f1 & f is left_identity )
proof
let f1 be morphism of CategoryStr(# X,comp #); :: thesis: ( f1 in the carrier of CategoryStr(# X,comp #) implies ex f being morphism of CategoryStr(# X,comp #) st
( f |> f1 & f is left_identity ) )
assume f1 in the carrier of CategoryStr(# X,comp #) ; :: thesis: ex f being morphism of CategoryStr(# X,comp #) st
( f |> f1 & f is left_identity )
reconsider f = 0 as morphism of CategoryStr(# X,comp #) by TARSKI:def 2;
take f ; :: thesis: ( f |> f1 & f is left_identity )
thus f |> f1 by A24; :: thesis: f is left_identity
for f2 being morphism of CategoryStr(# X,comp #) st f |> f2 holds
f (*) f2 = f2
proof
let f2 be morphism of CategoryStr(# X,comp #); :: thesis: ( f |> f2 implies f (*) f2 = f2 )
assume A28: f |> f2 ; :: thesis: f (*) f2 = f2
( f2 = 0 or f2 = 1 ) by TARSKI:def 2;
hence f (*) f2 = f2 by A28, A19; :: thesis: verum
end;
hence f is left_identity ; :: thesis: verum
end;
for f1 being morphism of CategoryStr(# X,comp #) st f1 in the carrier of CategoryStr(# X,comp #) holds
ex f being morphism of CategoryStr(# X,comp #) st
( f1 |> f & f is right_identity )
proof
let f1 be morphism of CategoryStr(# X,comp #); :: thesis: ( f1 in the carrier of CategoryStr(# X,comp #) implies ex f being morphism of CategoryStr(# X,comp #) st
( f1 |> f & f is right_identity ) )
assume f1 in the carrier of CategoryStr(# X,comp #) ; :: thesis: ex f being morphism of CategoryStr(# X,comp #) st
( f1 |> f & f is right_identity )
reconsider f = 0 as morphism of CategoryStr(# X,comp #) by TARSKI:def 2;
take f ; :: thesis: ( f1 |> f & f is right_identity )
thus f1 |> f by A24; :: thesis: f is right_identity
for f2 being morphism of CategoryStr(# X,comp #) st f2 |> f holds
f2 (*) f = f2
proof
let f2 be morphism of CategoryStr(# X,comp #); :: thesis: ( f2 |> f implies f2 (*) f = f2 )
assume A29: f2 |> f ; :: thesis: f2 (*) f = f2
( f2 = 0 or f2 = 1 ) by TARSKI:def 2;
hence f2 (*) f = f2 by A29, A19; :: thesis: verum
end;
hence f is right_identity ; :: thesis: verum
end;
then A30: CategoryStr(# X,comp #) is with_right_identities ;
for f1, f2, f3 being morphism of CategoryStr(# X,comp #) st f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 holds
f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
proof
let f1, f2, f3 be morphism of CategoryStr(# X,comp #); :: thesis: ( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 implies f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
assume A31: ( f1 |> f2 & f2 |> f3 ) ; :: thesis: ( not f1 (*) f2 |> f3 or not f1 |> f2 (*) f3 or f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
assume A32: f1 (*) f2 |> f3 ; :: thesis: ( not f1 |> f2 (*) f3 or f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
assume A33: f1 |> f2 (*) f3 ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
per cases ( f3 = 0 or f3 = 1 ) by TARSKI:def 2;
suppose A34: f3 = 0 ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
per cases ( f2 = 0 or f2 = 1 ) by TARSKI:def 2;
suppose A35: f2 = 0 ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
then A36: f2 (*) f3 = 0 by A34, A31, A19;
per cases ( f1 = 0 or f1 = 1 ) by TARSKI:def 2;
suppose f1 = 0 ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
hence f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 by A36, A34, A35; :: thesis: verum
end;
suppose A37: f1 = 1 ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
then A38: f1 (*) f2 = 1 by A31, A19;
thus f1 (*) (f2 (*) f3) = 1 by A37, A33, A19
.= (f1 (*) f2) (*) f3 by A32, A38, A19 ; :: thesis: verum
end;
end;
end;
suppose A39: f2 = 1 ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
then ( f2 (*) f3 = 1 & f1 (*) f2 = 1 ) by A31, A19;
hence f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 by A39; :: thesis: verum
end;
end;
end;
suppose A40: f3 = 1 ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
then f2 (*) f3 = 1 by A31, A19;
hence f1 (*) (f2 (*) f3) = 1 by A33, A19
.= (f1 (*) f2) (*) f3 by A32, A40, A19 ;
:: thesis: verum
end;
end;
end;
then reconsider D = CategoryStr(# X,comp #) as category by A26, A27, A30, Def6, Def10, Def12, A25, Def9, Def11;
take the non empty category ; :: thesis: ex D being category ex F being Functor of the non empty category,D st
( F is multiplicative & not F is identity-preserving )
take D ; :: thesis: ex F being Functor of the non empty category,D st
( F is multiplicative & not F is identity-preserving )
reconsider d1 = 1 as morphism of D by TARSKI:def 2;
deffunc H1( object ) -> morphism of D = d1;
A41: for x being object st x in the carrier of the non empty category holds
H1(x) in the carrier of D ;
consider F being Function of the carrier of the non empty category, the carrier of D such that
A42: for x being object st x in the carrier of the non empty category holds
F . x = H1(x) from FUNCT_2:sch 2(A41);
 reconsider F = F as Functor of the non empty category,D ;
take F ; :: thesis: ( F is multiplicative & not F is identity-preserving )
for f1, f2 being morphism of the non empty category st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
proof
let f1, f2 be morphism of the non empty category; :: thesis: ( f1 |> f2 implies ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) )
assume f1 |> f2 ; :: thesis: ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
thus F . f1 |> F . f2 by A24; :: thesis: F . (f1 (*) f2) = (F . f1) (*) (F . f2)
reconsider x1 = f1, x2 = f2, x12 = f1 (*) f2 as object ;
A43: F . f1 = F . x1 by Def21
.= d1 by A42 ;
A44: F . f2 = F . x2 by Def21
.= d1 by A42 ;
A45: d1 |> d1 by A24;
thus F . (f1 (*) f2) = F . x12 by Def21
.= d1 by A42
.= (F . f1) (*) (F . f2) by A43, A44, A45, A19 ; :: thesis: verum
end;
hence F is multiplicative ; :: thesis: not F is identity-preserving
ex f being morphism of the non empty category st
( f is identity & not F . f is identity )
proof
reconsider f = the Object of the non empty category as morphism of the non empty category by TARSKI:def 3;
take f ; :: thesis: ( f is identity & not F . f is identity )
thus f is identity by Th22; :: thesis: not F . f is identity
reconsider x = f as object ;
A46: F . f = F . x by Def21
.= d1 by A42 ;
ex d0 being morphism of D st
( d1 |> d0 & not d1 (*) d0 = d0 )
proof
reconsider d0 = 0 as morphism of D by TARSKI:def 2;
take d0 ; :: thesis: ( d1 |> d0 & not d1 (*) d0 = d0 )
thus d1 |> d0 by A24; :: thesis: not d1 (*) d0 = d0
hence not d1 (*) d0 = d0 by A19; :: thesis: verum
end;
hence not F . f is identity by A46, Def4; :: thesis: verum
end;
hence not F is identity-preserving ; :: thesis: verum