let S, R be non empty RelStr ; ( 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
; card the InternalRel of S = card the InternalRel of R
then consider f being Function of S,R such that
A1:
f is isomorphic
by WAYBEL_1:def 8;
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
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
proof
let a be
set ;
TARSKI:def 3 ( not a in rng ([:f,f:] | C) or a in the InternalRel of R )
assume
a in rng ([:f,f:] | C)
;
a in the InternalRel of R
then consider x being
set 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
set such that A10:
x = [x1,x2]
by A8, RELAT_1:def 1;
B:
x in dom [:f,f:]
by A8, RELAT_1:57;
then reconsider X1 =
x1,
X2 =
x2 as
Element of
S by A8, A10, ZFMISC_1:87;
X1 <= X2
by A6, A8, A10, ORDERS_2:def 5;
then A11:
f . X1 <= f . X2
by A5, ORDERS_3:def 5;
A12:
a = [:f,f:] . (
x1,
x2)
by A8, A9, A10, FUNCT_1:47;
(
x1 in dom f &
x2 in dom f )
by A3, A8, A10, ZFMISC_1:87, B;
then
a = [(f . x1),(f . x2)]
by A12, FUNCT_3:def 8;
hence
a in the
InternalRel of
R
by A11, ORDERS_2:def 5;
verum
end;
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;
reconsider F =
F as
Function of
(dom ([:f,f:] | C)), the
InternalRel of
R by A7, FUNCT_2:6;
A13:
rng F = the
InternalRel of
R
proof
thus
rng F c= the
InternalRel of
R
by A7;
XBOOLE_0:def 10 the InternalRel of R c= rng F
let x be
set ;
TARSKI:def 3 ( not x in the InternalRel of R or x in rng F )
assume A14:
x in the
InternalRel of
R
;
x in rng F
then consider x1,
x2 being
set such that A15:
x = [x1,x2]
by RELAT_1:def 1;
reconsider x19 =
x1,
x29 =
x2 as
Element of the
carrier of
R by A14, A15, ZFMISC_1:87;
x1 in the
carrier of
R
by A14, A15, ZFMISC_1:87;
then consider X1 being
set such that A16:
X1 in dom f
and A17:
x1 = f . X1
by A4, FUNCT_1:def 3;
x2 in the
carrier of
R
by A14, A15, ZFMISC_1:87;
then consider X2 being
set such that A18:
X2 in dom f
and A19:
x2 = f . X2
by A4, FUNCT_1:def 3;
reconsider X19 =
X1,
X29 =
X2 as
Element of
S by A16, A18;
x19 <= x29
by A14, A15, ORDERS_2:def 5;
then
X19 <= X29
by A1, A17, A19, WAYBEL_0:66;
then A20:
[X1,X2] in C
by ORDERS_2:def 5;
set Pi =
[X1,X2];
[X1,X2] in [:(dom f),(dom f):]
by A16, A18, ZFMISC_1:87;
then x =
[:f,f:] . (
X1,
X2)
by A15, A17, A19, FUNCT_3:65
.=
F . [X1,X2]
by A6, A20, FUNCT_1:47
;
hence
x in rng F
by A6, A20, FUNCT_1:def 3;
verum
end;
F is
one-to-one
by A2, FUNCT_1:52;
hence
the
InternalRel of
S, the
InternalRel of
R are_equipotent
by A6, A13, WELLORD2:def 4;
verum
end;
hence
card the InternalRel of S = card the InternalRel of R
by CARD_1:5; verum