let o, m be object ; the Comp of (1Cat (o,m)) = {[[m,m],m]}
set A = 1Cat (o,m);
A1:
1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #)
by CAT_1:def 11;
then reconsider f = m as Morphism of (1Cat (o,m)) by TARSKI:def 1;
set a = the Object of (1Cat (o,m));
thus
the Comp of (1Cat (o,m)) c= {[[m,m],m]}
XBOOLE_0:def 10 {[[m,m],m]} c= the Comp of (1Cat (o,m))proof
set o9 = the
Object of
(1Cat (o,m));
let x be
object ;
TARSKI:def 3 ( not x in the Comp of (1Cat (o,m)) or x in {[[m,m],m]} )
A2:
dom (id the Object of (1Cat (o,m))) = the
Object of
(1Cat (o,m))
;
A3:
cod (id the Object of (1Cat (o,m))) = the
Object of
(1Cat (o,m))
;
assume A4:
x in the
Comp of
(1Cat (o,m))
;
x in {[[m,m],m]}
then consider x1,
x2 being
object such that A5:
x = [x1,x2]
by RELAT_1:def 1;
A6:
x1 in dom the
Comp of
(1Cat (o,m))
by A4, A5, XTUPLE_0:def 12;
dom the
Comp of
(1Cat (o,m)) c= [: the carrier' of (1Cat (o,m)), the carrier' of (1Cat (o,m)):]
by RELAT_1:def 18;
then consider x11,
x12 being
object such that A7:
x11 in the
carrier' of
(1Cat (o,m))
and A8:
x12 in the
carrier' of
(1Cat (o,m))
and A9:
x1 = [x11,x12]
by A6, ZFMISC_1:def 2;
A10:
x12 = id the
Object of
(1Cat (o,m))
by A8, ZFMISC_1:def 10;
A11:
x2 is
set
by TARSKI:1;
x11 = id the
Object of
(1Cat (o,m))
by A7, ZFMISC_1:def 10;
then
x2 = the
Comp of
(1Cat (o,m)) . (
(id the Object of (1Cat (o,m))),
(id the Object of (1Cat (o,m))))
by A4, A5, A6, A9, A10, FUNCT_1:def 2, A11;
then
x2 = (id the Object of (1Cat (o,m))) (*) (id the Object of (1Cat (o,m)))
by A2, A3, CAT_1:16;
then A12:
x2 = m
by A1, TARSKI:def 1;
A13:
x12 = m
by A1, A8, TARSKI:def 1;
x11 = m
by A1, A7, TARSKI:def 1;
hence
x in {[[m,m],m]}
by A5, A9, A13, A12, TARSKI:def 1;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {[[m,m],m]} or x in the Comp of (1Cat (o,m)) )
assume
x in {[[m,m],m]}
; x in the Comp of (1Cat (o,m))
then A14:
x = [[m,m],m]
by TARSKI:def 1;
f = id the Object of (1Cat (o,m))
by A1, TARSKI:def 1;
hence
x in the Comp of (1Cat (o,m))
by A14, Th56; verum