let R be Relation; card R = card (R ~)
defpred S1[ object , object ] means for x, y being object st [x,y] = $1 holds
[y,x] = $2;
A1:
for x being object st x in R holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in R implies ex y being object st S1[x,y] )
assume
x in R
;
ex y being object st S1[x,y]
then consider y,
z being
object such that A2:
[y,z] = x
by RELAT_1:def 1;
take zy =
[z,y];
S1[x,zy]
let w,
t be
object ;
( [w,t] = x implies [t,w] = zy )
assume A3:
[w,t] = x
;
[t,w] = zy
then
w = y
by A2, XTUPLE_0:1;
hence
[t,w] = zy
by A3, A2, XTUPLE_0:1;
verum
end;
consider h being Function such that
A4:
( dom h = R & ( for x being object st x in R holds
S1[x,h . x] ) )
from CLASSES1:sch 1(A1);
A5:
h is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom h or not x2 in dom h or not h . x1 = h . x2 or x1 = x2 )
assume that A6:
x1 in dom h
and A7:
x2 in dom h
and A8:
h . x1 = h . x2
;
x1 = x2
consider y2,
z2 being
object such that A9:
x2 = [y2,z2]
by A4, A7, RELAT_1:def 1;
A10:
h . x2 = [z2,y2]
by A7, A9, A4;
consider y1,
z1 being
object such that A11:
x1 = [y1,z1]
by A6, A4, RELAT_1:def 1;
A12:
h . x1 = [z1,y1]
by A11, A6, A4;
then
z1 = z2
by A10, A8, XTUPLE_0:1;
hence
x1 = x2
by A12, A10, A8, XTUPLE_0:1, A11, A9;
verum
end;
A13:
rng h c= R ~
proof
let y be
object ;
TARSKI:def 3 ( not y in rng h or y in R ~ )
assume
y in rng h
;
y in R ~
then consider x being
object such that A14:
x in dom h
and A15:
h . x = y
by FUNCT_1:def 3;
consider t,
r being
object such that A16:
x = [t,r]
by A4, A14, RELAT_1:def 1;
h . x = [r,t]
by A14, A16, A4;
hence
y in R ~
by A14, A16, A4, RELAT_1:def 7, A15;
verum
end;
R ~ c= rng h
proof
let y,
z be
object ;
RELAT_1:def 3 ( not [y,z] in R ~ or [y,z] in rng h )
assume
[y,z] in R ~
;
[y,z] in rng h
then A17:
[z,y] in R
by RELAT_1:def 7;
then
h . [z,y] = [y,z]
by A4;
hence
[y,z] in rng h
by A17, A4, FUNCT_1:def 3;
verum
end;
then
rng h = R ~
by A13;
hence
card R = card (R ~)
by A5, WELLORD2:def 4, A4, CARD_1:5; verum