per cases ( X is empty or not X is empty ) ;
suppose A1: X is empty ; :: thesis: ex b1 being strict discrete category st the carrier of b1 = X
set C = the empty strict associative composable with_identities discrete CategoryStr ;
take the empty strict associative composable with_identities discrete CategoryStr ; :: thesis: the carrier of the empty strict associative composable with_identities discrete CategoryStr = X
thus the carrier of the empty strict associative composable with_identities discrete CategoryStr = X by A1; :: thesis: verum
end;
suppose not X is empty ; :: thesis: ex b1 being strict discrete category st the carrier of b1 = X
set F = { [[x,x],x] where x is Element of X : x in X } ;
A2: for x, y1, y2 being object st [x,y1] in { [[x,x],x] where x is Element of X : x in X } & [x,y2] in { [[x,x],x] where x is Element of X : x in X } holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [[x,x],x] where x is Element of X : x in X } & [x,y2] in { [[x,x],x] where x is Element of X : x in X } implies y1 = y2 )
assume [x,y1] in { [[x,x],x] where x is Element of X : x in X } ; :: thesis: ( not [x,y2] in { [[x,x],x] where x is Element of X : x in X } or y1 = y2 )
then consider x1 being Element of X such that
A3: ( [x,y1] = [[x1,x1],x1] & x1 in X ) ;
assume [x,y2] in { [[x,x],x] where x is Element of X : x in X } ; :: thesis: y1 = y2
then consider x2 being Element of X such that
A4: ( [x,y2] = [[x2,x2],x2] & x2 in X ) ;
A5: ( x = [x1,x1] & y1 = x1 ) by A3, XTUPLE_0:1;
( x = [x2,x2] & y2 = x2 ) by A4, XTUPLE_0:1;
hence y1 = y2 by A5, XTUPLE_0:1; :: thesis: verum
end;
for x being object st x in { [[x,x],x] where x is Element of X : x in X } holds
x in [:[:X,X:],X:]
proof
let x be object ; :: thesis: ( x in { [[x,x],x] where x is Element of X : x in X } implies x in [:[:X,X:],X:] )
assume x in { [[x,x],x] where x is Element of X : x in X } ; :: thesis: x in [:[:X,X:],X:]
then consider x1 being Element of X such that
A6: ( x = [[x1,x1],x1] & x1 in X ) ;
[x1,x1] in [:X,X:] by A6, ZFMISC_1:87;
hence x in [:[:X,X:],X:] by A6, ZFMISC_1:87; :: thesis: verum
end;
then reconsider F = { [[x,x],x] where x is Element of X : x in X } as PartFunc of [:X,X:],X by A2, TARSKI:def 3, FUNCT_1:def 1;
set C = CategoryStr(# X,F #);
for u being morphism of CategoryStr(# X,F #) holds u is identity
proof
let u be morphism of CategoryStr(# X,F #); :: thesis: u is identity
A7: for f being morphism of CategoryStr(# X,F #) st u |> f holds
u (*) f = f
proof
let f be morphism of CategoryStr(# X,F #); :: thesis: ( u |> f implies u (*) f = f )
assume A8: u |> f ; :: thesis: u (*) f = f
u (*) f = F . (u,f) by A8, Def3
.= F . [u,f] by BINOP_1:def 1 ;
then [[u,f],(u (*) f)] in F by A8, FUNCT_1:def 2;
then consider x being Element of X such that
A9: ( [[u,f],(u (*) f)] = [[x,x],x] & x in X ) ;
( [u,f] = [x,x] & u (*) f = x ) by A9, XTUPLE_0:1;
hence u (*) f = f by XTUPLE_0:1; :: thesis: verum
end;
for g being morphism of CategoryStr(# X,F #) st g |> u holds
g (*) u = g
proof
let g be morphism of CategoryStr(# X,F #); :: thesis: ( g |> u implies g (*) u = g )
assume A10: g |> u ; :: thesis: g (*) u = g
g (*) u = F . (g,u) by A10, Def3
.= F . [g,u] by BINOP_1:def 1 ;
then [[g,u],(g (*) u)] in F by A10, FUNCT_1:def 2;
then consider x being Element of X such that
A11: ( [[g,u],(g (*) u)] = [[x,x],x] & x in X ) ;
( [g,u] = [x,x] & g (*) u = x ) by A11, XTUPLE_0:1;
hence g (*) u = g by XTUPLE_0:1; :: thesis: verum
end;
then ( u is left_identity & u is right_identity ) by A7;
hence u is identity ; :: thesis: verum
end;
then reconsider C = CategoryStr(# X,F #) as strict discrete CategoryStr by Def15;
A12: now :: thesis: for f being morphism of C st f in the carrier of C holds
( ex c being morphism of C st
( c |> f & c is left_identity ) & ex d being morphism of C st
( f |> d & d is right_identity ) )
let f be morphism of C; :: thesis: ( f in the carrier of C implies ( ex c being morphism of C st
( c |> f & c is left_identity ) & ex d being morphism of C st
( f |> d & d is right_identity ) ) )
assume A13: f in the carrier of C ; :: thesis: ( ex c being morphism of C st
( c |> f & c is left_identity ) & ex d being morphism of C st
( f |> d & d is right_identity ) )
then A14: ( f is identity & f in X ) by Def15;
reconsider x = f as Element of X ;
[[f,f],f] in { [[x,x],x] where x is Element of X : x in X } by A13;
then [f,f] in dom the composition of C by XTUPLE_0:def 12;
hence ( ex c being morphism of C st
( c |> f & c is left_identity ) & ex d being morphism of C st
( f |> d & d is right_identity ) ) by Def2, A14; :: thesis: verum
end;
( C is with_left_identities & C is with_right_identities ) by A12;
then reconsider C = C as strict associative composable with_identities discrete CategoryStr by Def12;
take C ; :: thesis: the carrier of C = X
thus the carrier of C = X ; :: thesis: verum
end;
end;