let x be object ; for C being CategoryStr st the carrier of C = {x} & the composition of C = {[[x,x],x]} holds
C is non empty category
let C be CategoryStr ; ( the carrier of C = {x} & the composition of C = {[[x,x],x]} implies C is non empty category )
assume A1:
the carrier of C = {x}
; ( not the composition of C = {[[x,x],x]} or C is non empty category )
assume A2:
the composition of C = {[[x,x],x]}
; C is non empty category
A3:
the carrier of C = the carrier of (DiscreteCat {x})
by A1, CAT_6:def 16;
for y being object holds
( y in the composition of (DiscreteCat {x}) iff y in {[[x,x],x]} )
proof
let y be
object ;
( y in the composition of (DiscreteCat {x}) iff y in {[[x,x],x]} )
hereby ( y in {[[x,x],x]} implies y in the composition of (DiscreteCat {x}) )
assume
y in the
composition of
(DiscreteCat {x})
;
y in {[[x,x],x]}then consider x1,
x2 being
object such that A4:
(
y = [x1,x2] &
x1 in [: the carrier of (DiscreteCat {x}), the carrier of (DiscreteCat {x}):] &
x2 in the
carrier of
(DiscreteCat {x}) )
by RELSET_1:2;
A5:
(
x1 in [:{x},{x}:] &
x2 = x )
by A3, A4, A1, TARSKI:def 1;
x1 in {[x,x]}
by ZFMISC_1:29, A3, A4, A1;
then
x1 = [x,x]
by TARSKI:def 1;
hence
y in {[[x,x],x]}
by A5, A4, TARSKI:def 1;
verum
end;
assume A6:
y in {[[x,x],x]}
;
y in the composition of (DiscreteCat {x})
x in the
carrier of
(DiscreteCat {x})
by A3, A1, TARSKI:def 1;
then reconsider f =
x as
morphism of
(DiscreteCat {x}) by CAT_6:def 1;
A7:
y = [[f,f],f]
by A6, TARSKI:def 1;
A8:
not
DiscreteCat {x} is
empty
by CAT_6:def 16;
A9:
f is
identity
by CAT_6:def 15;
A10:
f |> f
by A8, CAT_6:24, CAT_6:def 15;
then A11:
[f,f] in dom the
composition of
(DiscreteCat {x})
by CAT_6:def 2;
f = f (*) f
by A9, A10, Th4;
then
the
composition of
(DiscreteCat {x}) . (
f,
f)
= f
by A10, CAT_6:def 3;
then
the
composition of
(DiscreteCat {x}) . [f,f] = f
by BINOP_1:def 1;
hence
y in the
composition of
(DiscreteCat {x})
by A7, A11, FUNCT_1:1;
verum
end;
then
the composition of (DiscreteCat {x}) = {[[x,x],x]}
by TARSKI:2;
hence
C is non empty category
by A3, A2, CAT_6:14, CAT_6:15, CAT_6:20; verum