let S, R be non empty RelStr ; :: thesis: ( S,R are_isomorphic implies card the InternalRel of S = card the InternalRel of R )
set A = the carrier of S;
set B = the carrier of R;
set C = the InternalRel of S;
set D = the InternalRel of R;
reconsider C = the InternalRel of S as set ;
assume S,R are_isomorphic ; :: thesis: card the InternalRel of S = card the InternalRel of R
then consider f being Function of S,R such that
A1: f is isomorphic ;
reconsider f9 = f as one-to-one Function by ;
A2: [:f9,f9:] is one-to-one ;
A3: dom f = the carrier of S by FUNCT_2:def 1;
A4: rng f = the carrier of R by ;
A5: f is monotone by ;
the InternalRel of S, the InternalRel of R are_equipotent
proof
set P = [:f,f:];
set F = [:f,f:] | C;
set L = dom ([:f,f:] | C);
A6: dom ([:f,f:] | C) = (dom [:f,f:]) /\ C by RELAT_1:61
.= [:(dom f),(dom f):] /\ C by FUNCT_3:def 8
.= C by ;
A7: rng ([:f,f:] | C) c= the InternalRel of R
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng ([:f,f:] | C) or a in the InternalRel of R )
assume a in rng ([:f,f:] | C) ; :: thesis: a in the InternalRel of R
then consider x being object such that
A8: x in dom ([:f,f:] | C) and
A9: a = ([:f,f:] | C) . x by FUNCT_1:def 3;
consider x1, x2 being object such that
A10: x = [x1,x2] by ;
A11: x in dom [:f,f:] by ;
then reconsider X1 = x1, X2 = x2 as Element of S by ;
X1 <= X2 by ;
then A12: f . X1 <= f . X2 by A5;
A13: a = [:f,f:] . (x1,x2) by ;
( x1 in dom f & x2 in dom f ) by ;
then a = [(f . x1),(f . x2)] by ;
hence a in the InternalRel of R by ; :: thesis: verum
end;
then reconsider F = [:f,f:] | C as Function of (dom ([:f,f:] | C)),[: the carrier of R, the carrier of R:] by ;
reconsider F = F as Function of (dom ([:f,f:] | C)), the InternalRel of R by ;
A14: rng F = the InternalRel of R
proof
thus rng F c= the InternalRel of R by A7; :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of R c= rng F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of R or x in rng F )
assume A15: x in the InternalRel of R ; :: thesis: x in rng F
then consider x1, x2 being object such that
A16: x = [x1,x2] by RELAT_1:def 1;
reconsider x19 = x1, x29 = x2 as Element of the carrier of R by ;
x1 in the carrier of R by ;
then consider X1 being object such that
A17: X1 in dom f and
A18: x1 = f . X1 by ;
x2 in the carrier of R by ;
then consider X2 being object such that
A19: X2 in dom f and
A20: x2 = f . X2 by ;
reconsider X19 = X1, X29 = X2 as Element of S by ;
x19 <= x29 by ;
then X19 <= X29 by ;
then A21: [X1,X2] in C by ORDERS_2:def 5;
set Pi = [X1,X2];
[X1,X2] in [:(dom f),(dom f):] by ;
then x = [:f,f:] . (X1,X2) by
.= F . [X1,X2] by ;
hence x in rng F by ; :: thesis: verum
end;
F is one-to-one by ;
hence the InternalRel of S, the InternalRel of R are_equipotent by ; :: thesis: verum
end;
hence card the InternalRel of S = card the InternalRel of R by CARD_1:5; :: thesis: verum