let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is bijective holds
X,Y are_equipotent
let f be Function of X,Y; :: thesis: ( f is bijective implies X,Y are_equipotent )
assume A1: f is bijective ; :: thesis: X,Y are_equipotent
take h = f; :: according to TARSKI:def 6 :: thesis: ( ( for b1 being object holds
( not b1 in X or ex b2 being object st
( b2 in Y & [b1,b2] in h ) ) ) & ( for b1 being object holds
( not b1 in Y or ex b2 being object st
( b2 in X & [b2,b1] in h ) ) ) & ( for b1, b2, b3, b4 being object holds
( not [b1,b2] in h or not [b3,b4] in h or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
A2: ( h is one-to-one & h is onto ) by A1, FUNCT_2:def 4;
then A3: rng h = Y by FUNCT_2:def 3;
hereby :: thesis: ( ( for b1 being object holds
( not b1 in Y or ex b2 being object st
( b2 in X & [b2,b1] in h ) ) ) & ( for b1, b2, b3, b4 being object holds
( not [b1,b2] in h or not [b3,b4] in h or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
let x be object ; :: thesis: ( x in X implies ex y being object st
( y in Y & [x,y] in h ) )
assume A4: x in X ; :: thesis: ex y being object st
( y in Y & [x,y] in h )
reconsider y = h . x as object ;
take y = y; :: thesis: ( y in Y & [x,y] in h )
thus y in Y by A3, A4, FUNCT_2:4; :: thesis: [x,y] in h
x in dom h by A4, FUNCT_2:def 1;
hence [x,y] in h by FUNCT_1:1; :: thesis: verum
end;
hereby :: thesis: for b1, b2, b3, b4 being object holds
( not [b1,b2] in h or not [b3,b4] in h or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) )
let y be object ; :: thesis: ( y in Y implies ex x being object st
( x in X & [x,y] in h ) )
assume y in Y ; :: thesis: ex x being object st
( x in X & [x,y] in h )
then consider x being object such that
A5: ( x in dom h & y = h . x ) by A3, FUNCT_1:def 3;
reconsider x = x as object ;
take x = x; :: thesis: ( x in X & [x,y] in h )
thus ( x in X & [x,y] in h ) by A5, FUNCT_1:1; :: thesis: verum
end;
let x, y, z, u be object ; :: thesis: ( not [x,y] in h or not [z,u] in h or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
assume that
A6: [x,y] in h and
A7: [z,u] in h ; :: thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )
A8: ( z in dom h & u = h . z ) by A7, FUNCT_1:1;
( x in dom h & y = h . x ) by A6, FUNCT_1:1;
hence ( ( not x = z or y = u ) & ( not y = u or x = z ) ) by A2, A8; :: thesis: verum