let O1, O2 be ordinal number ; :: thesis: for C1 being preorder O1 -ordered category
for C2 being preorder O2 -ordered category holds
( O1 = O2 iff C1 ~= C2 )
let C1 be preorder O1 -ordered category; :: thesis: for C2 being preorder O2 -ordered category holds
( O1 = O2 iff C1 ~= C2 )
let C2 be preorder O2 -ordered category; :: thesis: ( O1 = O2 iff C1 ~= C2 )
thus ( O1 = O2 implies C1 ~= C2 ) :: thesis: ( C1 ~= C2 implies O1 = O2 )

proof

assume A1: O1 = O2 ; :: thesis: C1 ~= C2

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

suppose O1 is empty ; :: thesis: C1 ~= C2

hence C1 ~= C2 by A1, Th13; :: thesis: verum

end;

suppose A2: not O1 is empty ; :: thesis: C1 ~= C2

then reconsider D1 = C1, D2 = C2 as non empty category by A1;
consider F1 being Function such that
A3: F1 is_isomorphism_of RelOb C1, RelIncl O1 by Def14, WELLORD1:def 8;
consider F2 being Function such that
A4: F2 is_isomorphism_of RelOb C2, RelIncl O2 by Def14, WELLORD1:def 8;
A5: F2 " is_isomorphism_of RelIncl O2, RelOb C2 by A4, WELLORD1:39;
set F3 = (F2 ") * F1;
A6: (F2 ") * F1 is_isomorphism_of RelOb C1, RelOb C2 by A1, A3, A5, WELLORD1:41;
consider F4 being Function of C1,(RelOb C1) such that
A7: ( F4 is bijective & ( for f being morphism of C1 holds F4 . f = [(dom f),(cod f)] ) ) by A2, Th36;
consider F5 being Function of C2,(RelOb C2) such that
A8: ( F5 is bijective & ( for f being morphism of C2 holds F5 . f = [(dom f),(cod f)] ) ) by A1, A2, Th36;
A9: ( dom ((F2 ") * F1) = field (RelOb C1) & rng ((F2 ") * F1) = field (RelOb C2) & (F2 ") * F1 is one-to-one & ( for a, b being set holds
( [a,b] in RelOb C1 iff ( a in field (RelOb C1) & b in field (RelOb C1) & [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] in RelOb C2 ) ) ) ) by A6, WELLORD1:def 7;
A10: field (RelOb C1) = (dom (RelOb C1)) \/ (rng (RelOb C1)) by RELAT_1:def 6
.= (dom (RelOb C1)) \/ (Ob C1) by Th34
.= (Ob C1) \/ (Ob C1) by Th34
.= Ob C1 ;
defpred S₁[ object , object ] means for a, b being set st $1 = [a,b] holds
$2 = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)];
A11: for x being Element of RelOb D1 ex y being Element of RelOb D2 st S₁[x,y]

proof

let x be Element of RelOb D1; :: thesis: ex y being Element of RelOb D2 st S₁[x,y]
x in RelOb D1 ;
then consider o1, o2 being Object of D1 such that
A12: ( x = [o1,o2] & ex f being morphism of D1 st f in Hom (o1,o2) ) ;
reconsider y = [(((F2 ") * F1) . o1),(((F2 ") * F1) . o2)] as Element of RelOb D2 by A12, A6, WELLORD1:def 7;
take y ; :: thesis: S₁[x,y]
for a, b being set st x = [a,b] holds
y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)]

proof

let a, b be set ; :: thesis: ( x = [a,b] implies y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] )
assume x = [a,b] ; :: thesis: y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)]
then ( a = o1 & b = o2 ) by A12, XTUPLE_0:1;
hence y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] ; :: thesis: verum

end;

hence S₁[x,y] ; :: thesis: verum

end;

consider F33 being Function of (RelOb D1),(RelOb D2) such that
A13: for x being Element of RelOb D1 holds S₁[x,F33 . x] from FUNCT_2:sch 3(A11);
A14: ( rng F5 = dom (F5 ") & dom F5 = rng (F5 ") ) by A8, FUNCT_1:33;
set F = ((F5 ") * F33) * F4;
rng F33 c= RelOb C2 ;
then rng F33 c= rng F5 by A8, FUNCT_2:def 3;
then A15: dom ((F5 ") * F33) = dom F33 by A14, RELAT_1:27;
RelOb C1 c= dom F33 by FUNCT_2:def 1;
then rng F4 c= dom F33 by XBOOLE_1:1;
then A16: dom (((F5 ") * F33) * F4) = dom F4 by A15, RELAT_1:27;
then A17: dom (((F5 ") * F33) * F4) = the carrier of C1 by FUNCT_2:def 1;
for y being object st y in RelOb C2 holds
y in rng F33

proof

let y be object ; :: thesis: ( y in RelOb C2 implies y in rng F33 )
assume y in RelOb C2 ; :: thesis: y in rng F33
then consider o1, o2 being Object of C2 such that
A18: ( y = [o1,o2] & ex g being morphism of C2 st g in Hom (o1,o2) ) ;
A19: rng ((F2 ") * F1) = (dom (RelOb C2)) \/ (rng (RelOb C2)) by A9, RELAT_1:def 6
.= (dom (RelOb C2)) \/ (Ob C2) by Th34
.= (Ob C2) \/ (Ob C2) by Th34
.= Ob D2 ;
consider x1 being object such that
A20: ( x1 in dom ((F2 ") * F1) & o1 = ((F2 ") * F1) . x1 ) by A19, FUNCT_1:def 3;
consider x2 being object such that
A21: ( x2 in dom ((F2 ") * F1) & o2 = ((F2 ") * F1) . x2 ) by A19, FUNCT_1:def 3;
reconsider x1 = x1, x2 = x2 as set by A20, A21;
set x = [x1,x2];
A22: ( x1 in field (RelOb C1) & x2 in field (RelOb C1) ) by A20, A21, A6, WELLORD1:def 7;
[(((F2 ") * F1) . x1),(((F2 ") * F1) . x2)] in RelOb C2 by A18, A20, A21;
then reconsider x = [x1,x2] as Element of RelOb D1 by A22, A6, WELLORD1:def 7;
A23: dom F33 = RelOb D1 by FUNCT_2:def 1;
F33 . x = [(((F2 ") * F1) . x1),(((F2 ") * F1) . x2)] by A13;
hence y in rng F33 by A23, A18, A20, A21, FUNCT_1:def 3; :: thesis: verum

end;

then RelOb C2 c= rng F33 by TARSKI:def 3;
then rng F5 c= rng F33 by A8, FUNCT_2:def 3;
then rng ((F5 ") * F33) = rng (F5 ") by A14, RELAT_1:28;
then A24: rng ((F5 ") * F33) = the carrier of C2 by A14, FUNCT_2:def 1;
dom F33 c= RelOb C1 ;
then dom F33 c= rng F4 by A7, FUNCT_2:def 3;
then A25: rng (((F5 ") * F33) * F4) = the carrier of C2 by A24, A15, RELAT_1:28;
then reconsider F = ((F5 ") * F33) * F4 as Functor of C1,C2 by A17, FUNCT_2:1;
for x1, x2 being object st x1 in dom F33 & x2 in dom F33 & F33 . x1 = F33 . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom F33 & x2 in dom F33 & F33 . x1 = F33 . x2 implies x1 = x2 )
assume x1 in dom F33 ; :: thesis: ( not x2 in dom F33 or not F33 . x1 = F33 . x2 or x1 = x2 )
then x1 in RelOb D1 ;
then consider o11, o12 being Object of D1 such that
A26: ( x1 = [o11,o12] & ex f1 being morphism of D1 st f1 in Hom (o11,o12) ) ;
A27: [o11,o12] in RelOb C1 by A26;
reconsider x11 = x1 as Element of RelOb D1 by A26, A27;
assume x2 in dom F33 ; :: thesis: ( not F33 . x1 = F33 . x2 or x1 = x2 )
then x2 in RelOb D1 ;
then consider o21, o22 being Object of D1 such that
A28: ( x2 = [o21,o22] & ex f1 being morphism of D1 st f1 in Hom (o21,o22) ) ;
A29: [o21,o22] in RelOb C1 by A28;
reconsider x22 = x2 as Element of RelOb D1 by A28, A29;
assume A30: F33 . x1 = F33 . x2 ; :: thesis: x1 = x2
( F33 . x11 = [(((F2 ") * F1) . o11),(((F2 ") * F1) . o12)] & F33 . x22 = [(((F2 ") * F1) . o21),(((F2 ") * F1) . o22)] ) by A13, A26, A28;
then ( ((F2 ") * F1) . o11 = ((F2 ") * F1) . o21 & ((F2 ") * F1) . o12 = ((F2 ") * F1) . o22 ) by A30, XTUPLE_0:1;
then ( o11 = o21 & o12 = o22 ) by A10, A9, FUNCT_1:def 4;
hence x1 = x2 by A26, A28; :: thesis: verum

end;

then A31: F33 is one-to-one by FUNCT_1:def 4;
A32: F is onto by A25, FUNCT_2:def 3;
A33: for f being morphism of C1 holds
( dom (F . f) = ((F2 ") * F1) . (dom f) & cod (F . f) = ((F2 ") * F1) . (cod f) )

proof

let f be morphism of C1; :: thesis: ( dom (F . f) = ((F2 ") * F1) . (dom f) & cod (F . f) = ((F2 ") * F1) . (cod f) )
reconsider x = f as object ;
x in Mor C1 by A2, SUBSET_1:def 1;
then A34: x in dom F4 by A17, A16, CAT_6:def 1;
f in Hom ((dom f),(cod f)) by A2, Th20;
then A35: [(dom f),(cod f)] in RelOb D1 ;
then A36: [(dom f),(cod f)] in dom F33 by FUNCT_2:def 1;
reconsider x1 = [(dom f),(cod f)] as Element of RelOb D1 by A35;
A37: for a, b being set st x1 = [a,b] holds
F33 . x1 = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] by A13;
[(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] in RelOb C2 by A35, A6, WELLORD1:def 7;
then A38: [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] in rng F5 by A8, FUNCT_2:def 3;
A39: F . f = (((F5 ") * F33) * F4) . x by CAT_6:def 21
.= ((F5 ") * F33) . (F4 . x) by A34, FUNCT_1:13
.= ((F5 ") * F33) . [(dom f),(cod f)] by A7
.= (F5 ") . (F33 . [(dom f),(cod f)]) by A36, FUNCT_1:13
.= (F5 ") . [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] by A37 ;
[(dom (F . f)),(cod (F . f))] = F5 . ((F5 ") . [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))]) by A8, A39
.= [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] by A8, A38, FUNCT_1:35 ;
hence ( dom (F . f) = ((F2 ") * F1) . (dom f) & cod (F . f) = ((F2 ") * F1) . (cod f) ) by XTUPLE_0:1; :: thesis: verum

end;

for f1, f2 being morphism of C1 st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )

proof

let f1, f2 be morphism of C1; :: thesis: ( f1 |> f2 implies ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) )
assume A40: f1 |> f2 ; :: thesis: ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
dom (F . f1) = ((F2 ") * F1) . (dom f1) by A33
.= ((F2 ") * F1) . (cod f2) by A2, A40, Th5
.= cod (F . f2) by A33 ;
hence A41: F . f1 |> F . f2 by Th5; :: thesis: F . (f1 (*) f2) = (F . f1) (*) (F . f2)
set g1 = F . (f1 (*) f2);
set g2 = (F . f1) (*) (F . f2);
A42: dom (F . (f1 (*) f2)) = ((F2 ") * F1) . (dom (f1 (*) f2)) by A33
.= ((F2 ") * F1) . (dom f2) by A40, Th4
.= dom (F . f2) by A33
.= dom ((F . f1) (*) (F . f2)) by A41, Th4 ;
A43: cod (F . (f1 (*) f2)) = ((F2 ") * F1) . (cod (f1 (*) f2)) by A33
.= ((F2 ") * F1) . (cod f1) by A40, Th4
.= cod (F . f1) by A33
.= cod ((F . f1) (*) (F . f2)) by A41, Th4 ;
A44: F . (f1 (*) f2) in Hom ((dom (F . (f1 (*) f2))),(cod (F . (f1 (*) f2)))) by Th20;
(F . f1) (*) (F . f2) in Hom ((dom (F . (f1 (*) f2))),(cod (F . (f1 (*) f2)))) by A42, A43, Th20;
hence F . (f1 (*) f2) = (F . f1) (*) (F . f2) by A44, Def12; :: thesis: verum

end;

then A45: F is multiplicative by CAT_6:def 23;
for f being morphism of C1 st f is identity holds
F . f is identity

proof

let f be morphism of C1; :: thesis: ( f is identity implies F . f is identity )
assume A46: f is identity ; :: thesis: F . f is identity
then A47: dom f = f by Th6
.= cod f by A46, Th6 ;
A48: for g1 being morphism of C2 st F . f |> g1 holds
(F . f) (*) g1 = g1

proof

let g1 be morphism of C2; :: thesis: ( F . f |> g1 implies (F . f) (*) g1 = g1 )
assume A49: F . f |> g1 ; :: thesis: (F . f) (*) g1 = g1
set g2 = (F . f) (*) g1;
A50: dom ((F . f) (*) g1) = dom g1 by A49, Th4;
A51: cod ((F . f) (*) g1) = cod (F . f) by A49, Th4
.= ((F2 ") * F1) . (dom f) by A33, A47
.= dom (F . f) by A33
.= cod g1 by A49, Th5 ;
A52: g1 in Hom ((dom g1),(cod g1)) by A1, A2, Th20;
(F . f) (*) g1 in Hom ((dom g1),(cod g1)) by A50, A51, Th20;
hence (F . f) (*) g1 = g1 by A52, Def12; :: thesis: verum

end;

then F . f is left_identity by CAT_6:def 4;
then F . f is right_identity by CAT_6:9;
hence F . f is identity by A48, CAT_6:def 4, CAT_6:def 14; :: thesis: verum

end;

then F is identity-preserving by CAT_6:def 22;
hence C1 ~= C2 by A32, Th12, A45, CAT_6:def 25, A8, A7, A31; :: thesis: verum

end;

end;

end;

thus ( C1 ~= C2 implies O1 = O2 ) :: thesis: verum

proof

assume C1 ~= C2 ; :: thesis: O1 = O2
then A53: RelOb C1, RelOb C2 are_isomorphic by Th35;
A54: RelOb C1, RelIncl O1 are_isomorphic by Def14;
RelOb C2, RelIncl O2 are_isomorphic by Def14;
then RelOb C1, RelIncl O2 are_isomorphic by A53, WELLORD1:42;
then RelIncl O2, RelOb C1 are_isomorphic by WELLORD1:40;
hence O1 = O2 by A54, WELLORD1:42, WELLORD2:10; :: thesis: verum

end;