let O be ordinal number ; ex C being strict preorder category st
( Ob C = O & ( for o1, o2 being Object of C st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} ) & RelOb C = RelIncl O & Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )
per cases
( O is empty or not O is empty )
;
suppose A1:
O is
empty
;
ex C being strict preorder category st
( Ob C = O & ( for o1, o2 being Object of C st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} ) & RelOb C = RelIncl O & Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )set C = the
empty strict category;
take
the
empty strict category
;
( Ob the empty strict category = O & ( for o1, o2 being Object of the empty strict category st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} ) & RelOb the empty strict category = RelIncl O & Mor the empty strict category = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )thus
Ob the
empty strict category = O
by A1;
( ( for o1, o2 being Object of the empty strict category st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} ) & RelOb the empty strict category = RelIncl O & Mor the empty strict category = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )
for
x being
object holds not
x in { [o1,o2] where o1, o2 is Element of O : o1 in o2 }
hence
( ( for
o1,
o2 being
Object of the
empty strict category st
o1 in o2 holds
Hom (
o1,
o2)
= {[o1,o2]} ) &
RelOb the
empty strict category = RelIncl O &
Mor the
empty strict category = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )
by A1, SUBSET_1:def 1, XBOOLE_0:def 1;
verum end; suppose A3:
not
O is
empty
;
ex C being strict preorder category st
( Ob C = O & ( for o1, o2 being Object of C st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} ) & RelOb C = RelIncl O & Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )set X1 =
{ [o1,o2] where o1, o2 is Element of O : o1 in o2 } ;
set X =
O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ;
set F1 =
{ [[o1,o1],o1] where o1 is Element of O : verum } ;
set F2 =
{ [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ;
set F3 =
{ [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ;
set F4 =
{ [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } ;
set F =
(( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } ;
A4:
for
x being
object holds
( not
x in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } or ex
o1 being
Element of
O st
x = [[o1,o1],o1] or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
proof
let x be
object ;
( not x in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } or ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
assume A5:
x in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) }
;
( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
per cases
( x in ( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } or x in { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } )
by A5, XBOOLE_0:def 3;
suppose A6:
x in ( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 }
;
( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )per cases
( x in { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } or x in { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } )
by A6, XBOOLE_0:def 3;
suppose A7:
x in { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 }
;
( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )per cases
( x in { [[o1,o1],o1] where o1 is Element of O : verum } or x in { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } )
by A7, XBOOLE_0:def 3;
suppose
x in { [[o1,o1],o1] where o1 is Element of O : verum }
;
( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )then consider o1 being
Element of
O such that A8:
x = [[o1,o1],o1]
;
thus
( ex
o1 being
Element of
O st
x = [[o1,o1],o1] or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A8;
verum end; suppose
x in { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 }
;
( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )then consider o1,
o2 being
Element of
O such that A9:
(
x = [[o2,[o1,o2]],[o1,o2]] &
o1 in o2 )
;
thus
( ex
o1 being
Element of
O st
x = [[o1,o1],o1] or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A9;
verum end; suppose
x in { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 }
;
( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )then consider o1,
o2 being
Element of
O such that A10:
(
x = [[[o1,o2],o1],[o1,o2]] &
o1 in o2 )
;
thus
( ex
o1 being
Element of
O st
x = [[o1,o1],o1] or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A10;
verum end; suppose
x in { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) }
;
( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )then consider o1,
o2,
o3 being
Element of
O such that A11:
(
x = [[[o2,o3],[o1,o2]],[o1,o3]] &
o1 in o2 &
o2 in o3 )
;
thus
( ex
o1 being
Element of
O st
x = [[o1,o1],o1] or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A11;
verum end;
end; A12:
for
x,
y1,
y2 being
object st
[x,y1] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } &
[x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( [x,y1] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } & [x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } implies y1 = y2 )
assume A13:
[x,y1] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) }
;
( not [x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } or y1 = y2 )
per cases
( ex o1 being Element of O st [x,y1] = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( [x,y1] = [[o2,[o1,o2]],[o1,o2]] or [x,y1] = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & [x,y1] = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A4, A13;
suppose
ex
o1 being
Element of
O st
[x,y1] = [[o1,o1],o1]
;
( not [x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } or y1 = y2 )then consider o1 being
Element of
O such that A14:
[x,y1] = [[o1,o1],o1]
;
A15:
(
x = [o1,o1] &
y1 = o1 )
by A14, XTUPLE_0:1;
assume A16:
[x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) }
;
y1 = y2per cases
( ex o1 being Element of O st [x,y2] = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( [x,y2] = [[o2,[o1,o2]],[o1,o2]] or [x,y2] = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & [x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A4, A16;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
[x,y2] = [[o2,[o1,o2]],[o1,o2]] or
[x,y2] = [[[o1,o2],o1],[o1,o2]] ) )
;
y1 = y2then consider o11,
o12 being
Element of
O such that A18:
(
o11 in o12 & (
[x,y2] = [[o12,[o11,o12]],[o11,o12]] or
[x,y2] = [[[o11,o12],o11],[o11,o12]] ) )
;
(
x = [o12,[o11,o12]] or
x = [[o11,o12],o11] )
by A18, XTUPLE_0:1;
hence
y1 = y2
by A15, XTUPLE_0:1;
verum end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
[x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
y1 = y2then consider o11,
o12,
o13 being
Element of
O such that A19:
(
o11 in o12 &
o12 in o13 &
[x,y2] = [[[o12,o13],[o11,o12]],[o11,o13]] )
;
x = [[o12,o13],[o11,o12]]
by A19, XTUPLE_0:1;
hence
y1 = y2
by A15, XTUPLE_0:1;
verum end; end; suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
[x,y1] = [[o2,[o1,o2]],[o1,o2]] or
[x,y1] = [[[o1,o2],o1],[o1,o2]] ) )
;
( not [x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } or y1 = y2 )then consider o1,
o2 being
Element of
O such that A20:
(
o1 in o2 & (
[x,y1] = [[o2,[o1,o2]],[o1,o2]] or
[x,y1] = [[[o1,o2],o1],[o1,o2]] ) )
;
per cases
( [x,y1] = [[o2,[o1,o2]],[o1,o2]] or [x,y1] = [[[o1,o2],o1],[o1,o2]] )
by A20;
suppose
[x,y1] = [[o2,[o1,o2]],[o1,o2]]
;
( not [x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } or y1 = y2 )then A21:
(
x = [o2,[o1,o2]] &
y1 = [o1,o2] )
by XTUPLE_0:1;
assume A22:
[x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) }
;
y1 = y2per cases
( ex o1 being Element of O st [x,y2] = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( [x,y2] = [[o2,[o1,o2]],[o1,o2]] or [x,y2] = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & [x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A4, A22;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
[x,y2] = [[o2,[o1,o2]],[o1,o2]] or
[x,y2] = [[[o1,o2],o1],[o1,o2]] ) )
;
y1 = y2then consider o11,
o12 being
Element of
O such that A24:
(
o11 in o12 & (
[x,y2] = [[o12,[o11,o12]],[o11,o12]] or
[x,y2] = [[[o11,o12],o11],[o11,o12]] ) )
;
per cases
( [x,y2] = [[o12,[o11,o12]],[o11,o12]] or [x,y2] = [[[o11,o12],o11],[o11,o12]] )
by A24;
end; end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
[x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
y1 = y2then consider o11,
o12,
o13 being
Element of
O such that A25:
(
o11 in o12 &
o12 in o13 &
[x,y2] = [[[o12,o13],[o11,o12]],[o11,o13]] )
;
x = [[o12,o13],[o11,o12]]
by A25, XTUPLE_0:1;
hence
y1 = y2
by A21, XTUPLE_0:1;
verum end; end; suppose
[x,y1] = [[[o1,o2],o1],[o1,o2]]
;
( not [x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } or y1 = y2 )then A26:
(
x = [[o1,o2],o1] &
y1 = [o1,o2] )
by XTUPLE_0:1;
assume A27:
[x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) }
;
y1 = y2per cases
( ex o1 being Element of O st [x,y2] = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( [x,y2] = [[o2,[o1,o2]],[o1,o2]] or [x,y2] = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & [x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A4, A27;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
[x,y2] = [[o2,[o1,o2]],[o1,o2]] or
[x,y2] = [[[o1,o2],o1],[o1,o2]] ) )
;
y1 = y2then consider o11,
o12 being
Element of
O such that A29:
(
o11 in o12 & (
[x,y2] = [[o12,[o11,o12]],[o11,o12]] or
[x,y2] = [[[o11,o12],o11],[o11,o12]] ) )
;
per cases
( [x,y2] = [[o12,[o11,o12]],[o11,o12]] or [x,y2] = [[[o11,o12],o11],[o11,o12]] )
by A29;
end; end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
[x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
y1 = y2then consider o11,
o12,
o13 being
Element of
O such that A31:
(
o11 in o12 &
o12 in o13 &
[x,y2] = [[[o12,o13],[o11,o12]],[o11,o13]] )
;
x = [[o12,o13],[o11,o12]]
by A31, XTUPLE_0:1;
hence
y1 = y2
by A26, XTUPLE_0:1;
verum end; end; end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
[x,y1] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
( not [x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } or y1 = y2 )then consider o1,
o2,
o3 being
Element of
O such that A32:
(
o1 in o2 &
o2 in o3 &
[x,y1] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
A33:
(
x = [[o2,o3],[o1,o2]] &
y1 = [o1,o3] )
by A32, XTUPLE_0:1;
assume A34:
[x,y2] in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) }
;
y1 = y2per cases
( ex o1 being Element of O st [x,y2] = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( [x,y2] = [[o2,[o1,o2]],[o1,o2]] or [x,y2] = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & [x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A4, A34;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
[x,y2] = [[o2,[o1,o2]],[o1,o2]] or
[x,y2] = [[[o1,o2],o1],[o1,o2]] ) )
;
y1 = y2then consider o11,
o12 being
Element of
O such that A36:
(
o11 in o12 & (
[x,y2] = [[o12,[o11,o12]],[o11,o12]] or
[x,y2] = [[[o11,o12],o11],[o11,o12]] ) )
;
(
x = [o12,[o11,o12]] or
x = [[o11,o12],o11] )
by A36, XTUPLE_0:1;
hence
y1 = y2
by A33, XTUPLE_0:1;
verum end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
[x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
y1 = y2then consider o11,
o12,
o13 being
Element of
O such that A37:
(
o11 in o12 &
o12 in o13 &
[x,y2] = [[[o12,o13],[o11,o12]],[o11,o13]] )
;
(
x = [[o12,o13],[o11,o12]] &
y2 = [o11,o13] )
by A37, XTUPLE_0:1;
then
(
[o1,o2] = [o11,o12] &
[o2,o3] = [o12,o13] )
by A33, XTUPLE_0:1;
then
(
o1 = o11 &
o2 = o12 &
o3 = o13 )
by XTUPLE_0:1;
hence
y1 = y2
by A32, XTUPLE_0:1, A37;
verum end; end;
end; A38:
for
o1,
o2 being
Element of
O st
o1 in o2 holds
[o1,o2] in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 }
proof
let o1,
o2 be
Element of
O;
( o1 in o2 implies [o1,o2] in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )
assume
o1 in o2
;
[o1,o2] in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 }
then
[o1,o2] in { [o1,o2] where o1, o2 is Element of O : o1 in o2 }
;
hence
[o1,o2] in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 }
by XBOOLE_0:def 3;
verum
end;
for
x being
object st
x in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } holds
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
proof
let x be
object ;
( x in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } implies x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):] )
assume A39:
x in (( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) }
;
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
per cases
( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A39, A4;
suppose
ex
o1 being
Element of
O st
x = [[o1,o1],o1]
;
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]then consider o1 being
Element of
O such that A40:
x = [[o1,o1],o1]
;
A41:
o1 in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 }
by A3, XBOOLE_0:def 3;
then
[o1,o1] in [:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
by ZFMISC_1:def 2;
hence
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
by A40, A41, ZFMISC_1:def 2;
verum end; suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) )
;
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]then consider o1,
o2 being
Element of
O such that A42:
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) )
;
per cases
( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] )
by A42;
suppose A43:
x = [[o2,[o1,o2]],[o1,o2]]
;
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]A44:
(
o2 in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } &
[o1,o2] in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )
by A42, A38, A3, XBOOLE_0:def 3;
then
[o2,[o1,o2]] in [:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
by ZFMISC_1:def 2;
hence
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
by A43, A44, ZFMISC_1:def 2;
verum end; suppose A45:
x = [[[o1,o2],o1],[o1,o2]]
;
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]A46:
(
o1 in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } &
[o1,o2] in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )
by A42, A38, A3, XBOOLE_0:def 3;
then
[[o1,o2],o1] in [:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
by ZFMISC_1:def 2;
hence
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
by A45, A46, ZFMISC_1:def 2;
verum end; end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]then consider o1,
o2,
o3 being
Element of
O such that A47:
(
o1 in o2 &
o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
A48:
(
[o1,o2] in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } &
[o2,o3] in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } &
[o1,o3] in O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )
by A47, A38, ORDINAL1:10;
then
[[o2,o3],[o1,o2]] in [:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
by ZFMISC_1:def 2;
hence
x in [:[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):]
by A47, A48, ZFMISC_1:def 2;
verum end;
end; then reconsider F =
(( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o2,o3],[o1,o2]],[o1,o3]] where o1, o2, o3 is Element of O : ( o1 in o2 & o2 in o3 ) } as
PartFunc of
[:(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ):],
(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ) by A12, TARSKI:def 3, FUNCT_1:def 1;
set C =
CategoryStr(#
(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),
F #);
reconsider C =
CategoryStr(#
(O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } ),
F #) as non
empty strict CategoryStr by A3;
A49:
for
f being
morphism of
C holds
(
f is
Element of
O or ex
o1,
o2 being
Element of
O st
(
f = [o1,o2] &
o1 in o2 ) )
A52:
for
o being
Element of
O holds
o is
morphism of
C
A53:
for
o1,
o2 being
Element of
O st
o1 in o2 holds
ex
f being
morphism of
C st
f = [o1,o2]
A54:
for
x being
object st ( ex
o1 being
Element of
O st
x = [[o1,o1],o1] or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]] ) ) holds
x in F
proof
let x be
object ;
( ( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) ) implies x in F )
assume A55:
( ex
o1 being
Element of
O st
x = [[o1,o1],o1] or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
;
x in F
per cases
( ex o1 being Element of O st x = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( x = [[o2,[o1,o2]],[o1,o2]] or x = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A55;
suppose
ex
o1 being
Element of
O st
x = [[o1,o1],o1]
;
x in Fthen
x in { [[o1,o1],o1] where o1 is Element of O : verum }
;
then
x in { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 }
by XBOOLE_0:def 3;
then
x in ( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 }
by XBOOLE_0:def 3;
hence
x in F
by XBOOLE_0:def 3;
verum end; suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
x = [[o2,[o1,o2]],[o1,o2]] or
x = [[[o1,o2],o1],[o1,o2]] ) )
;
x in Fthen
(
x in { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } or
x in { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } )
;
then
x in { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 }
by XBOOLE_0:def 3;
then
x in { [[o1,o1],o1] where o1 is Element of O : verum } \/ ( { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } )
by XBOOLE_0:def 3;
then
x in ( { [[o1,o1],o1] where o1 is Element of O : verum } \/ { [[o2,[o1,o2]],[o1,o2]] where o1, o2 is Element of O : o1 in o2 } ) \/ { [[[o1,o2],o1],[o1,o2]] where o1, o2 is Element of O : o1 in o2 }
by XBOOLE_1:4;
hence
x in F
by XBOOLE_0:def 3;
verum end;
end; A56:
for
o1 being
Element of
O for
f1,
f2 being
morphism of
C st
f1 = o1 &
f2 = o1 holds
(
f1 |> f2 &
f1 (*) f2 = o1 )
proof
let o1 be
Element of
O;
for f1, f2 being morphism of C st f1 = o1 & f2 = o1 holds
( f1 |> f2 & f1 (*) f2 = o1 )let f1,
f2 be
morphism of
C;
( f1 = o1 & f2 = o1 implies ( f1 |> f2 & f1 (*) f2 = o1 ) )
assume A57:
(
f1 = o1 &
f2 = o1 )
;
( f1 |> f2 & f1 (*) f2 = o1 )
A58:
[[f1,f2],f2] in F
by A57, A54;
then A59:
[f1,f2] in dom the
composition of
C
by XTUPLE_0:def 12;
hence
f1 |> f2
by CAT_6:def 2;
f1 (*) f2 = o1
thus f1 (*) f2 =
the
composition of
C . (
f1,
f2)
by A59, CAT_6:def 2, CAT_6:def 3
.=
F . [f1,f2]
by BINOP_1:def 1
.=
o1
by A57, A58, FUNCT_1:1
;
verum
end; A60:
for
o1,
o2 being
Element of
O for
f1,
f2 being
morphism of
C st
f1 = o2 &
f2 = [o1,o2] &
o1 in o2 holds
(
f1 |> f2 &
f1 (*) f2 = [o1,o2] )
proof
let o1,
o2 be
Element of
O;
for f1, f2 being morphism of C st f1 = o2 & f2 = [o1,o2] & o1 in o2 holds
( f1 |> f2 & f1 (*) f2 = [o1,o2] )let f1,
f2 be
morphism of
C;
( f1 = o2 & f2 = [o1,o2] & o1 in o2 implies ( f1 |> f2 & f1 (*) f2 = [o1,o2] ) )
assume A61:
(
f1 = o2 &
f2 = [o1,o2] )
;
( not o1 in o2 or ( f1 |> f2 & f1 (*) f2 = [o1,o2] ) )
assume A62:
o1 in o2
;
( f1 |> f2 & f1 (*) f2 = [o1,o2] )
A63:
[[f1,f2],f2] in F
by A61, A62, A54;
then A64:
[f1,f2] in dom the
composition of
C
by XTUPLE_0:def 12;
hence
f1 |> f2
by CAT_6:def 2;
f1 (*) f2 = [o1,o2]
thus f1 (*) f2 =
the
composition of
C . (
f1,
f2)
by A64, CAT_6:def 2, CAT_6:def 3
.=
F . [f1,f2]
by BINOP_1:def 1
.=
[o1,o2]
by A61, A63, FUNCT_1:1
;
verum
end; A65:
for
o1,
o2 being
Element of
O for
f1,
f2 being
morphism of
C st
f1 = [o1,o2] &
f2 = o1 &
o1 in o2 holds
(
f1 |> f2 &
f1 (*) f2 = [o1,o2] )
proof
let o1,
o2 be
Element of
O;
for f1, f2 being morphism of C st f1 = [o1,o2] & f2 = o1 & o1 in o2 holds
( f1 |> f2 & f1 (*) f2 = [o1,o2] )let f1,
f2 be
morphism of
C;
( f1 = [o1,o2] & f2 = o1 & o1 in o2 implies ( f1 |> f2 & f1 (*) f2 = [o1,o2] ) )
assume A66:
(
f1 = [o1,o2] &
f2 = o1 )
;
( not o1 in o2 or ( f1 |> f2 & f1 (*) f2 = [o1,o2] ) )
assume A67:
o1 in o2
;
( f1 |> f2 & f1 (*) f2 = [o1,o2] )
A68:
[[f1,f2],f1] in F
by A66, A67, A54;
then A69:
[f1,f2] in dom the
composition of
C
by XTUPLE_0:def 12;
hence
f1 |> f2
by CAT_6:def 2;
f1 (*) f2 = [o1,o2]
thus f1 (*) f2 =
the
composition of
C . (
f1,
f2)
by A69, CAT_6:def 2, CAT_6:def 3
.=
F . [f1,f2]
by BINOP_1:def 1
.=
[o1,o2]
by A66, A68, FUNCT_1:1
;
verum
end; A70:
for
o1,
o2,
o3 being
Element of
O for
f1,
f2 being
morphism of
C st
f1 = [o2,o3] &
f2 = [o1,o2] &
o1 in o2 &
o2 in o3 holds
(
f1 |> f2 &
f1 (*) f2 = [o1,o3] )
proof
let o1,
o2,
o3 be
Element of
O;
for f1, f2 being morphism of C st f1 = [o2,o3] & f2 = [o1,o2] & o1 in o2 & o2 in o3 holds
( f1 |> f2 & f1 (*) f2 = [o1,o3] )let f1,
f2 be
morphism of
C;
( f1 = [o2,o3] & f2 = [o1,o2] & o1 in o2 & o2 in o3 implies ( f1 |> f2 & f1 (*) f2 = [o1,o3] ) )
assume A71:
(
f1 = [o2,o3] &
f2 = [o1,o2] )
;
( not o1 in o2 or not o2 in o3 or ( f1 |> f2 & f1 (*) f2 = [o1,o3] ) )
assume A72:
(
o1 in o2 &
o2 in o3 )
;
( f1 |> f2 & f1 (*) f2 = [o1,o3] )
then consider f3 being
morphism of
C such that A73:
f3 = [o1,o3]
by A53, ORDINAL1:10;
A74:
[[f1,f2],f3] in F
by A71, A72, A73, A54;
then A75:
[f1,f2] in dom the
composition of
C
by XTUPLE_0:def 12;
hence
f1 |> f2
by CAT_6:def 2;
f1 (*) f2 = [o1,o3]
thus f1 (*) f2 =
the
composition of
C . (
f1,
f2)
by A75, CAT_6:def 2, CAT_6:def 3
.=
F . [f1,f2]
by BINOP_1:def 1
.=
[o1,o3]
by A73, A74, FUNCT_1:1
;
verum
end; A76:
for
o1,
o2 being
Element of
O for
f1,
f2 being
morphism of
C st
f1 = o1 &
f2 = o2 &
f1 |> f2 holds
o1 = o2
proof
let o1,
o2 be
Element of
O;
for f1, f2 being morphism of C st f1 = o1 & f2 = o2 & f1 |> f2 holds
o1 = o2let f1,
f2 be
morphism of
C;
( f1 = o1 & f2 = o2 & f1 |> f2 implies o1 = o2 )
assume A77:
(
f1 = o1 &
f2 = o2 )
;
( not f1 |> f2 or o1 = o2 )
assume
f1 |> f2
;
o1 = o2
then
[f1,f2] in dom the
composition of
C
by CAT_6:def 2;
then consider y being
object such that A78:
[[f1,f2],y] in F
by XTUPLE_0:def 12;
per cases
( ex o1 being Element of O st [[f1,f2],y] = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( [[f1,f2],y] = [[o2,[o1,o2]],[o1,o2]] or [[f1,f2],y] = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & [[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A78, A4;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
[[f1,f2],y] = [[o2,[o1,o2]],[o1,o2]] or
[[f1,f2],y] = [[[o1,o2],o1],[o1,o2]] ) )
;
o1 = o2then consider o11,
o12 being
Element of
O such that A80:
(
o11 in o12 & (
[[f1,f2],y] = [[o12,[o11,o12]],[o11,o12]] or
[[f1,f2],y] = [[[o11,o12],o11],[o11,o12]] ) )
;
(
[f1,f2] = [o12,[o11,o12]] or
[f1,f2] = [[o11,o12],o11] )
by A80, XTUPLE_0:1;
hence
o1 = o2
by A77, XTUPLE_0:1;
verum end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
o1 = o2then consider o1,
o2,
o3 being
Element of
O such that A81:
(
o1 in o2 &
o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
[f1,f2] = [[o2,o3],[o1,o2]]
by A81, XTUPLE_0:1;
hence
o1 = o2
by A77, XTUPLE_0:1;
verum end;
end; A82:
for
o1,
o2,
o3 being
Element of
O for
f1,
f2 being
morphism of
C st
f1 = o1 &
f2 = [o2,o3] &
f1 |> f2 holds
o1 = o3
proof
let o1,
o2,
o3 be
Element of
O;
for f1, f2 being morphism of C st f1 = o1 & f2 = [o2,o3] & f1 |> f2 holds
o1 = o3let f1,
f2 be
morphism of
C;
( f1 = o1 & f2 = [o2,o3] & f1 |> f2 implies o1 = o3 )
assume A83:
(
f1 = o1 &
f2 = [o2,o3] )
;
( not f1 |> f2 or o1 = o3 )
assume
f1 |> f2
;
o1 = o3
then
[f1,f2] in dom the
composition of
C
by CAT_6:def 2;
then consider y being
object such that A84:
[[f1,f2],y] in F
by XTUPLE_0:def 12;
per cases
( ex o1 being Element of O st [[f1,f2],y] = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( [[f1,f2],y] = [[o2,[o1,o2]],[o1,o2]] or [[f1,f2],y] = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & [[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A84, A4;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
[[f1,f2],y] = [[o2,[o1,o2]],[o1,o2]] or
[[f1,f2],y] = [[[o1,o2],o1],[o1,o2]] ) )
;
o1 = o3then consider o11,
o12 being
Element of
O such that A86:
(
o11 in o12 & (
[[f1,f2],y] = [[o12,[o11,o12]],[o11,o12]] or
[[f1,f2],y] = [[[o11,o12],o11],[o11,o12]] ) )
;
end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
o1 = o3then consider o1,
o2,
o3 being
Element of
O such that A87:
(
o1 in o2 &
o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
[f1,f2] = [[o2,o3],[o1,o2]]
by A87, XTUPLE_0:1;
hence
o1 = o3
by A83, XTUPLE_0:1;
verum end;
end; A88:
for
o1,
o2,
o3 being
Element of
O for
f1,
f2 being
morphism of
C st
f1 = [o1,o2] &
f2 = o3 &
f1 |> f2 holds
o1 = o3
proof
let o1,
o2,
o3 be
Element of
O;
for f1, f2 being morphism of C st f1 = [o1,o2] & f2 = o3 & f1 |> f2 holds
o1 = o3let f1,
f2 be
morphism of
C;
( f1 = [o1,o2] & f2 = o3 & f1 |> f2 implies o1 = o3 )
assume A89:
(
f1 = [o1,o2] &
f2 = o3 )
;
( not f1 |> f2 or o1 = o3 )
assume
f1 |> f2
;
o1 = o3
then
[f1,f2] in dom the
composition of
C
by CAT_6:def 2;
then consider y being
object such that A90:
[[f1,f2],y] in F
by XTUPLE_0:def 12;
per cases
( ex o1 being Element of O st [[f1,f2],y] = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( [[f1,f2],y] = [[o2,[o1,o2]],[o1,o2]] or [[f1,f2],y] = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & [[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A90, A4;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
[[f1,f2],y] = [[o2,[o1,o2]],[o1,o2]] or
[[f1,f2],y] = [[[o1,o2],o1],[o1,o2]] ) )
;
o1 = o3then consider o11,
o12 being
Element of
O such that A92:
(
o11 in o12 & (
[[f1,f2],y] = [[o12,[o11,o12]],[o11,o12]] or
[[f1,f2],y] = [[[o11,o12],o11],[o11,o12]] ) )
;
end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
o1 = o3then consider o1,
o2,
o3 being
Element of
O such that A93:
(
o1 in o2 &
o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
[f1,f2] = [[o2,o3],[o1,o2]]
by A93, XTUPLE_0:1;
hence
o1 = o3
by A89, XTUPLE_0:1;
verum end;
end; A94:
for
o being
Element of
O for
f being
morphism of
C st
f = o holds
f is
identity
for
f1 being
morphism of
C st
f1 in the
carrier of
C holds
ex
f being
morphism of
C st
(
f |> f1 &
f is
left_identity )
then A103:
C is
with_left_identities
by CAT_6:def 6;
A104:
for
f1 being
morphism of
C st
f1 in the
carrier of
C holds
ex
f being
morphism of
C st
(
f1 |> f &
f is
right_identity )
A107:
for
f1,
f2 being
morphism of
C holds
( not
f1 |> f2 or ex
o1 being
Element of
O st
(
f1 = o1 &
f2 = o1 ) or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f1 = [o1,o2] &
f2 = o1 ) or (
f1 = o2 &
f2 = [o1,o2] ) ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f1 = [o2,o3] &
f2 = [o1,o2] ) )
proof
let f1,
f2 be
morphism of
C;
( not f1 |> f2 or ex o1 being Element of O st
( f1 = o1 & f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 = [o1,o2] & f2 = o1 ) or ( f1 = o2 & f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2] ) )
assume
f1 |> f2
;
( ex o1 being Element of O st
( f1 = o1 & f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 = [o1,o2] & f2 = o1 ) or ( f1 = o2 & f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2] ) )
then
[f1,f2] in dom the
composition of
C
by CAT_6:def 2;
then consider y being
object such that A108:
[[f1,f2],y] in F
by XTUPLE_0:def 12;
per cases
( ex o1 being Element of O st [[f1,f2],y] = [[o1,o1],o1] or ex o1, o2 being Element of O st
( o1 in o2 & ( [[f1,f2],y] = [[o2,[o1,o2]],[o1,o2]] or [[f1,f2],y] = [[[o1,o2],o1],[o1,o2]] ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & [[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] ) )
by A108, A4;
suppose
ex
o1 being
Element of
O st
[[f1,f2],y] = [[o1,o1],o1]
;
( ex o1 being Element of O st
( f1 = o1 & f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 = [o1,o2] & f2 = o1 ) or ( f1 = o2 & f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2] ) )then consider o11 being
Element of
O such that A109:
[[f1,f2],y] = [[o11,o11],o11]
;
[f1,f2] = [o11,o11]
by A109, XTUPLE_0:1;
then
(
f1 = o11 &
f2 = o11 )
by XTUPLE_0:1;
hence
( ex
o1 being
Element of
O st
(
f1 = o1 &
f2 = o1 ) or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f1 = [o1,o2] &
f2 = o1 ) or (
f1 = o2 &
f2 = [o1,o2] ) ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f1 = [o2,o3] &
f2 = [o1,o2] ) )
;
verum end; suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & (
[[f1,f2],y] = [[o2,[o1,o2]],[o1,o2]] or
[[f1,f2],y] = [[[o1,o2],o1],[o1,o2]] ) )
;
( ex o1 being Element of O st
( f1 = o1 & f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 = [o1,o2] & f2 = o1 ) or ( f1 = o2 & f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2] ) )then consider o11,
o12 being
Element of
O such that A110:
(
o11 in o12 & (
[[f1,f2],y] = [[o12,[o11,o12]],[o11,o12]] or
[[f1,f2],y] = [[[o11,o12],o11],[o11,o12]] ) )
;
per cases
( [f1,f2] = [o12,[o11,o12]] or [f1,f2] = [[o11,o12],o11] )
by A110, XTUPLE_0:1;
suppose
[f1,f2] = [o12,[o11,o12]]
;
( ex o1 being Element of O st
( f1 = o1 & f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 = [o1,o2] & f2 = o1 ) or ( f1 = o2 & f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2] ) )then
(
f1 = o12 &
f2 = [o11,o12] )
by XTUPLE_0:1;
hence
( ex
o1 being
Element of
O st
(
f1 = o1 &
f2 = o1 ) or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f1 = [o1,o2] &
f2 = o1 ) or (
f1 = o2 &
f2 = [o1,o2] ) ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f1 = [o2,o3] &
f2 = [o1,o2] ) )
by A110;
verum end; suppose
[f1,f2] = [[o11,o12],o11]
;
( ex o1 being Element of O st
( f1 = o1 & f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 = [o1,o2] & f2 = o1 ) or ( f1 = o2 & f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2] ) )then
(
f1 = [o11,o12] &
f2 = o11 )
by XTUPLE_0:1;
hence
( ex
o1 being
Element of
O st
(
f1 = o1 &
f2 = o1 ) or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f1 = [o1,o2] &
f2 = o1 ) or (
f1 = o2 &
f2 = [o1,o2] ) ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f1 = [o2,o3] &
f2 = [o1,o2] ) )
by A110;
verum end; end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
( ex o1 being Element of O st
( f1 = o1 & f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 = [o1,o2] & f2 = o1 ) or ( f1 = o2 & f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2] ) )then consider o1,
o2,
o3 being
Element of
O such that A111:
(
o1 in o2 &
o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]] )
;
[f1,f2] = [[o2,o3],[o1,o2]]
by A111, XTUPLE_0:1;
then
(
f1 = [o2,o3] &
f2 = [o1,o2] )
by XTUPLE_0:1;
hence
( ex
o1 being
Element of
O st
(
f1 = o1 &
f2 = o1 ) or ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f1 = [o1,o2] &
f2 = o1 ) or (
f1 = o2 &
f2 = [o1,o2] ) ) ) or ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f1 = [o2,o3] &
f2 = [o1,o2] ) )
by A111;
verum end;
end;
for
f,
f1,
f2 being
morphism of
C st
f1 |> f2 holds
(
f1 (*) f2 |> f iff
f2 |> f )
proof
let f,
f1,
f2 be
morphism of
C;
( f1 |> f2 implies ( f1 (*) f2 |> f iff f2 |> f ) )
assume A112:
f1 |> f2
;
( f1 (*) f2 |> f iff f2 |> f )
per cases
( ex o1 being Element of O st
( f1 = o1 & f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 = [o1,o2] & f2 = o1 ) or ( f1 = o2 & f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2] ) )
by A112, A107;
suppose
ex
o1 being
Element of
O st
(
f1 = o1 &
f2 = o1 )
;
( f1 (*) f2 |> f iff f2 |> f )then consider o1 being
Element of
O such that A113:
(
f1 = o1 &
f2 = o1 )
;
A114:
f1 (*) f2 = o1
by A113, A56;
hereby ( f2 |> f implies f1 (*) f2 |> f )
assume A115:
f1 (*) f2 |> f
;
f2 |> fper cases
( ex o1 being Element of O st
( f1 (*) f2 = o1 & f = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 (*) f2 = [o1,o2] & f = o1 ) or ( f1 (*) f2 = o2 & f = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 (*) f2 = [o2,o3] & f = [o1,o2] ) )
by A115, A107;
suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f1 (*) f2 = [o2,o3] &
f = [o1,o2] )
;
f2 |> fthen consider o11,
o12,
o13 being
Element of
O such that A118:
(
o11 in o12 &
o12 in o13 &
f1 (*) f2 = [o12,o13] &
f = [o11,o12] )
;
thus
f2 |> f
by A118, A113, A56;
verum end;
end; assume A119:
f2 |> f
;
f1 (*) f2 |> f end; suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f1 = [o1,o2] &
f2 = o1 ) or (
f1 = o2 &
f2 = [o1,o2] ) ) )
;
( f1 (*) f2 |> f iff f2 |> f )then consider o1,
o2 being
Element of
O such that A123:
(
o1 in o2 & ( (
f1 = [o1,o2] &
f2 = o1 ) or (
f1 = o2 &
f2 = [o1,o2] ) ) )
;
A124:
f1 (*) f2 = [o1,o2]
by A123, A60, A65;
hereby ( f2 |> f implies f1 (*) f2 |> f )
assume A125:
f1 (*) f2 |> f
;
f2 |> f
end; assume A130:
f2 |> f
;
f1 (*) f2 |> fper cases
( ex o1 being Element of O st
( f2 = o1 & f = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f2 = [o1,o2] & f = o1 ) or ( f2 = o2 & f = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f2 = [o2,o3] & f = [o1,o2] ) )
by A130, A107;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f2 = [o1,o2] &
f = o1 ) or (
f2 = o2 &
f = [o1,o2] ) ) )
;
f1 (*) f2 |> fthen consider o11,
o12 being
Element of
O such that A132:
(
o11 in o12 & ( (
f2 = [o11,o12] &
f = o11 ) or (
f2 = o12 &
f = [o11,o12] ) ) )
;
end; end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f1 = [o2,o3] &
f2 = [o1,o2] )
;
( f1 (*) f2 |> f iff f2 |> f )then consider o1,
o2,
o3 being
Element of
O such that A135:
(
o1 in o2 &
o2 in o3 &
f1 = [o2,o3] &
f2 = [o1,o2] )
;
A136:
f1 (*) f2 = [o1,o3]
by A135, A70;
hereby ( f2 |> f implies f1 (*) f2 |> f )
assume A137:
f1 (*) f2 |> f
;
f2 |> f
end; assume A141:
f2 |> f
;
f1 (*) f2 |> fper cases
( ex o1 being Element of O st
( f2 = o1 & f = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f2 = [o1,o2] & f = o1 ) or ( f2 = o2 & f = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f2 = [o2,o3] & f = [o1,o2] ) )
by A141, A107;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f2 = [o1,o2] &
f = o1 ) or (
f2 = o2 &
f = [o1,o2] ) ) )
;
f1 (*) f2 |> fthen consider o11,
o12 being
Element of
O such that A143:
(
o11 in o12 & ( (
f2 = [o11,o12] &
f = o11 ) or (
f2 = o12 &
f = [o11,o12] ) ) )
;
end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f2 = [o2,o3] &
f = [o1,o2] )
;
f1 (*) f2 |> fthen consider o11,
o12,
o13 being
Element of
O such that A146:
(
o11 in o12 &
o12 in o13 &
f2 = [o12,o13] &
f = [o11,o12] )
;
A147:
(
o1 = o12 &
o2 = o13 )
by A135, A146, XTUPLE_0:1;
o1 in o3
by A135, ORDINAL1:10;
hence
f1 (*) f2 |> f
by A146, A147, A136, A70;
verum end; end;
end; then A148:
C is
left_composable
by CAT_6:def 8;
A149:
for
f,
f1,
f2 being
morphism of
C st
f1 |> f2 holds
(
f |> f1 (*) f2 iff
f |> f1 )
proof
let f,
f1,
f2 be
morphism of
C;
( f1 |> f2 implies ( f |> f1 (*) f2 iff f |> f1 ) )
assume A150:
f1 |> f2
;
( f |> f1 (*) f2 iff f |> f1 )
per cases
( ex o1 being Element of O st
( f1 = o1 & f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f1 = [o1,o2] & f2 = o1 ) or ( f1 = o2 & f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2] ) )
by A150, A107;
suppose
ex
o1 being
Element of
O st
(
f1 = o1 &
f2 = o1 )
;
( f |> f1 (*) f2 iff f |> f1 )then consider o1 being
Element of
O such that A151:
(
f1 = o1 &
f2 = o1 )
;
A152:
f1 (*) f2 = o1
by A151, A56;
hereby ( f |> f1 implies f |> f1 (*) f2 )
assume A153:
f |> f1 (*) f2
;
f |> f1per cases
( ex o1 being Element of O st
( f = o1 & f1 (*) f2 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f = [o1,o2] & f1 (*) f2 = o1 ) or ( f = o2 & f1 (*) f2 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f = [o2,o3] & f1 (*) f2 = [o1,o2] ) )
by A153, A107;
suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f = [o2,o3] &
f1 (*) f2 = [o1,o2] )
;
f |> f1then consider o11,
o12,
o13 being
Element of
O such that A156:
(
o11 in o12 &
o12 in o13 &
f = [o12,o13] &
f1 (*) f2 = [o11,o12] )
;
thus
f |> f1
by A156, A151, A56;
verum end;
end; assume A157:
f |> f1
;
f |> f1 (*) f2 end; suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f1 = [o1,o2] &
f2 = o1 ) or (
f1 = o2 &
f2 = [o1,o2] ) ) )
;
( f |> f1 (*) f2 iff f |> f1 )then consider o1,
o2 being
Element of
O such that A161:
(
o1 in o2 & ( (
f1 = [o1,o2] &
f2 = o1 ) or (
f1 = o2 &
f2 = [o1,o2] ) ) )
;
A162:
f1 (*) f2 = [o1,o2]
by A161, A60, A65;
hereby ( f |> f1 implies f |> f1 (*) f2 )
assume A163:
f |> f1 (*) f2
;
f |> f1
end; assume A168:
f |> f1
;
f |> f1 (*) f2per cases
( ex o1 being Element of O st
( f = o1 & f1 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f = [o1,o2] & f1 = o1 ) or ( f = o2 & f1 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f = [o2,o3] & f1 = [o1,o2] ) )
by A168, A107;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f = [o1,o2] &
f1 = o1 ) or (
f = o2 &
f1 = [o1,o2] ) ) )
;
f |> f1 (*) f2then consider o11,
o12 being
Element of
O such that A170:
(
o11 in o12 & ( (
f = [o11,o12] &
f1 = o11 ) or (
f = o12 &
f1 = [o11,o12] ) ) )
;
end; end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f1 = [o2,o3] &
f2 = [o1,o2] )
;
( f |> f1 (*) f2 iff f |> f1 )then consider o1,
o2,
o3 being
Element of
O such that A174:
(
o1 in o2 &
o2 in o3 &
f1 = [o2,o3] &
f2 = [o1,o2] )
;
A175:
f1 (*) f2 = [o1,o3]
by A174, A70;
hereby ( f |> f1 implies f |> f1 (*) f2 )
assume A176:
f |> f1 (*) f2
;
f |> f1
end; assume A180:
f |> f1
;
f |> f1 (*) f2per cases
( ex o1 being Element of O st
( f = o1 & f1 = o1 ) or ex o1, o2 being Element of O st
( o1 in o2 & ( ( f = [o1,o2] & f1 = o1 ) or ( f = o2 & f1 = [o1,o2] ) ) ) or ex o1, o2, o3 being Element of O st
( o1 in o2 & o2 in o3 & f = [o2,o3] & f1 = [o1,o2] ) )
by A180, A107;
suppose
ex
o1,
o2 being
Element of
O st
(
o1 in o2 & ( (
f = [o1,o2] &
f1 = o1 ) or (
f = o2 &
f1 = [o1,o2] ) ) )
;
f |> f1 (*) f2then consider o11,
o12 being
Element of
O such that A182:
(
o11 in o12 & ( (
f = [o11,o12] &
f1 = o11 ) or (
f = o12 &
f1 = [o11,o12] ) ) )
;
end; suppose
ex
o1,
o2,
o3 being
Element of
O st
(
o1 in o2 &
o2 in o3 &
f = [o2,o3] &
f1 = [o1,o2] )
;
f |> f1 (*) f2then consider o11,
o12,
o13 being
Element of
O such that A185:
(
o11 in o12 &
o12 in o13 &
f = [o12,o13] &
f1 = [o11,o12] )
;
A186:
(
o2 = o11 &
o3 = o12 )
by A174, A185, XTUPLE_0:1;
o1 in o3
by A174, ORDINAL1:10;
hence
f |> f1 (*) f2
by A185, A186, A175, A70;
verum end; end;
end; reconsider C =
C as non
empty strict composable with_identities CategoryStr by A104, A103, CAT_6:def 7, CAT_6:def 12, A149, A148, CAT_6:def 9, CAT_6:def 11;
A187:
for
x being
object holds
(
x in Ob C iff
x in O )
then A194:
Ob C = O
by TARSKI:2;
A195:
for
o1,
o2 being
Object of
C for
f being
morphism of
C holds
( not
f in Hom (
o1,
o2) or (
f = o1 &
o1 = o2 ) or (
f = [o1,o2] &
o1 in o2 ) )
proof
let o1,
o2 be
Object of
C;
for f being morphism of C holds
( not f in Hom (o1,o2) or ( f = o1 & o1 = o2 ) or ( f = [o1,o2] & o1 in o2 ) )let f be
morphism of
C;
( not f in Hom (o1,o2) or ( f = o1 & o1 = o2 ) or ( f = [o1,o2] & o1 in o2 ) )
assume
f in Hom (
o1,
o2)
;
( ( f = o1 & o1 = o2 ) or ( f = [o1,o2] & o1 in o2 ) )
then A196:
(
dom f = o1 &
cod f = o2 )
by Th20;
assume A197:
( not
f = o1 or not
o1 = o2 )
;
( f = [o1,o2] & o1 in o2 )
per cases
( f is Element of O or ex o1, o2 being Element of O st
( f = [o1,o2] & o1 in o2 ) )
by A49;
suppose
ex
o1,
o2 being
Element of
O st
(
f = [o1,o2] &
o1 in o2 )
;
( f = [o1,o2] & o1 in o2 )then consider o11,
o22 being
Element of
O such that A198:
(
f = [o11,o22] &
o11 in o22 )
;
A199:
(
o11 in Ob C &
o22 in Ob C )
by A194;
reconsider f1 =
o11,
f2 =
o22 as
morphism of
C by A199;
f1 is
identity
by A94;
then A200:
dom f = o11
by A198, A65, CAT_6:26;
f2 is
identity
by A94;
hence
(
f = [o1,o2] &
o1 in o2 )
by A198, A200, A196, A60, CAT_6:27;
verum end;
end; A201:
for
o1,
o2 being
Object of
C for
f1,
f2 being
morphism of
C st
f1 in Hom (
o1,
o2) &
f2 in Hom (
o1,
o2) holds
f1 = f2
proof
let o1,
o2 be
Object of
C;
for f1, f2 being morphism of C st f1 in Hom (o1,o2) & f2 in Hom (o1,o2) holds
f1 = f2let f1,
f2 be
morphism of
C;
( f1 in Hom (o1,o2) & f2 in Hom (o1,o2) implies f1 = f2 )
assume A202:
f1 in Hom (
o1,
o2)
;
( not f2 in Hom (o1,o2) or f1 = f2 )
assume A203:
f2 in Hom (
o1,
o2)
;
f1 = f2
end; then
C is
preorder
;
then reconsider C =
C as
strict preorder category ;
take
C
;
( Ob C = O & ( for o1, o2 being Object of C st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} ) & RelOb C = RelIncl O & Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )thus A206:
Ob C = O
by A187, TARSKI:2;
( ( for o1, o2 being Object of C st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} ) & RelOb C = RelIncl O & Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )thus A207:
for
o1,
o2 being
Object of
C st
o1 in o2 holds
Hom (
o1,
o2)
= {[o1,o2]}
( RelOb C = RelIncl O & Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )proof
let o1,
o2 be
Object of
C;
( o1 in o2 implies Hom (o1,o2) = {[o1,o2]} )
A208:
(
o1 in Ob C &
o2 in Ob C )
by SUBSET_1:def 1;
assume A209:
o1 in o2
;
Hom (o1,o2) = {[o1,o2]}
reconsider o11 =
o1,
o22 =
o2 as
Element of
O by A187;
consider f being
morphism of
C such that A210:
f = [o11,o22]
by A209, A53;
reconsider f1 =
o1,
f2 =
o2 as
morphism of
C by A208;
A211:
f1 is
identity
by A94, A206;
A212:
dom f = o1
by A210, A209, A65, A211, CAT_6:26;
A213:
f2 is
identity
by A94, A206;
cod f = o2
by A210, A209, A60, A213, CAT_6:27;
then
f in { ff where ff is morphism of C : ( dom ff = o1 & cod ff = o2 ) }
by A212;
then A214:
f in Hom (
o1,
o2)
by Def2;
for
x being
object holds
(
x in Hom (
o1,
o2) iff
x = [o1,o2] )
by A210, A214, A201;
hence
Hom (
o1,
o2)
= {[o1,o2]}
by TARSKI:def 1;
verum
end;
for
a,
b being
object holds
(
[a,b] in RelOb C iff
[a,b] in RelIncl O )
proof
let a,
b be
object ;
( [a,b] in RelOb C iff [a,b] in RelIncl O )
hereby ( [a,b] in RelIncl O implies [a,b] in RelOb C )
assume
[a,b] in RelOb C
;
[a,b] in RelIncl Othen consider o1,
o2 being
Object of
C such that A215:
(
[a,b] = [o1,o2] & ex
f being
morphism of
C st
f in Hom (
o1,
o2) )
;
consider f being
morphism of
C such that A216:
f in Hom (
o1,
o2)
by A215;
A217:
(
dom f = o1 &
cod f = o2 )
by A216, Th20;
A218:
o1 c= o2
proof
per cases
( f is Element of O or ex o1, o2 being Element of O st
( f = [o1,o2] & o1 in o2 ) )
by A49;
suppose
ex
o1,
o2 being
Element of
O st
(
f = [o1,o2] &
o1 in o2 )
;
o1 c= o2then consider o11,
o22 being
Element of
O such that A219:
(
f = [o11,o22] &
o11 in o22 )
;
(
o11 in O &
o22 in O )
by A3;
then reconsider f1 =
o11,
f2 =
o22 as
morphism of
C by A206;
A220:
f1 is
identity
by A94;
A221:
f2 is
identity
by A94;
(
o1 = o11 &
o2 = o22 )
by A219, A65, A220, CAT_6:26, A217, A60, A221, CAT_6:27;
hence
o1 c= o2
by A219, ORDINAL1:def 2;
verum end;
end; thus
[a,b] in RelIncl O
by A206, A215, A218, WELLORD2:def 1;
verum
end;
assume A222:
[a,b] in RelIncl O
;
[a,b] in RelOb C
then A223:
(
a in field (RelIncl O) &
b in field (RelIncl O) )
by RELAT_1:15;
then A224:
(
a in O &
b in O )
by WELLORD2:def 1;
reconsider o1 =
a,
o2 =
b as
Object of
C by A223, A206, WELLORD2:def 1;
A225:
o1 c= o2
by A222, A224, WELLORD2:def 1;
ex
f being
morphism of
C st
f in Hom (
o1,
o2)
hence
[a,b] in RelOb C
;
verum
end; hence
RelOb C = RelIncl O
by RELAT_1:def 2;
Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } thus
Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 }
by CAT_6:def 1;
verum end;