let X, Y be set ; :: thesis: ( card X c= card Y iff ex f being Function st

( f is one-to-one & X c= dom f & f .: X c= Y ) )

thus ( card X c= card Y implies ex f being Function st

( f is one-to-one & X c= dom f & f .: X c= Y ) ) :: thesis: ( ex f being Function st

( f is one-to-one & X c= dom f & f .: X c= Y ) implies card X c= card Y )

A3: X c= dom f and

A4: f .: X c= Y ; :: thesis: card X c= card Y

A5: rng (f | X) c= Y

hence card X c= card Y by A5, CARD_1:10; :: thesis: verum

( f is one-to-one & X c= dom f & f .: X c= Y ) )

thus ( card X c= card Y implies ex f being Function st

( f is one-to-one & X c= dom f & f .: X c= Y ) ) :: thesis: ( ex f being Function st

( f is one-to-one & X c= dom f & f .: X c= Y ) implies card X c= card Y )

proof

given f being Function such that A2:
f is one-to-one
and
assume
card X c= card Y
; :: thesis: ex f being Function st

( f is one-to-one & X c= dom f & f .: X c= Y )

then consider f being Function such that

A1: ( f is one-to-one & dom f = X & rng f c= Y ) by CARD_1:10;

take f ; :: thesis: ( f is one-to-one & X c= dom f & f .: X c= Y )

thus ( f is one-to-one & X c= dom f & f .: X c= Y ) by A1, RELAT_1:113; :: thesis: verum

end;( f is one-to-one & X c= dom f & f .: X c= Y )

then consider f being Function such that

A1: ( f is one-to-one & dom f = X & rng f c= Y ) by CARD_1:10;

take f ; :: thesis: ( f is one-to-one & X c= dom f & f .: X c= Y )

thus ( f is one-to-one & X c= dom f & f .: X c= Y ) by A1, RELAT_1:113; :: thesis: verum

A3: X c= dom f and

A4: f .: X c= Y ; :: thesis: card X c= card Y

A5: rng (f | X) c= Y

proof

( f | X is one-to-one & dom (f | X) = X )
by A2, A3, FUNCT_1:52, RELAT_1:62;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | X) or y in Y )

assume y in rng (f | X) ; :: thesis: y in Y

then consider x being object such that

A6: ( x in dom (f | X) & y = (f | X) . x ) by FUNCT_1:def 3;

( x in X & y = f . x ) by A3, A6, FUNCT_1:47, RELAT_1:62;

then y in f .: X by A3, FUNCT_1:def 6;

hence y in Y by A4; :: thesis: verum

end;assume y in rng (f | X) ; :: thesis: y in Y

then consider x being object such that

A6: ( x in dom (f | X) & y = (f | X) . x ) by FUNCT_1:def 3;

( x in X & y = f . x ) by A3, A6, FUNCT_1:47, RELAT_1:62;

then y in f .: X by A3, FUNCT_1:def 6;

hence y in Y by A4; :: thesis: verum

hence card X c= card Y by A5, CARD_1:10; :: thesis: verum