let X be set ; :: thesis: for x being object holds
( X,{x} are_equipotent iff ex x being object st X = {x} )
let x be object ; :: thesis: ( X,{x} are_equipotent iff ex x being object st X = {x} )
thus ( X,{x} are_equipotent implies ex x being object st X = {x} ) :: thesis: ( ex x being object st X = {x} implies X,{x} are_equipotent )
proof
assume X,{x} are_equipotent ; :: thesis: ex x being object st X = {x}
then consider f being Function such that
f is one-to-one and
A1: dom f = {x} and
A2: rng f = X by WELLORD2:def 4;
rng f = {(f . x)} by A1, FUNCT_1:4;
hence ex x being object st X = {x} by A2; :: thesis: verum
end;
given y being object such that A3: X = {y} ; :: thesis: X,{x} are_equipotent
take f = X --> x; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = {x} )
A4: dom f = X ;
thus f is one-to-one :: thesis: ( dom f = X & rng f = {x} )
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A5: a in dom f and
A6: b in dom f and
f . a = f . b ; :: thesis: a = b
a = y by A3, A5, TARSKI:def 1;
hence a = b by A3, A6, TARSKI:def 1; :: thesis: verum
end;
thus dom f = X ; :: thesis: rng f = {x}
thus rng f c= {x} by FUNCOP_1:13; :: according to XBOOLE_0:def 10 :: thesis: {x} c= rng f
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} or a in rng f )
assume a in {x} ; :: thesis: a in rng f
then A7: a = x by TARSKI:def 1;
A8: y in {y} by TARSKI:def 1;
then f . y = x by A3, FUNCOP_1:7;
hence a in rng f by A3, A4, A7, A8, FUNCT_1:def 3; :: thesis: verum