set C = DiscrCat A;
thus
DiscrCat A is pseudo-functional
( DiscrCat A is pseudo-discrete & DiscrCat A is with_units & DiscrCat A is associative )proof
let o1,
o2,
o3 be
Object of
(DiscrCat A);
ALTCAT_1:def 13 the Comp of (DiscrCat A) . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
A1:
id o1 in Funcs (
o1,
o1)
by FUNCT_2:126;
per cases
( ( o1 = o2 & o2 = o3 ) or o1 <> o2 or o2 <> o3 )
;
suppose A2:
(
o1 = o2 &
o2 = o3 )
;
the Comp of (DiscrCat A) . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]then A3:
<^o2,o3^> = {(id o1)}
by Def20;
then A4:
<^o1,o2^> c= Funcs (
o1,
o2)
by A1, A2, ZFMISC_1:31;
thus the
Comp of
(DiscrCat A) . (
o1,
o2,
o3) =
(
(id o1),
(id o1))
:-> (id o1)
by A2, Th19
.=
FuncComp (
{(id o1)},
{(id o1)})
by Th7
.=
(FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
by A2, A3, A4, Th8
;
verum end; suppose A5:
(
o1 <> o2 or
o2 <> o3 )
;
the Comp of (DiscrCat A) . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]then A6:
(
<^o2,o3^> = {} or
<^o1,o2^> = {} )
by Def18;
thus the
Comp of
(DiscrCat A) . (
o1,
o2,
o3) =
{}
by A5, Th18
.=
(FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
by A6
;
verum end;
end;
thus
DiscrCat A is pseudo-discrete
( DiscrCat A is with_units & DiscrCat A is associative )
thus
DiscrCat A is with_units
DiscrCat A is associative proof
thus
the
Comp of
(DiscrCat A) is
with_left_units
ALTCAT_1:def 16 the Comp of (DiscrCat A) is with_right_units proof
let j be
Element of
(DiscrCat A);
ALTCAT_1:def 7 ex e being set st
( e in the Arrows of (DiscrCat A) . (j,j) & ( for i being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (i,j) holds
( the Comp of (DiscrCat A) . (i,j,j)) . (e,f) = f ) )
reconsider j9 =
j as
Object of
(DiscrCat A) ;
take
id j9
;
( id j9 in the Arrows of (DiscrCat A) . (j,j) & ( for i being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (i,j) holds
( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = f ) )
the
Arrows of
(DiscrCat A) . (
j,
j) =
<^j9,j9^>
.=
{(id j9)}
by Def20
;
hence
id j9 in the
Arrows of
(DiscrCat A) . (
j,
j)
by TARSKI:def 1;
for i being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (i,j) holds
( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = f
let i be
Element of
(DiscrCat A);
for f being set st f in the Arrows of (DiscrCat A) . (i,j) holds
( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = flet f be
set ;
( f in the Arrows of (DiscrCat A) . (i,j) implies ( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = f )
assume A7:
f in the
Arrows of
(DiscrCat A) . (
i,
j)
;
( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = f
reconsider i9 =
i as
Object of
(DiscrCat A) ;
A8:
the
Arrows of
(DiscrCat A) . (
i,
j)
= <^i9,j9^>
;
then A9:
i9 = j9
by A7, Def18;
then
f in {(id i9)}
by A7, A8, Def20;
then A10:
f = id i9
by TARSKI:def 1;
thus ( the Comp of (DiscrCat A) . (i,j,j)) . (
(id j9),
f) =
(((id i9),(id i9)) :-> (id i9)) . (
(id j9),
f)
by A9, Th19
.=
f
by A9, A10, FUNCT_4:80
;
verum
end;
let j be
Element of
(DiscrCat A);
ALTCAT_1:def 6 ex e being set st
( e in the Arrows of (DiscrCat A) . (j,j) & ( for j being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (j,j) holds
( the Comp of (DiscrCat A) . (j,j,j)) . (f,e) = f ) )
reconsider j9 =
j as
Object of
(DiscrCat A) ;
take
id j9
;
( id j9 in the Arrows of (DiscrCat A) . (j,j) & ( for j being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (j,j) holds
( the Comp of (DiscrCat A) . (j,j,j)) . (f,(id j9)) = f ) )
the
Arrows of
(DiscrCat A) . (
j,
j) =
<^j9,j9^>
.=
{(id j9)}
by Def20
;
hence
id j9 in the
Arrows of
(DiscrCat A) . (
j,
j)
by TARSKI:def 1;
for j being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (j,j) holds
( the Comp of (DiscrCat A) . (j,j,j)) . (f,(id j9)) = f
let i be
Element of
(DiscrCat A);
for f being set st f in the Arrows of (DiscrCat A) . (j,i) holds
( the Comp of (DiscrCat A) . (j,j,i)) . (f,(id j9)) = flet f be
set ;
( f in the Arrows of (DiscrCat A) . (j,i) implies ( the Comp of (DiscrCat A) . (j,j,i)) . (f,(id j9)) = f )
assume A11:
f in the
Arrows of
(DiscrCat A) . (
j,
i)
;
( the Comp of (DiscrCat A) . (j,j,i)) . (f,(id j9)) = f
reconsider i9 =
i as
Object of
(DiscrCat A) ;
A12:
the
Arrows of
(DiscrCat A) . (
j,
i)
= <^j9,i9^>
;
then A13:
i9 = j9
by A11, Def18;
then
f in {(id i9)}
by A11, A12, Def20;
then A14:
f = id i9
by TARSKI:def 1;
thus ( the Comp of (DiscrCat A) . (j,j,i)) . (
f,
(id j9)) =
(((id i9),(id i9)) :-> (id i9)) . (
f,
(id j9))
by A13, Th19
.=
f
by A13, A14, FUNCT_4:80
;
verum
end;
thus
DiscrCat A is associative
verumproof
let i,
j,
k,
l be
Element of
(DiscrCat A);
ALTCAT_1:def 5,
ALTCAT_1:def 15 for f, g, h being set st f in the Arrows of (DiscrCat A) . (i,j) & g in the Arrows of (DiscrCat A) . (j,k) & h in the Arrows of (DiscrCat A) . (k,l) holds
( the Comp of (DiscrCat A) . (i,k,l)) . (h,(( the Comp of (DiscrCat A) . (i,j,k)) . (g,f))) = ( the Comp of (DiscrCat A) . (i,j,l)) . ((( the Comp of (DiscrCat A) . (j,k,l)) . (h,g)),f)
set G = the
Arrows of
(DiscrCat A);
set c = the
Comp of
(DiscrCat A);
reconsider i9 =
i,
j9 =
j,
k9 =
k,
l9 =
l as
Object of
(DiscrCat A) ;
let f,
g,
h be
set ;
( f in the Arrows of (DiscrCat A) . (i,j) & g in the Arrows of (DiscrCat A) . (j,k) & h in the Arrows of (DiscrCat A) . (k,l) implies ( the Comp of (DiscrCat A) . (i,k,l)) . (h,(( the Comp of (DiscrCat A) . (i,j,k)) . (g,f))) = ( the Comp of (DiscrCat A) . (i,j,l)) . ((( the Comp of (DiscrCat A) . (j,k,l)) . (h,g)),f) )
assume that A15:
f in the
Arrows of
(DiscrCat A) . (
i,
j)
and A16:
g in the
Arrows of
(DiscrCat A) . (
j,
k)
and A17:
h in the
Arrows of
(DiscrCat A) . (
k,
l)
;
( the Comp of (DiscrCat A) . (i,k,l)) . (h,(( the Comp of (DiscrCat A) . (i,j,k)) . (g,f))) = ( the Comp of (DiscrCat A) . (i,j,l)) . ((( the Comp of (DiscrCat A) . (j,k,l)) . (h,g)),f)
f in <^i9,j9^>
by A15;
then A18:
i9 = j9
by Def18;
A19:
<^i9,i9^> = {(id i9)}
by Def20;
then A20:
f = id i9
by A15, A18, TARSKI:def 1;
g in <^j9,k9^>
by A16;
then A21:
j9 = k9
by Def18;
then A22:
g = id i9
by A16, A18, A19, TARSKI:def 1;
A23:
the
Comp of
(DiscrCat A) . (
i9,
i9,
i9)
= (
(id i9),
(id i9))
:-> (id i9)
by Th19;
h in <^k9,l9^>
by A17;
then A24:
k9 = l9
by Def18;
then
h = id i9
by A17, A18, A21, A19, TARSKI:def 1;
hence
( the Comp of (DiscrCat A) . (i,k,l)) . (
h,
(( the Comp of (DiscrCat A) . (i,j,k)) . (g,f)))
= ( the Comp of (DiscrCat A) . (i,j,l)) . (
(( the Comp of (DiscrCat A) . (j,k,l)) . (h,g)),
f)
by A18, A21, A24, A20, A22, A23, FUNCT_4:80;
verum
end;