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 )
proof
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 set such that
A3: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 & x1 <> x2 ) by FUNCT_1:def 8;
reconsider Xx = X \ {x1} as finite set ;
Y c= F .: Xx
proof
let Fy be set ; :: according to TARSKI:def 3 :: thesis: ( not Fy in Y or Fy in F .: Xx )
assume A4: Fy in Y ; :: thesis: Fy in F .: Xx
Fy in rng F by A2, A4, FUNCT_2:def 3;
then consider y being set such that
A5: ( y in dom F & F . y = Fy ) by FUNCT_1:def 5;
now
per cases ( y = x1 or y <> x1 ) ;
suppose y = x1 ; :: thesis: Fy in F .: Xx
then ( Fy = F . x2 & x2 in Xx ) by A3, A5, ZFMISC_1:64;
hence Fy in F .: Xx by A3, FUNCT_1:def 12; :: thesis: verum
end;
end;
end;
hence Fy in F .: Xx ; :: thesis: verum
end;
then ( card Y c= card Xx & x1 in X ) by A3, CARD_2:2;
then ( card Y <= card Xx & card Xx < card X ) by Lm3, NAT_1:40;
hence contradiction by A1; :: thesis: verum
end;
thus ( F is one-to-one implies F is onto ) :: thesis: verum
proof
assume A6: F is one-to-one ; :: thesis: F is onto
assume not F is onto ; :: thesis: contradiction
then not rng F = Y by FUNCT_2:def 3;
then not Y c= rng F by XBOOLE_0:def 10;
then consider y being set such that
A7: ( y in Y & not y in rng F ) by TARSKI:def 3;
( rng F c= Y \ {y} & dom F,F .: (dom F) are_equipotent ) by A6, A7, CARD_1:60, ZFMISC_1:40;
then ( card (rng F) <= card (Y \ {y}) & card (Y \ {y}) < card Y & card (dom F) = card (F .: (dom F)) & F .: (dom F) = rng F & dom F = X ) by A7, Lm3, CARD_1:21, FUNCT_2:def 1, NAT_1:44, RELAT_1:146;
hence contradiction by A1; :: thesis: verum
end;