let C be category; ( ( not C is empty & C is trivial ) iff C ~= OrdC 1 )
hereby ( C ~= OrdC 1 implies ( not C is empty & C is trivial ) )
assume A1:
( not
C is
empty &
C is
trivial )
;
C ~= OrdC 1consider f being
morphism of
(OrdC 1) such that A2:
(
f is
identity &
Ob (OrdC 1) = {f} &
Mor (OrdC 1) = {f} )
by Th15;
ex
F being
Functor of
C,
(OrdC 1) st
(
F is
covariant &
F is
bijective )
proof
set F = the
carrier of
C --> f;
the
carrier of
(OrdC 1) = {f}
by A2, CAT_6:def 1;
then
f in the
carrier of
(OrdC 1)
by TARSKI:def 1;
then reconsider F = the
carrier of
C --> f as
Functor of
C,
(OrdC 1) by FUNCOP_1:45;
take
F
;
( F is covariant & F is bijective )
for
f1 being
morphism of
C st
f1 is
identity holds
F . f1 is
identity
then A4:
F is
identity-preserving
by CAT_6:def 22;
for
f1,
f2 being
morphism of
C st
f1 |> f2 holds
(
F . f1 |> F . f2 &
F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
proof
let f1,
f2 be
morphism of
C;
( f1 |> f2 implies ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) )
assume
f1 |> f2
;
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
reconsider x1 =
f1,
x2 =
f2,
x =
f1 (*) f2 as
object ;
not
Mor C is
empty
by A1;
then
(
f1 in Mor C &
f2 in Mor C &
f1 (*) f2 in Mor C )
;
then A5:
(
f1 in the
carrier of
C &
f2 in the
carrier of
C &
f1 (*) f2 in the
carrier of
C )
by CAT_6:def 1;
A6:
F . f1 =
F . x1
by A1, CAT_6:def 21
.=
f
by A5, FUNCOP_1:7
;
A7:
F . f2 =
F . x2
by A1, CAT_6:def 21
.=
f
by A5, FUNCOP_1:7
;
A8:
F . (f1 (*) f2) =
F . x
by A1, CAT_6:def 21
.=
f
by A5, FUNCOP_1:7
;
thus
F . f1 |> F . f2
by A2, A6, A7, CAT_6:24;
F . (f1 (*) f2) = (F . f1) (*) (F . f2)
f |> f
by A2, CAT_6:24;
hence
F . (f1 (*) f2) = (F . f1) (*) (F . f2)
by A2, A6, A7, A8, Th4;
verum
end;
hence
F is
covariant
by A4, CAT_6:def 25, CAT_6:def 23;
F is bijective
for
x1,
x2 being
object st
x1 in dom F &
x2 in dom F &
F . x1 = F . x2 holds
x1 = x2
by A1, ZFMISC_1:def 10;
then A9:
F is
one-to-one
by FUNCT_1:def 4;
rng F =
{f}
by A1, FUNCOP_1:8
.=
the
carrier of
(OrdC 1)
by A2, CAT_6:def 1
;
then
F is
onto
by FUNCT_2:def 3;
hence
F is
bijective
by A9;
verum
end; hence
C ~= OrdC 1
by CAT_7:12;
verum
end;
assume
C ~= OrdC 1
; ( not C is empty & C is trivial )
then
C is terminal
by Th26;
hence
( not C is empty & C is trivial )
by Lm1; verum