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