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
by WAYBEL_1:def 8;
A2:
f is monotone
by A1, WAYBEL_0:def 38;
reconsider f' = f as one-to-one Function by A1, WAYBEL_0:def 38;
A3:
[:f',f':] is one-to-one
;
A4:
dom f = the carrier of S
by FUNCT_2:def 1;
A5:
rng f = the carrier of R
by A1, WAYBEL_0:66;
the InternalRel of S,the InternalRel of R are_equipotent
proof
set F =
[:f,f:] | C;
set L =
dom ([:f,f:] | C);
set P =
[:f,f:];
A6:
dom ([:f,f:] | C) =
(dom [:f,f:]) /\ C
by RELAT_1:90
.=
[:(dom f),(dom f):] /\ C
by FUNCT_3:def 9
.=
C
by A4, XBOOLE_1:28
;
A7:
rng ([:f,f:] | C) c= the
InternalRel of
R
proof
let a be
set ;
:: 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
set such that A8:
x in dom ([:f,f:] | C)
and A9:
a = ([:f,f:] | C) . x
by FUNCT_1:def 5;
consider x1,
x2 being
set such that A10:
x = [x1,x2]
by A8, RELAT_1:def 1;
A11:
(
x1 in dom f &
x2 in dom f )
by A4, A8, A10, ZFMISC_1:106;
a = [:f,f:] . x1,
x2
by A8, A9, A10, FUNCT_1:70;
then A12:
a = [(f . x1),(f . x2)]
by A11, FUNCT_3:def 9;
reconsider X1 =
x1,
X2 =
x2 as
Element of
S by A8, A10, ZFMISC_1:106;
X1 <= X2
by A6, A8, A10, ORDERS_2:def 9;
then
f . X1 <= f . X2
by A2, ORDERS_3:def 5;
hence
a in the
InternalRel of
R
by A12, ORDERS_2:def 9;
:: 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 FUNCT_2:4, XBOOLE_1:1;
reconsider F =
F as
Function of
(dom ([:f,f:] | C)),the
InternalRel of
R by A7, FUNCT_2:8;
A13:
F is
one-to-one
by A3, FUNCT_1:84;
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
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of R or x in rng F )
assume A14:
x in the
InternalRel of
R
;
:: thesis: x in rng F
then consider x1,
x2 being
set such that A15:
x = [x1,x2]
by RELAT_1:def 1;
A16:
(
x1 in the
carrier of
R &
x2 in the
carrier of
R )
by A14, A15, ZFMISC_1:106;
reconsider x1' =
x1,
x2' =
x2 as
Element of the
carrier of
R by A14, A15, ZFMISC_1:106;
A17:
x1' <= x2'
by A14, A15, ORDERS_2:def 9;
consider X1 being
set such that A18:
X1 in dom f
and A19:
x1 = f . X1
by A5, A16, FUNCT_1:def 5;
consider X2 being
set such that A20:
X2 in dom f
and A21:
x2 = f . X2
by A5, A16, FUNCT_1:def 5;
reconsider X1' =
X1,
X2' =
X2 as
Element of
S by A18, A20;
X1' <= X2'
by A1, A17, A19, A21, WAYBEL_0:66;
then A22:
[X1,X2] in C
by ORDERS_2:def 9;
set Pi =
[X1,X2];
[X1,X2] in [:(dom f),(dom f):]
by A18, A20, ZFMISC_1:106;
then x =
[:f,f:] . X1,
X2
by A15, A19, A21, FUNCT_3:86
.=
F . [X1,X2]
by A6, A22, FUNCT_1:70
;
hence
x in rng F
by A6, A22, FUNCT_1:def 5;
:: thesis: verum
end;
hence
the
InternalRel of
S,the
InternalRel of
R are_equipotent
by A6, A13, WELLORD2:def 4;
:: thesis: verum
end;
hence
card the InternalRel of S = card the InternalRel of R
by CARD_1:21; :: thesis: verum