consider C being strict preorder category such that
A1:
Ob C = 1
and
for o1, o2 being Object of C st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]}
and
A2:
RelOb C = RelIncl 1
and
A3:
Mor C = 1 \/ { [o1,o2] where o1, o2 is Element of 1 : o1 in o2 }
by CAT_7:37;
A4:
C is 1 -ordered
by A2, WELLORD1:38, CAT_7:def 14;
then A5:
C ~= OrdC 1
by CAT_7:38;
consider F being Functor of C,(OrdC 1), G being Functor of (OrdC 1),C such that
A6:
( F is covariant & G is covariant )
and
A7:
( G (*) F = id C & F (*) G = id (OrdC 1) )
by A4, CAT_7:38, CAT_6:def 28;
A8:
0 in Ob C
by A1, CARD_1:49, TARSKI:def 1;
then reconsider g = 0 as morphism of C ;
A9:
not C is empty
by A1;
then A10:
g is identity
by A8, CAT_6:22;
set f = F . g;
take
F . g
; ( F . g is identity & Ob (OrdC 1) = {(F . g)} & Mor (OrdC 1) = {(F . g)} )
thus A11:
F . g is identity
by A6, A10, CAT_6:def 22, CAT_6:def 25; ( Ob (OrdC 1) = {(F . g)} & Mor (OrdC 1) = {(F . g)} )
card (Ob (OrdC 1)) = card 1
by A1, A5, CAT_7:14;
then consider x being object such that
A12:
Ob (OrdC 1) = {x}
by CARD_2:42;
F . g is Object of (OrdC 1)
by A11, CAT_6:22;
hence A13:
Ob (OrdC 1) = {(F . g)}
by A12, TARSKI:def 1; Mor (OrdC 1) = {(F . g)}
for x being object holds
( x in Mor (OrdC 1) iff x in {(F . g)} )
proof
let x be
object ;
( x in Mor (OrdC 1) iff x in {(F . g)} )
hereby ( x in {(F . g)} implies x in Mor (OrdC 1) )
assume A14:
x in Mor (OrdC 1)
;
x in {(F . g)}then A15:
x in the
carrier of
(OrdC 1)
by CAT_6:def 1;
reconsider f1 =
x as
morphism of
(OrdC 1) by A14;
per cases
( f1 is identity or not f1 is identity )
;
suppose A16:
not
f1 is
identity
;
x in {(F . g)}A17:
(id the carrier of (OrdC 1)) . x = x
by A15, FUNCT_1:18;
A18:
F . (G . f1) =
(F (*) G) . f1
by A6, CAT_6:34
.=
(id the carrier of (OrdC 1)) . f1
by A7, STRUCT_0:def 4
.=
f1
by A17, CAT_6:def 21
;
not
G . f1 is
identity
by A18, A16, CAT_6:def 22, A6, CAT_6:def 25;
then
not
G . f1 in 1
by A1, A9, CAT_6:22;
then
G . f1 in { [o1,o2] where o1, o2 is Element of 1 : o1 in o2 }
by A3, XBOOLE_0:def 3;
then consider o1,
o2 being
Element of 1
such that A19:
(
G . f1 = [o1,o2] &
o1 in o2 )
;
A20:
o1 = 0
by CARD_1:49, TARSKI:def 1;
o2 = 0
by CARD_1:49, TARSKI:def 1;
hence
x in {(F . g)}
by A19, A20;
verum end; end;
end;
assume
x in {(F . g)}
;
x in Mor (OrdC 1)
hence
x in Mor (OrdC 1)
by A13;
verum
end;
hence
Mor (OrdC 1) = {(F . g)}
by TARSKI:2; verum