let C, D be with_identities CategoryStr ; :: thesis: ( C ~= D implies ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) ) )

assume C ~= D ; :: thesis: ( 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 ;

assume C ~= D ; :: thesis: ( 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 )
;

end;

suppose A4:
D is empty
; :: thesis: ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) )

C is empty
by A4, A1, CAT_6:31;

hence ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) ) by A4; :: thesis: verum

end;hence ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) ) by A4; :: thesis: verum

suppose A5:
not D is empty
; :: thesis: ( 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; :: thesis: 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 )

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; :: thesis: verum

end;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; :: thesis: 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

then A19:
rng (F | (Ob C)) = Ob D
by TARSKI:2;
let y be object ; :: thesis: ( y in rng (F | (Ob C)) iff y in Ob D )

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; :: thesis: verum

end;hereby :: thesis: ( y in Ob D implies y in rng (F | (Ob C)) )

assume
y in Ob D
; :: thesis: y in rng (F | (Ob C))assume
y in rng (F | (Ob C))
; :: thesis: y in Ob D

then consider x being object such that

A10: ( x in dom (F | (Ob C)) & y = (F | (Ob C)) . x ) by FUNCT_1:def 3;

A11: x in Ob C by A10;

A12: y = F . x by A10, FUNCT_1:49;

x in { f where f is morphism of C : ( f is identity & f in Mor C ) } by A11, CAT_6:def 17;

then consider f being morphism of C such that

A13: ( x = f & f is identity & f in Mor C ) ;

not C is empty by A10;

then A14: y = F . f by A12, A13, CAT_6:def 21;

then reconsider g = y as morphism of D ;

Mor D <> {} by A5;

then ( g is identity & g in Mor D ) by A14, A13, CAT_6:def 22, A1, CAT_6:def 25;

then g in { f1 where f1 is morphism of D : ( f1 is identity & f1 in Mor D ) } ;

hence y in Ob D by CAT_6:def 17; :: thesis: verum

end;then consider x being object such that

A10: ( x in dom (F | (Ob C)) & y = (F | (Ob C)) . x ) by FUNCT_1:def 3;

A11: x in Ob C by A10;

A12: y = F . x by A10, FUNCT_1:49;

x in { f where f is morphism of C : ( f is identity & f in Mor C ) } by A11, CAT_6:def 17;

then consider f being morphism of C such that

A13: ( x = f & f is identity & f in Mor C ) ;

not C is empty by A10;

then A14: y = F . f by A12, A13, CAT_6:def 21;

then reconsider g = y as morphism of D ;

Mor D <> {} by A5;

then ( g is identity & g in Mor D ) by A14, A13, CAT_6:def 22, A1, CAT_6:def 25;

then g in { f1 where f1 is morphism of D : ( f1 is identity & f1 in Mor D ) } ;

hence y in Ob D by CAT_6:def 17; :: thesis: verum

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; :: thesis: verum

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; :: thesis: verum