let X, Y be finite set ; :: thesis: for F being Function of X,Y st card X = card Y holds

( F is onto iff F is one-to-one )

let F be Function of X,Y; :: thesis: ( card X = card Y implies ( F is onto iff F is one-to-one ) )

assume A1: card X = card Y ; :: thesis: ( F is onto iff F is one-to-one )

thus ( F is onto implies F is one-to-one ) :: thesis: ( F is one-to-one implies F is onto )

( F is onto iff F is one-to-one )

let F be Function of X,Y; :: thesis: ( card X = card Y implies ( F is onto iff F is one-to-one ) )

assume A1: card X = card Y ; :: thesis: ( F is onto iff F is one-to-one )

thus ( F is onto implies F is one-to-one ) :: thesis: ( F is one-to-one implies F is onto )

proof

thus
( F is one-to-one implies F is onto )
:: thesis: verum
assume A2:
F is onto
; :: thesis: F is one-to-one

assume not F is one-to-one ; :: thesis: contradiction

then consider x1, x2 being object such that

A3: x1 in dom F and

A4: x2 in dom F and

A5: F . x1 = F . x2 and

A6: x1 <> x2 ;

reconsider Xx = X \ {x1} as finite set ;

Y c= F .: Xx

card Xx < card X by A3, Lm4;

then Segm (card Xx) c< Segm (card X) by NAT_1:39;

then Segm (card X) c< Segm (card Y) by A1, A10, XBOOLE_1:58;

hence contradiction by A1; :: thesis: verum

end;assume not F is one-to-one ; :: thesis: contradiction

then consider x1, x2 being object such that

A3: x1 in dom F and

A4: x2 in dom F and

A5: F . x1 = F . x2 and

A6: x1 <> x2 ;

reconsider Xx = X \ {x1} as finite set ;

Y c= F .: Xx

proof

then A10:
Segm (card Y) c= Segm (card Xx)
by CARD_1:66;
let Fy be object ; :: according to TARSKI:def 3 :: thesis: ( not Fy in Y or Fy in F .: Xx )

assume Fy in Y ; :: thesis: Fy in F .: Xx

then Fy in rng F by A2, FUNCT_2:def 3;

then consider y being object such that

A7: y in dom F and

A8: F . y = Fy by FUNCT_1:def 3;

end;assume Fy in Y ; :: thesis: Fy in F .: Xx

then Fy in rng F by A2, FUNCT_2:def 3;

then consider y being object such that

A7: y in dom F and

A8: F . y = Fy by FUNCT_1:def 3;

now :: thesis: Fy in F .: Xx

hence
Fy in F .: Xx
; :: thesis: verumend;

card Xx < card X by A3, Lm4;

then Segm (card Xx) c< Segm (card X) by NAT_1:39;

then Segm (card X) c< Segm (card Y) by A1, A10, XBOOLE_1:58;

hence contradiction by A1; :: thesis: verum

proof

assume
F is one-to-one
; :: thesis: F is onto

then dom F,F .: (dom F) are_equipotent by CARD_1:33;

then A11: card (dom F) = card (F .: (dom F)) by CARD_1:5;

assume not F is onto ; :: thesis: contradiction

then not rng F = Y by FUNCT_2:def 3;

then not Y c= rng F ;

then consider y being object such that

A12: y in Y and

A13: not y in rng F ;

A14: card (rng F) <= card (Y \ {y}) by A13, NAT_1:43, ZFMISC_1:34;

A15: F .: (dom F) = rng F by RELAT_1:113;

card (Y \ {y}) < card Y by A12, Lm4;

hence contradiction by A1, A12, A14, A11, A15, FUNCT_2:def 1; :: thesis: verum

end;then dom F,F .: (dom F) are_equipotent by CARD_1:33;

then A11: card (dom F) = card (F .: (dom F)) by CARD_1:5;

assume not F is onto ; :: thesis: contradiction

then not rng F = Y by FUNCT_2:def 3;

then not Y c= rng F ;

then consider y being object such that

A12: y in Y and

A13: not y in rng F ;

A14: card (rng F) <= card (Y \ {y}) by A13, NAT_1:43, ZFMISC_1:34;

A15: F .: (dom F) = rng F by RELAT_1:113;

card (Y \ {y}) < card Y by A12, Lm4;

hence contradiction by A1, A12, A14, A11, A15, FUNCT_2:def 1; :: thesis: verum