let D be non empty set ; :: thesis: ( D is countable implies D * is countable )
defpred S1[ object , object ] means ex n being Nat st
( \$1 = n & \$2 = n -tuples_on D );
A1: for x being object st x in NAT holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st S1[x,y] )
assume x in NAT ; :: thesis: ex y being object st S1[x,y]
then reconsider n = x as Element of NAT ;
reconsider y = n -tuples_on D as set ;
take y ; :: thesis: S1[x,y]
take n ; :: thesis: ( x = n & y = n -tuples_on D )
thus ( x = n & y = n -tuples_on D ) ; :: thesis: verum
end;
consider f being Function such that
A2: ( dom f = NAT & ( for x being object st x in NAT holds
S1[x,f . x] ) ) from A3: D * = union { () where k is Nat : verum } by FINSEQ_2:108;
A4: Union f = D *
proof
thus Union f c= D * :: according to XBOOLE_0:def 10 :: thesis: D * c= Union f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union f or x in D * )
assume x in Union f ; :: thesis: x in D *
then consider X being set such that
A5: x in X and
A6: X in rng f by TARSKI:def 4;
consider y being object such that
A7: y in dom f and
A8: X = f . y by ;
reconsider y = y as Element of NAT by A2, A7;
ex n being Nat st
( y = n & X = n -tuples_on D ) by A2, A8;
then X in { () where k is Nat : verum } ;
hence x in D * by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D * or x in Union f )
assume x in D * ; :: thesis: x in Union f
then consider X being set such that
A9: ( x in X & X in { () where k is Nat : verum } ) by ;
consider n being Nat such that
A10: X = n -tuples_on D by A9;
A11: n in NAT by ORDINAL1:def 12;
then ex k being Nat st
( n = k & f . n = k -tuples_on D ) by A2;
then X in rng f by ;
hence x in Union f by ; :: thesis: verum
end;
assume A12: D is countable ; :: thesis: D * is countable
now :: thesis: for x being set st x in dom f holds
f . x is countable
let x be set ; :: thesis: ( x in dom f implies f . x is countable )
assume x in dom f ; :: thesis: f . x is countable
then ex n being Nat st
( x = n & f . x = n -tuples_on D ) by A2;
hence f . x is countable by ; :: thesis: verum
end;
hence D * is countable by A2, A4, Th11; :: thesis: verum