let m, o be set ; the Comp of (1Cat (o,m)) = {[[m,m],m]}
set A = 1Cat (o,m);
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]} )
A1:
dom (id the Object of (1Cat (o,m))) = the
Object of
(1Cat (o,m))
;
A2:
cod (id the Object of (1Cat (o,m))) = the
Object of
(1Cat (o,m))
;
assume A3:
x in the
Comp of
(1Cat (o,m))
;
x in {[[m,m],m]}
then consider x1,
x2 being
object such that A4:
x = [x1,x2]
by RELAT_1:def 1;
A5:
x1 in dom the
Comp of
(1Cat (o,m))
by A3, A4, 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 A6:
x11 in the
carrier' of
(1Cat (o,m))
and A7:
x12 in the
carrier' of
(1Cat (o,m))
and A8:
x1 = [x11,x12]
by A5, ZFMISC_1:def 2;
A9:
x12 = id the
Object of
(1Cat (o,m))
by A7, ZFMISC_1:def 10;
A10:
x2 is
set
by TARSKI:1;
x11 = id the
Object of
(1Cat (o,m))
by A6, 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 A3, A4, A5, A8, A9, FUNCT_1:def 2, A10;
then
x2 = (id the Object of (1Cat (o,m))) (*) (id the Object of (1Cat (o,m)))
by A1, A2, CAT_1:16;
then A11:
x2 = m
by TARSKI:def 1;
A12:
x12 = m
by A7, TARSKI:def 1;
x11 = m
by A6, TARSKI:def 1;
hence
x in {[[m,m],m]}
by A4, A8, A12, A11, 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 A13:
x = [[m,m],m]
by TARSKI:def 1;
f = id the Object of (1Cat (o,m))
by TARSKI:def 1;
hence
x in the Comp of (1Cat (o,m))
by A13, Th1; verum