let C, D be with_identities CategoryStr ; ( C ~= D implies ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) ) )
assume
C ~= D
; ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) )
then consider F being Functor of C,D, G being Functor of D,C such that
A1:
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D )
by CAT_6:def 28;
F * G =
id C
by A1, CAT_6:def 27
.=
id the carrier of C
by STRUCT_0:def 4
;
then A2:
F is one-to-one
by FUNCT_2:23;
A3: G * F =
id D
by A1, CAT_6:def 27
.=
id the carrier of D
by STRUCT_0:def 4
;
per cases
( D is empty or not D is empty )
;
suppose A5:
not
D is
empty
;
( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) )
F is
onto
by A3, FUNCT_2:23;
then
rng F = the
carrier of
D
by FUNCT_2:def 3;
then A6:
rng F = Mor D
by CAT_6:def 1;
A7:
dom F = the
carrier of
C
by A5, FUNCT_2:def 1;
then A8:
dom F = Mor C
by CAT_6:def 1;
hence
card (Mor C) = card (Mor D)
by CARD_1:5, A6, A2, WELLORD2:def 4;
card (Ob C) = card (Ob D)set F1 =
F | (Ob C);
A9:
dom (F | (Ob C)) = Ob C
by A8, RELAT_1:62;
for
y being
object holds
(
y in rng (F | (Ob C)) iff
y in Ob D )
proof
let y be
object ;
( y in rng (F | (Ob C)) iff y in Ob D )
assume
y in Ob D
;
y in rng (F | (Ob C))
then
y in { g where g is morphism of D : ( g is identity & g in Mor D ) }
by CAT_6:def 17;
then consider g being
morphism of
D such that A15:
(
y = g &
g is
identity &
g in Mor D )
;
consider x being
object such that A16:
(
x in dom F &
g = F . x )
by A15, A6, FUNCT_1:def 3;
reconsider f =
x as
morphism of
C by A16, CAT_6:def 1;
A17:
not
C is
empty
by A16;
then
g = F . f
by A16, CAT_6:def 21;
then G . g =
(G (*) F) . f
by A1, A17, CAT_6:34
.=
(id C) . x
by A1, A17, CAT_6:def 21
.=
(id the carrier of C) . x
by STRUCT_0:def 4
.=
x
by FUNCT_1:18, A16
;
then
(
f is
identity &
f in Mor C )
by A16, A7, A15, CAT_6:def 22, A1, CAT_6:def 25, CAT_6:def 1;
then
f in { f1 where f1 is morphism of C : ( f1 is identity & f1 in Mor C ) }
;
then A18:
f in Ob C
by CAT_6:def 17;
g = (F | (Ob C)) . f
by A18, A16, FUNCT_1:49;
hence
y in rng (F | (Ob C))
by A9, A18, A15, FUNCT_1:def 3;
verum
end; then A19:
rng (F | (Ob C)) = Ob D
by TARSKI:2;
F | (Ob C) is
one-to-one
by A2, FUNCT_1:52;
hence
card (Ob C) = card (Ob D)
by CARD_1:5, A9, A19, WELLORD2:def 4;
verum end; end;