let X, Y be set ; ( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] )
deffunc H3( object ) -> object = [($1 `2),($1 `1)];
consider f being Function such that
A1:
( dom f = [:X,Y:] & ( for x being object st x in [:X,Y:] holds
f . x = H3(x) ) )
from FUNCT_1:sch 3();
thus
[:X,Y:],[:Y,X:] are_equipotent
card [:X,Y:] = card [:Y,X:]proof
take
f
;
WELLORD2:def 4 ( f is one-to-one & proj1 f = [:X,Y:] & proj2 f = [:Y,X:] )
thus
f is
one-to-one
( proj1 f = [:X,Y:] & proj2 f = [:Y,X:] )proof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume A2:
(
x in dom f &
y in dom f )
;
( not f . x = f . y or x = y )
then A3:
(
x = [(x `1),(x `2)] &
y = [(y `1),(y `2)] )
by A1, MCART_1:21;
assume A4:
f . x = f . y
;
x = y
A5:
(
f . x = [(x `2),(x `1)] &
f . y = [(y `2),(y `1)] )
by A1, A2;
then
x `1 = y `1
by A4, XTUPLE_0:1;
hence
x = y
by A3, A5, A4, XTUPLE_0:1;
verum
end;
thus
dom f = [:X,Y:]
by A1;
proj2 f = [:Y,X:]
thus
rng f c= [:Y,X:]
XBOOLE_0:def 10 [:Y,X:] c= proj2 fproof
let x be
object ;
TARSKI:def 3 ( not x in rng f or x in [:Y,X:] )
assume
x in rng f
;
x in [:Y,X:]
then consider y being
object such that A6:
y in dom f
and A7:
x = f . y
by FUNCT_1:def 3;
A8:
y `2 in Y
by A1, A6, MCART_1:10;
(
x = [(y `2),(y `1)] &
y `1 in X )
by A1, A6, A7, MCART_1:10;
hence
x in [:Y,X:]
by A8, ZFMISC_1:87;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in [:Y,X:] or x in proj2 f )
A9:
(
[(x `2),(x `1)] `1 = x `2 &
[(x `2),(x `1)] `2 = x `1 )
;
assume A10:
x in [:Y,X:]
;
x in proj2 f
then A11:
x = [(x `1),(x `2)]
by MCART_1:21;
A12:
(
x `1 in Y &
x `2 in X )
by A10, MCART_1:10;
then
[(x `2),(x `1)] in [:X,Y:]
by ZFMISC_1:87;
then
f . [(x `2),(x `1)] in rng f
by A1, FUNCT_1:def 3;
hence
x in proj2 f
by A1, A11, A12, A9, ZFMISC_1:87;
verum
end;
hence
card [:X,Y:] = card [:Y,X:]
by CARD_1:5; verum