let A, B be Ordinal; ( A *^ B,[:A,B:] are_equipotent & card (A *^ B) = card [:A,B:] )
defpred S1[ object , object ] means ex O1, O2 being Ordinal st
( O1 = $1 `1 & O2 = $1 `2 & $2 = (O1 *^ B) +^ O2 );
A1:
for x being object st x in [:A,B:] holds
ex y being object st S1[x,y]
consider f being Function such that
A2:
( dom f = [:A,B:] & ( for x being object st x in [:A,B:] holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A1);
A3:
[:A,B:],A *^ B are_equipotent
proof
take
f
;
WELLORD2:def 4 ( f is one-to-one & proj1 f = [:A,B:] & proj2 f = A *^ B )
thus
f is
one-to-one
( proj1 f = [:A,B:] & proj2 f = A *^ B )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 A4:
(
x in dom f &
y in dom f )
;
( not f . x = f . y or x = y )
then A5:
(
x `2 in B &
y `2 in B )
by A2, MCART_1:10;
(
x `1 in A &
y `1 in A )
by A2, A4, MCART_1:10;
then reconsider x1 =
x `1 ,
y1 =
y `1 as
Ordinal ;
assume A6:
f . x = f . y
;
x = y
A7:
(
x = [(x `1),(x `2)] &
y = [(y `1),(y `2)] )
by A2, A4, MCART_1:21;
A8:
( ex
O1,
O2 being
Ordinal st
(
O1 = x `1 &
O2 = x `2 &
f . x = (O1 *^ B) +^ O2 ) & ex
O3,
O4 being
Ordinal st
(
O3 = y `1 &
O4 = y `2 &
f . y = (O3 *^ B) +^ O4 ) )
by A2, A4;
then
x1 = y1
by A5, A6, ORDINAL3:48;
hence
x = y
by A7, A5, A8, A6, ORDINAL3:48;
verum
end;
thus
dom f = [:A,B:]
by A2;
proj2 f = A *^ B
thus
rng f c= A *^ B
XBOOLE_0:def 10 A *^ B c= proj2 fproof
let y be
object ;
TARSKI:def 3 ( not y in rng f or y in A *^ B )
A9:
1
*^ B = B
by ORDINAL2:39;
assume
y in rng f
;
y in A *^ B
then consider x being
object such that A10:
x in dom f
and A11:
y = f . x
by FUNCT_1:def 3;
consider x1,
x2 being
Ordinal such that A12:
x1 = x `1
and A13:
(
x2 = x `2 &
f . x = (x1 *^ B) +^ x2 )
by A2, A10;
x1 +^ 1
= succ x1
by ORDINAL2:31;
then A14:
(x1 *^ B) +^ (1 *^ B) = (succ x1) *^ B
by ORDINAL3:46;
succ x1 c= A
by A12, A2, A10, MCART_1:10, ORDINAL1:21;
then A15:
(x1 *^ B) +^ (1 *^ B) c= A *^ B
by A14, ORDINAL2:41;
y in (x1 *^ B) +^ (1 *^ B)
by A11, A13, A9, A2, A10, MCART_1:10, ORDINAL2:32;
hence
y in A *^ B
by A15;
verum
end;
let y be
object ;
TARSKI:def 3 ( not y in A *^ B or y in proj2 f )
assume A16:
y in A *^ B
;
y in proj2 f
then reconsider C =
y as
Ordinal ;
A17:
(
C = ((C div^ B) *^ B) +^ (C mod^ B) &
[(C div^ B),(C mod^ B)] `1 = C div^ B )
by ORDINAL3:65;
(
C div^ B in A &
C mod^ B in B )
by A16, ORDINAL3:67;
then A18:
[(C div^ B),(C mod^ B)] in [:A,B:]
by ZFMISC_1:87;
then
(
[(C div^ B),(C mod^ B)] `2 = C mod^ B & ex
O1,
O2 being
Ordinal st
(
O1 = [(C div^ B),(C mod^ B)] `1 &
O2 = [(C div^ B),(C mod^ B)] `2 &
f . [(C div^ B),(C mod^ B)] = (O1 *^ B) +^ O2 ) )
by A2;
hence
y in proj2 f
by A2, A18, A17, FUNCT_1:def 3;
verum
end;
hence
A *^ B,[:A,B:] are_equipotent
; card (A *^ B) = card [:A,B:]
thus
card (A *^ B) = card [:A,B:]
by A3, CARD_1:5; verum