let o, m 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;
consider a being 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
consider o9 being
Object of
(1Cat o,m);
let x be
set ;
TARSKI:def 3 ( not x in the Comp of (1Cat o,m) or x in {[[m,m],m]} )
A1:
dom (id o9) = o9
by CAT_1:44;
A2:
cod (id o9) = o9
by CAT_1:44;
assume A3:
x in the
Comp of
(1Cat o,m)
;
x in {[[m,m],m]}
then consider x1,
x2 being
set such that A4:
x = [x1,x2]
by RELAT_1:def 1;
A5:
x1 in dom the
Comp of
(1Cat o,m)
by A3, A4, RELAT_1:def 4;
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
set 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 o9
by A7, Th4;
x11 = id o9
by A6, Th4;
then
x2 = the
Comp of
(1Cat o,m) . (id o9),
(id o9)
by A3, A4, A5, A8, A9, FUNCT_1:def 4;
then
x2 = (id o9) * (id o9)
by A1, A2, CAT_1:41;
then A10:
x2 = m
by TARSKI:def 1;
A11:
x12 = m
by A7, TARSKI:def 1;
x11 = m
by A6, TARSKI:def 1;
hence
x in {[[m,m],m]}
by A4, A8, A11, A10, TARSKI:def 1;
verum
end;
let x be set ; 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 A12:
x = [[m,m],m]
by TARSKI:def 1;
f = id a
by TARSKI:def 1;
hence
x in the Comp of (1Cat o,m)
by A12, Th5; verum