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 A1, WAYBEL_0:def 38;

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 A1, WAYBEL_0:66;

A5: f is monotone by A1, WAYBEL_0:def 38;

the InternalRel of S, the InternalRel of R are_equipotent

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 A1, WAYBEL_0:def 38;

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 A1, WAYBEL_0:66;

A5: f is monotone by A1, WAYBEL_0:def 38;

the InternalRel of S, the InternalRel of R are_equipotent

proof

hence
card the InternalRel of S = card the InternalRel of R
by CARD_1:5; :: thesis: verum
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 A3, XBOOLE_1:28 ;

A7: rng ([:f,f:] | C) c= the InternalRel of R

reconsider F = F as Function of (dom ([:f,f:] | C)), the InternalRel of R by A7, FUNCT_2:6;

A14: rng F = the InternalRel of R

hence the InternalRel of S, the InternalRel of R are_equipotent by A6, A14, WELLORD2:def 4; :: thesis: verum

end;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 A3, XBOOLE_1:28 ;

A7: rng ([:f,f:] | C) c= the InternalRel of R

proof

then reconsider F = [:f,f:] | C as Function of (dom ([:f,f:] | C)),[: the carrier of R, the carrier of R:] by FUNCT_2:2, XBOOLE_1:1;
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 A8, RELAT_1:def 1;

A11: x in dom [:f,f:] by A8, RELAT_1:57;

then reconsider X1 = x1, X2 = x2 as Element of S by A10, ZFMISC_1:87;

X1 <= X2 by A8, A10, ORDERS_2:def 5;

then A12: f . X1 <= f . X2 by A5;

A13: a = [:f,f:] . (x1,x2) by A8, A9, A10, FUNCT_1:47;

( x1 in dom f & x2 in dom f ) by A3, A10, A11, ZFMISC_1:87;

then a = [(f . x1),(f . x2)] by A13, FUNCT_3:def 8;

hence a in the InternalRel of R by A12, ORDERS_2:def 5; :: thesis: verum

end;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 A8, RELAT_1:def 1;

A11: x in dom [:f,f:] by A8, RELAT_1:57;

then reconsider X1 = x1, X2 = x2 as Element of S by A10, ZFMISC_1:87;

X1 <= X2 by A8, A10, ORDERS_2:def 5;

then A12: f . X1 <= f . X2 by A5;

A13: a = [:f,f:] . (x1,x2) by A8, A9, A10, FUNCT_1:47;

( x1 in dom f & x2 in dom f ) by A3, A10, A11, ZFMISC_1:87;

then a = [(f . x1),(f . x2)] by A13, FUNCT_3:def 8;

hence a in the InternalRel of R by A12, ORDERS_2:def 5; :: thesis: verum

reconsider F = F as Function of (dom ([:f,f:] | C)), the InternalRel of R by A7, FUNCT_2:6;

A14: rng F = the InternalRel of R

proof

F is one-to-one
by A2, FUNCT_1:52;
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 A15, A16, ZFMISC_1:87;

x1 in the carrier of R by A15, A16, ZFMISC_1:87;

then consider X1 being object such that

A17: X1 in dom f and

A18: x1 = f . X1 by A4, FUNCT_1:def 3;

x2 in the carrier of R by A15, A16, ZFMISC_1:87;

then consider X2 being object such that

A19: X2 in dom f and

A20: x2 = f . X2 by A4, FUNCT_1:def 3;

reconsider X19 = X1, X29 = X2 as Element of S by A17, A19;

x19 <= x29 by A15, A16, ORDERS_2:def 5;

then X19 <= X29 by A1, A18, A20, WAYBEL_0:66;

then A21: [X1,X2] in C by ORDERS_2:def 5;

set Pi = [X1,X2];

[X1,X2] in [:(dom f),(dom f):] by A17, A19, ZFMISC_1:87;

then x = [:f,f:] . (X1,X2) by A16, A18, A20, FUNCT_3:65

.= F . [X1,X2] by A6, A21, FUNCT_1:47 ;

hence x in rng F by A6, A21, FUNCT_1:def 3; :: thesis: verum

end;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 A15, A16, ZFMISC_1:87;

x1 in the carrier of R by A15, A16, ZFMISC_1:87;

then consider X1 being object such that

A17: X1 in dom f and

A18: x1 = f . X1 by A4, FUNCT_1:def 3;

x2 in the carrier of R by A15, A16, ZFMISC_1:87;

then consider X2 being object such that

A19: X2 in dom f and

A20: x2 = f . X2 by A4, FUNCT_1:def 3;

reconsider X19 = X1, X29 = X2 as Element of S by A17, A19;

x19 <= x29 by A15, A16, ORDERS_2:def 5;

then X19 <= X29 by A1, A18, A20, WAYBEL_0:66;

then A21: [X1,X2] in C by ORDERS_2:def 5;

set Pi = [X1,X2];

[X1,X2] in [:(dom f),(dom f):] by A17, A19, ZFMISC_1:87;

then x = [:f,f:] . (X1,X2) by A16, A18, A20, FUNCT_3:65

.= F . [X1,X2] by A6, A21, FUNCT_1:47 ;

hence x in rng F by A6, A21, FUNCT_1:def 3; :: thesis: verum

hence the InternalRel of S, the InternalRel of R are_equipotent by A6, A14, WELLORD2:def 4; :: thesis: verum