let X, Y be set ; :: thesis: ( card X c= card Y iff ex f being Function st
( dom f = Y & X c= rng f ) )
thus ( card X c= card Y implies ex f being Function st
( dom f = Y & X c= rng f ) ) :: thesis: ( ex f being Function st
( dom f = Y & X c= rng f ) implies card X c= card Y )
proof
assume card X c= card Y ; :: thesis: ex f being Function st
( dom f = Y & X c= rng f )
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f c= Y by Th9;
defpred S1[ object , object ] means ( ( $1 in rng f & $2 = (f ") . $1 ) or ( not $1 in rng f & $2 = 0 ) );
A4: for x being object st x in Y holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in Y implies ex y being object st S1[x,y] )
assume x in Y ; :: thesis: ex y being object st S1[x,y]
( not x in rng f implies ex y being object st S1[x,y] ) ;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
A5: for x, y, z being object st x in Y & S1[x,y] & S1[x,z] holds
y = z ;
consider g being Function such that
A6: ( dom g = Y & ( for y being object st y in Y holds
S1[y,g . y] ) ) from FUNCT_1:sch 2(A5, A4);
 take g ; :: thesis: ( dom g = Y & X c= rng g )
thus dom g = Y by A6; :: thesis: X c= rng g
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in rng g )
assume A7: x in X ; :: thesis: x in rng g
then A8: f . x in rng f by A2, FUNCT_1:def 3;
(f ") . (f . x) = x by A1, A2, A7, FUNCT_1:34;
then x = g . (f . x) by A3, A6, A8;
hence x in rng g by A3, A6, A8, FUNCT_1:def 3; :: thesis: verum
end;
given f being Function such that A9: dom f = Y and
A10: X c= rng f ; :: thesis: card X c= card Y
deffunc H1( object ) -> set = f " {$1};
consider g being Function such that
A11: ( dom g = X & ( for x being object st x in X holds
g . x = H1(x) ) ) from FUNCT_1:sch 3();
per cases ( X <> {} or X = {} ) ;
suppose X <> {} ; :: thesis: card X c= card Y
then reconsider M = rng g as non empty set by A11, RELAT_1:42;
for Z being set st Z in M holds
Z <> {}
proof
let Z be set ; :: thesis: ( Z in M implies Z <> {} )
assume Z in M ; :: thesis: Z <> {}
then consider x being object such that
A12: ( x in dom g & Z = g . x ) by FUNCT_1:def 3;
A13: x in {x} by TARSKI:def 1;
( Z = f " {x} & ex y being object st
( y in dom f & x = f . y ) ) by A10, A11, A12, FUNCT_1:def 3;
hence Z <> {} by A13, FUNCT_1:def 7; :: thesis: verum
end;
then consider F being Function such that
A14: dom F = M and
A15: for Z being set st Z in M holds
F . Z in Z by FUNCT_1:111;
A16: dom (F * g) = X by A11, A14, RELAT_1:27;
A17: F * g is one-to-one
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (F * g) or not y in dom (F * g) or not (F * g) . x = (F * g) . y or x = y )
assume that
A18: x in dom (F * g) and
A19: y in dom (F * g) and
A20: (F * g) . x = (F * g) . y ; :: thesis: x = y
A21: g . y = f " {y} by A11, A16, A19;
then f " {y} in M by A11, A16, A19, FUNCT_1:def 3;
then F . (f " {y}) in f " {y} by A15;
then A22: f . (F . (f " {y})) in {y} by FUNCT_1:def 7;
A23: g . x = f " {x} by A11, A16, A18;
then f " {x} in M by A11, A16, A18, FUNCT_1:def 3;
then F . (f " {x}) in f " {x} by A15;
then f . (F . (f " {x})) in {x} by FUNCT_1:def 7;
then A24: f . (F . (f " {x})) = x by TARSKI:def 1;
( (F * g) . x = F . (g . x) & (F * g) . y = F . (g . y) ) by A11, A16, A18, A19, FUNCT_1:13;
hence x = y by A20, A23, A21, A22, A24, TARSKI:def 1; :: thesis: verum
end;
rng (F * g) c= Y
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (F * g) or x in Y )
assume x in rng (F * g) ; :: thesis: x in Y
then consider y being object such that
A25: y in dom (F * g) and
A26: x = (F * g) . y by FUNCT_1:def 3;
A27: x = F . (g . y) by A11, A16, A25, A26, FUNCT_1:13;
A28: g . y = f " {y} by A11, A16, A25;
then f " {y} in M by A11, A16, A25, FUNCT_1:def 3;
then x in f " {y} by A15, A28, A27;
hence x in Y by A9, FUNCT_1:def 7; :: thesis: verum
end;
hence card X c= card Y by A16, A17, Th9; :: thesis: verum
end;
suppose X = {} ; :: thesis: card X c= card Y
hence card X c= card Y ; :: thesis: verum
end;
end;