let C1, C2 be composable with_identities CategoryStr ; :: thesis: ( C1 ~= C2 implies RelOb C1, RelOb C2 are_isomorphic )

assume A1: C1 ~= C2 ; :: thesis: RelOb C1, RelOb C2 are_isomorphic

assume A1: C1 ~= C2 ; :: thesis: RelOb C1, RelOb C2 are_isomorphic

per cases
( C1 is empty or not C1 is empty )
;

end;

suppose A2:
C1 is empty
; :: thesis: RelOb C1, RelOb C2 are_isomorphic

then A3:
RelOb C1 is empty
;

C2 is empty by A2, A1, Th15;

then RelOb C2 is empty ;

hence RelOb C1, RelOb C2 are_isomorphic by A3, WELLORD1:38; :: thesis: verum

end;C2 is empty by A2, A1, Th15;

then RelOb C2 is empty ;

hence RelOb C1, RelOb C2 are_isomorphic by A3, WELLORD1:38; :: thesis: verum

suppose A4:
not C1 is empty
; :: thesis: RelOb C1, RelOb C2 are_isomorphic

then A5:
not C2 is empty
by A1, Th15;

consider F being Functor of C1,C2, G being Functor of C2,C1 such that

A6: ( F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2 ) by A1, CAT_6:def 28;

F * G = id C1 by A6, CAT_6:def 27

.= id the carrier of C1 by STRUCT_0:def 4 ;

then A7: F is one-to-one by FUNCT_2:23;

set F1 = F | (Ob C1);

A8: dom F = the carrier of C1 by A5, FUNCT_2:def 1

.= Mor C1 by CAT_6:def 1 ;

then A9: dom (F | (Ob C1)) = Ob C1 by RELAT_1:62;

A10: Ob C1 = (Ob C1) \/ (Ob C1)

.= (Ob C1) \/ (rng (RelOb C1)) by Th34

.= (dom (RelOb C1)) \/ (rng (RelOb C1)) by Th34

.= field (RelOb C1) by RELAT_1:def 6 ;

then A11: dom (F | (Ob C1)) = field (RelOb C1) by A8, RELAT_1:62;

for y being object st y in rng (F | (Ob C1)) holds

y in Ob C2

for y being object st y in Ob C2 holds

y in rng (F | (Ob C1))

then A26: rng (F | (Ob C1)) = Ob C2 by A15, XBOOLE_0:def 10;

A27: rng (F | (Ob C1)) = (Ob C2) \/ (Ob C2) by A25, A15, XBOOLE_0:def 10

.= (Ob C2) \/ (rng (RelOb C2)) by Th34

.= (dom (RelOb C2)) \/ (rng (RelOb C2)) by Th34

.= field (RelOb C2) by RELAT_1:def 6 ;

A28: F | (Ob C1) is one-to-one by A7, FUNCT_1:52;

for a, b being object holds

( [a,b] in RelOb C1 iff ( a in field (RelOb C1) & b in field (RelOb C1) & [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 ) )

end;consider F being Functor of C1,C2, G being Functor of C2,C1 such that

A6: ( F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2 ) by A1, CAT_6:def 28;

F * G = id C1 by A6, CAT_6:def 27

.= id the carrier of C1 by STRUCT_0:def 4 ;

then A7: F is one-to-one by FUNCT_2:23;

set F1 = F | (Ob C1);

A8: dom F = the carrier of C1 by A5, FUNCT_2:def 1

.= Mor C1 by CAT_6:def 1 ;

then A9: dom (F | (Ob C1)) = Ob C1 by RELAT_1:62;

A10: Ob C1 = (Ob C1) \/ (Ob C1)

.= (Ob C1) \/ (rng (RelOb C1)) by Th34

.= (dom (RelOb C1)) \/ (rng (RelOb C1)) by Th34

.= field (RelOb C1) by RELAT_1:def 6 ;

then A11: dom (F | (Ob C1)) = field (RelOb C1) by A8, RELAT_1:62;

for y being object st y in rng (F | (Ob C1)) holds

y in Ob C2

proof

then A15:
rng (F | (Ob C1)) c= Ob C2
by TARSKI:def 3;
let y be object ; :: thesis: ( y in rng (F | (Ob C1)) implies y in Ob C2 )

assume y in rng (F | (Ob C1)) ; :: thesis: y in Ob C2

then consider x being object such that

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

x in Ob C1 by A12;

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

then consider f being morphism of C1 such that

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

A14: y = F . x by A12, FUNCT_1:49

.= F . f by A13, A4, CAT_6:def 21 ;

F . f is identity by A13, CAT_6:def 22, A6, CAT_6:def 25;

then F . f in { g where g is morphism of C2 : ( g is identity & g in Mor C2 ) } by A5;

hence y in Ob C2 by A14, CAT_6:def 17; :: thesis: verum

end;assume y in rng (F | (Ob C1)) ; :: thesis: y in Ob C2

then consider x being object such that

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

x in Ob C1 by A12;

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

then consider f being morphism of C1 such that

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

A14: y = F . x by A12, FUNCT_1:49

.= F . f by A13, A4, CAT_6:def 21 ;

F . f is identity by A13, CAT_6:def 22, A6, CAT_6:def 25;

then F . f in { g where g is morphism of C2 : ( g is identity & g in Mor C2 ) } by A5;

hence y in Ob C2 by A14, CAT_6:def 17; :: thesis: verum

for y being object st y in Ob C2 holds

y in rng (F | (Ob C1))

proof

then A25:
Ob C2 c= rng (F | (Ob C1))
by TARSKI:def 3;
let y be object ; :: thesis: ( y in Ob C2 implies y in rng (F | (Ob C1)) )

assume A16: y in Ob C2 ; :: thesis: y in rng (F | (Ob C1))

set x = G . y;

A17: G * F = id C2 by A6, CAT_6:def 27;

A18: y in Mor C2 by A16;

then A19: y in the carrier of C2 by CAT_6:def 1;

y in dom (id the carrier of C2) by A18, CAT_6:def 1;

then A20: y in dom (G * F) by A17, STRUCT_0:def 4;

then A21: G . y in dom F by FUNCT_1:11;

A22: F . (G . y) = (G * F) . y by A20, FUNCT_1:12

.= (id C2) . y by A6, CAT_6:def 27

.= (id the carrier of C2) . y by STRUCT_0:def 4

.= y by A19, FUNCT_1:18 ;

y in { g where g is morphism of C2 : ( g is identity & g in Mor C2 ) } by A16, CAT_6:def 17;

then consider g being morphism of C2 such that

A23: ( y = g & g is identity & g in Mor C2 ) ;

A24: G . y = G . g by A23, A4, A1, Th15, CAT_6:def 21;

G . g is identity by A23, CAT_6:def 22, A6, CAT_6:def 25;

then G . g in { f where f is morphism of C1 : ( f is identity & f in Mor C1 ) } by A4;

then G . y in Ob C1 by A24, CAT_6:def 17;

hence y in rng (F | (Ob C1)) by A21, A22, FUNCT_1:50; :: thesis: verum

end;assume A16: y in Ob C2 ; :: thesis: y in rng (F | (Ob C1))

set x = G . y;

A17: G * F = id C2 by A6, CAT_6:def 27;

A18: y in Mor C2 by A16;

then A19: y in the carrier of C2 by CAT_6:def 1;

y in dom (id the carrier of C2) by A18, CAT_6:def 1;

then A20: y in dom (G * F) by A17, STRUCT_0:def 4;

then A21: G . y in dom F by FUNCT_1:11;

A22: F . (G . y) = (G * F) . y by A20, FUNCT_1:12

.= (id C2) . y by A6, CAT_6:def 27

.= (id the carrier of C2) . y by STRUCT_0:def 4

.= y by A19, FUNCT_1:18 ;

y in { g where g is morphism of C2 : ( g is identity & g in Mor C2 ) } by A16, CAT_6:def 17;

then consider g being morphism of C2 such that

A23: ( y = g & g is identity & g in Mor C2 ) ;

A24: G . y = G . g by A23, A4, A1, Th15, CAT_6:def 21;

G . g is identity by A23, CAT_6:def 22, A6, CAT_6:def 25;

then G . g in { f where f is morphism of C1 : ( f is identity & f in Mor C1 ) } by A4;

then G . y in Ob C1 by A24, CAT_6:def 17;

hence y in rng (F | (Ob C1)) by A21, A22, FUNCT_1:50; :: thesis: verum

then A26: rng (F | (Ob C1)) = Ob C2 by A15, XBOOLE_0:def 10;

A27: rng (F | (Ob C1)) = (Ob C2) \/ (Ob C2) by A25, A15, XBOOLE_0:def 10

.= (Ob C2) \/ (rng (RelOb C2)) by Th34

.= (dom (RelOb C2)) \/ (rng (RelOb C2)) by Th34

.= field (RelOb C2) by RELAT_1:def 6 ;

A28: F | (Ob C1) is one-to-one by A7, FUNCT_1:52;

for a, b being object holds

( [a,b] in RelOb C1 iff ( a in field (RelOb C1) & b in field (RelOb C1) & [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 ) )

proof

hence
RelOb C1, RelOb C2 are_isomorphic
by A11, A27, A28, WELLORD1:def 7, WELLORD1:def 8; :: thesis: verum
let a, b be object ; :: thesis: ( [a,b] in RelOb C1 iff ( a in field (RelOb C1) & b in field (RelOb C1) & [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 ) )

assume [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 ; :: thesis: [a,b] in RelOb C1

then consider a2, b2 being Object of C2 such that

A36: ( [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] = [a2,b2] & ex g being morphism of C2 st g in Hom (a2,b2) ) ;

consider g being morphism of C2 such that

A37: g in Hom (a2,b2) by A36;

reconsider a1 = a, b1 = b as Object of C1 by A10, A35;

A38: F * G = id C1 by A6, CAT_6:def 27;

A39: a in Mor C1 by A10, A35;

then A40: a in the carrier of C1 by CAT_6:def 1;

a in dom (id the carrier of C1) by A39, CAT_6:def 1;

then A41: a in dom (F * G) by A38, STRUCT_0:def 4;

A42: G . a2 = G . ((F | (Ob C1)) . a) by A36, XTUPLE_0:1

.= G . (F . a) by A10, A35, FUNCT_1:49

.= (F * G) . a by A41, FUNCT_1:12

.= (id C1) . a by A6, CAT_6:def 27

.= (id the carrier of C1) . a by STRUCT_0:def 4

.= a1 by A40, FUNCT_1:18 ;

A43: b in Mor C1 by A10, A35;

then A44: b in the carrier of C1 by CAT_6:def 1;

b in dom (id the carrier of C1) by A43, CAT_6:def 1;

then A45: b in dom (F * G) by A38, STRUCT_0:def 4;

A46: G . b2 = G . ((F | (Ob C1)) . b) by A36, XTUPLE_0:1

.= G . (F . b) by A10, A35, FUNCT_1:49

.= (F * G) . b by A45, FUNCT_1:12

.= (id C1) . b by A6, CAT_6:def 27

.= (id the carrier of C1) . b by STRUCT_0:def 4

.= b1 by A44, FUNCT_1:18 ;

( G . (dom g) = G . a2 & G . (cod g) = G . b2 ) by A37, A5, Th20;

then ( dom (G . g) = G . a2 & cod (G . g) = G . b2 ) by A4, A5, A6, CAT_6:32;

then G . g in Hom (a1,b1) by A42, A46, A4, Th20;

hence [a,b] in RelOb C1 ; :: thesis: verum

end;hereby :: thesis: ( a in field (RelOb C1) & b in field (RelOb C1) & [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 implies [a,b] in RelOb C1 )

assume A35:
( a in field (RelOb C1) & b in field (RelOb C1) )
; :: thesis: ( not [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 or [a,b] in RelOb C1 )assume
[a,b] in RelOb C1
; :: thesis: ( a in field (RelOb C1) & b in field (RelOb C1) & [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 )

then consider a1, b1 being Object of C1 such that

A29: ( [a,b] = [a1,b1] & ex f being morphism of C1 st f in Hom (a1,b1) ) ;

consider f being morphism of C1 such that

A30: f in Hom (a1,b1) by A29;

A31: ( a = a1 & b = b1 ) by A29, XTUPLE_0:1;

not Ob C1 is empty by A4;

then A32: ( a1 in Ob C1 & b1 in Ob C1 ) ;

hence ( a in field (RelOb C1) & b in field (RelOb C1) ) by A10, A29, XTUPLE_0:1; :: thesis: [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2

A33: (F | (Ob C1)) . a = F . a1 by A31, A4, FUNCT_1:49;

A34: (F | (Ob C1)) . b = F . b1 by A31, A4, FUNCT_1:49;

( a in dom (F | (Ob C1)) & b in dom (F | (Ob C1)) ) by A9, A29, XTUPLE_0:1, A32;

then reconsider a2 = (F | (Ob C1)) . a, b2 = (F | (Ob C1)) . b as Object of C2 by A26, FUNCT_1:3;

( dom f = a1 & cod f = b1 ) by A30, A4, Th20;

then ( dom (F . f) = F . a1 & cod (F . f) = F . b1 ) by A4, A5, A6, CAT_6:32;

then F . f in Hom (a2,b2) by A33, A34, A5, Th20;

hence [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 ; :: thesis: verum

end;then consider a1, b1 being Object of C1 such that

A29: ( [a,b] = [a1,b1] & ex f being morphism of C1 st f in Hom (a1,b1) ) ;

consider f being morphism of C1 such that

A30: f in Hom (a1,b1) by A29;

A31: ( a = a1 & b = b1 ) by A29, XTUPLE_0:1;

not Ob C1 is empty by A4;

then A32: ( a1 in Ob C1 & b1 in Ob C1 ) ;

hence ( a in field (RelOb C1) & b in field (RelOb C1) ) by A10, A29, XTUPLE_0:1; :: thesis: [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2

A33: (F | (Ob C1)) . a = F . a1 by A31, A4, FUNCT_1:49;

A34: (F | (Ob C1)) . b = F . b1 by A31, A4, FUNCT_1:49;

( a in dom (F | (Ob C1)) & b in dom (F | (Ob C1)) ) by A9, A29, XTUPLE_0:1, A32;

then reconsider a2 = (F | (Ob C1)) . a, b2 = (F | (Ob C1)) . b as Object of C2 by A26, FUNCT_1:3;

( dom f = a1 & cod f = b1 ) by A30, A4, Th20;

then ( dom (F . f) = F . a1 & cod (F . f) = F . b1 ) by A4, A5, A6, CAT_6:32;

then F . f in Hom (a2,b2) by A33, A34, A5, Th20;

hence [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 ; :: thesis: verum

assume [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 ; :: thesis: [a,b] in RelOb C1

then consider a2, b2 being Object of C2 such that

A36: ( [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] = [a2,b2] & ex g being morphism of C2 st g in Hom (a2,b2) ) ;

consider g being morphism of C2 such that

A37: g in Hom (a2,b2) by A36;

reconsider a1 = a, b1 = b as Object of C1 by A10, A35;

A38: F * G = id C1 by A6, CAT_6:def 27;

A39: a in Mor C1 by A10, A35;

then A40: a in the carrier of C1 by CAT_6:def 1;

a in dom (id the carrier of C1) by A39, CAT_6:def 1;

then A41: a in dom (F * G) by A38, STRUCT_0:def 4;

A42: G . a2 = G . ((F | (Ob C1)) . a) by A36, XTUPLE_0:1

.= G . (F . a) by A10, A35, FUNCT_1:49

.= (F * G) . a by A41, FUNCT_1:12

.= (id C1) . a by A6, CAT_6:def 27

.= (id the carrier of C1) . a by STRUCT_0:def 4

.= a1 by A40, FUNCT_1:18 ;

A43: b in Mor C1 by A10, A35;

then A44: b in the carrier of C1 by CAT_6:def 1;

b in dom (id the carrier of C1) by A43, CAT_6:def 1;

then A45: b in dom (F * G) by A38, STRUCT_0:def 4;

A46: G . b2 = G . ((F | (Ob C1)) . b) by A36, XTUPLE_0:1

.= G . (F . b) by A10, A35, FUNCT_1:49

.= (F * G) . b by A45, FUNCT_1:12

.= (id C1) . b by A6, CAT_6:def 27

.= (id the carrier of C1) . b by STRUCT_0:def 4

.= b1 by A44, FUNCT_1:18 ;

( G . (dom g) = G . a2 & G . (cod g) = G . b2 ) by A37, A5, Th20;

then ( dom (G . g) = G . a2 & cod (G . g) = G . b2 ) by A4, A5, A6, CAT_6:32;

then G . g in Hom (a1,b1) by A42, A46, A4, Th20;

hence [a,b] in RelOb C1 ; :: thesis: verum