let X be set ; :: thesis: for M being Cardinal st X <> {} holds
card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M))
let M be Cardinal; :: thesis: ( X <> {} implies card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M)) )
set Z = { Y where Y is Subset of X : card Y in M } ;
X, card X are_equipotent by CARD_1:def 2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by WELLORD2:def 4;
defpred S1[ object , object ] means ex X being set ex A being Ordinal ex phi being Ordinal-Sequence st
( X = $1 & $2 = [A,phi] & dom phi = M & phi | A is increasing & rng (phi | A) = f .: X & ( for B being Ordinal st A c= B & B in M holds
phi . B = {} ) );
A4: for x being object st x in { Y where Y is Subset of X : card Y in M } holds
ex y being object st S1[x,y]
proof
deffunc H1( set ) -> set = {} ;
let x be object ; :: thesis: ( x in { Y where Y is Subset of X : card Y in M } implies ex y being object st S1[x,y] )
reconsider xx = x as set by TARSKI:1;
set A = order_type_of (RelIncl (f .: xx));
consider xi2 being Ordinal-Sequence such that
A5: ( dom xi2 = M -^ (order_type_of (RelIncl (f .: xx))) & ( for B being Ordinal st B in M -^ (order_type_of (RelIncl (f .: xx))) holds
xi2 . B = H1(B) ) ) from ORDINAL2:sch 3();
 assume x in { Y where Y is Subset of X : card Y in M } ; :: thesis: ex y being object st S1[x,y]
then A6: ex Y being Subset of X st
( x = Y & card Y in M ) ;
consider xi1 being Ordinal-Sequence such that
xi1 = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl (f .: xx)))),(RelIncl (f .: xx))) and
A7: xi1 is increasing and
A8: dom xi1 = order_type_of (RelIncl (f .: xx)) and
A9: rng xi1 = f .: xx by A3, Th5, RELAT_1:111;
set phi = xi1 ^ xi2;
take y = [(order_type_of (RelIncl (f .: xx))),(xi1 ^ xi2)]; :: thesis: S1[x,y]
take xx ; :: thesis: ex A being Ordinal ex phi being Ordinal-Sequence st
( xx = x & y = [A,phi] & dom phi = M & phi | A is increasing & rng (phi | A) = f .: xx & ( for B being Ordinal st A c= B & B in M holds
phi . B = {} ) )
take order_type_of (RelIncl (f .: xx)) ; :: thesis: ex phi being Ordinal-Sequence st
( xx = x & y = [(order_type_of (RelIncl (f .: xx))),phi] & dom phi = M & phi | (order_type_of (RelIncl (f .: xx))) is increasing & rng (phi | (order_type_of (RelIncl (f .: xx)))) = f .: xx & ( for B being Ordinal st order_type_of (RelIncl (f .: xx)) c= B & B in M holds
phi . B = {} ) )
take xi1 ^ xi2 ; :: thesis: ( xx = x & y = [(order_type_of (RelIncl (f .: xx))),(xi1 ^ xi2)] & dom (xi1 ^ xi2) = M & (xi1 ^ xi2) | (order_type_of (RelIncl (f .: xx))) is increasing & rng ((xi1 ^ xi2) | (order_type_of (RelIncl (f .: xx)))) = f .: xx & ( for B being Ordinal st order_type_of (RelIncl (f .: xx)) c= B & B in M holds
(xi1 ^ xi2) . B = {} ) )
thus xx = x ; :: thesis: ( y = [(order_type_of (RelIncl (f .: xx))),(xi1 ^ xi2)] & dom (xi1 ^ xi2) = M & (xi1 ^ xi2) | (order_type_of (RelIncl (f .: xx))) is increasing & rng ((xi1 ^ xi2) | (order_type_of (RelIncl (f .: xx)))) = f .: xx & ( for B being Ordinal st order_type_of (RelIncl (f .: xx)) c= B & B in M holds
(xi1 ^ xi2) . B = {} ) )
card (f .: xx) = card (order_type_of (RelIncl (f .: xx))) by A3, Th7, RELAT_1:111;
then card (order_type_of (RelIncl (f .: xx))) in M by A6, CARD_1:67, ORDINAL1:12;
then order_type_of (RelIncl (f .: xx)) in M by CARD_3:44;
then order_type_of (RelIncl (f .: xx)) c= M by ORDINAL1:def 2;
then (order_type_of (RelIncl (f .: xx))) +^ (M -^ (order_type_of (RelIncl (f .: xx)))) = M by ORDINAL3:def 5;
hence ( y = [(order_type_of (RelIncl (f .: xx))),(xi1 ^ xi2)] & dom (xi1 ^ xi2) = M & (xi1 ^ xi2) | (order_type_of (RelIncl (f .: xx))) is increasing & rng ((xi1 ^ xi2) | (order_type_of (RelIncl (f .: xx)))) = f .: xx ) by A7, A8, A9, A5, Th12, ORDINAL4:def 1; :: thesis: for B being Ordinal st order_type_of (RelIncl (f .: xx)) c= B & B in M holds
(xi1 ^ xi2) . B = {}
let B be Ordinal; :: thesis: ( order_type_of (RelIncl (f .: xx)) c= B & B in M implies (xi1 ^ xi2) . B = {} )
assume that
A10: order_type_of (RelIncl (f .: xx)) c= B and
A11: B in M ; :: thesis: (xi1 ^ xi2) . B = {}
A12: B -^ (order_type_of (RelIncl (f .: xx))) in M -^ (order_type_of (RelIncl (f .: xx))) by A10, A11, ORDINAL3:53;
B = (order_type_of (RelIncl (f .: xx))) +^ (B -^ (order_type_of (RelIncl (f .: xx)))) by A10, ORDINAL3:def 5;
then (xi1 ^ xi2) . B = xi2 . (B -^ (order_type_of (RelIncl (f .: xx)))) by A8, A5, A12, ORDINAL4:def 1;
hence (xi1 ^ xi2) . B = {} by A5, A12; :: thesis: verum
end;
consider g being Function such that
A13: ( dom g = { Y where Y is Subset of X : card Y in M } & ( for x being object st x in { Y where Y is Subset of X : card Y in M } holds
S1[x,g . x] ) ) from CLASSES1:sch 1(A4);
 assume A14: X <> {} ; :: thesis: card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M))
rng g c= [:M,(Funcs (M,(card X))):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in [:M,(Funcs (M,(card X))):] )
assume x in rng g ; :: thesis: x in [:M,(Funcs (M,(card X))):]
then consider y being object such that
A15: y in dom g and
A16: x = g . y by FUNCT_1:def 3;
consider yy being set , A being Ordinal, phi being Ordinal-Sequence such that
A17: yy = y and
A18: x = [A,phi] and
A19: dom phi = M and
A20: phi | A is increasing and
A21: rng (phi | A) = f .: yy and
A22: for B being Ordinal st A c= B & B in M holds
phi . B = {} by A13, A15, A16;
A23: ex Y being Subset of X st
( y = Y & card Y in M ) by A13, A15;
rng phi c= card X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng phi or x in card X )
assume x in rng phi ; :: thesis: x in card X
then consider z being object such that
A24: z in dom phi and
A25: x = phi . z by FUNCT_1:def 3;
reconsider z = z as Ordinal by A24;
( z in A or A c= z ) by ORDINAL1:16;
then ( ( x in f .: yy & f .: yy c= card X ) or x = {} ) by A3, A19, A21, A22, A24, A25, FUNCT_1:50, RELAT_1:111;
hence x in card X by A14, ORDINAL3:8; :: thesis: verum
end;
then A26: phi in Funcs (M,(card X)) by A19, FUNCT_2:def 2;
A27: ( A c= M or M c= A ) ;
phi | A is one-to-one by A20, Th11;
then dom (phi | A),f .: yy are_equipotent by A21, WELLORD2:def 4;
then card (dom (phi | A)) = card (f .: yy) by CARD_1:5;
then card (dom (phi | A)) in M by A23, CARD_1:67, ORDINAL1:12, A17;
then A28: dom (phi | A) in M by CARD_3:44;
then dom (phi | A) <> M ;
then A in M by A19, A28, A27, RELAT_1:62, RELAT_1:68;
hence x in [:M,(Funcs (M,(card X))):] by A18, A26, ZFMISC_1:87; :: thesis: verum
end;
then A29: card (rng g) c= card [:M,(Funcs (M,(card X))):] by CARD_1:11;
g is one-to-one
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
assume that
A30: x in dom g and
A31: y in dom g and
A32: g . x = g . y ; :: thesis: x = y
consider yy being set , A2 being Ordinal, phi2 being Ordinal-Sequence such that
A33: yy = y and
A34: g . y = [A2,phi2] and
dom phi2 = M and
phi2 | A2 is increasing and
A35: rng (phi2 | A2) = f .: yy and
for B being Ordinal st A2 c= B & B in M holds
phi2 . B = {} by A13, A31;
consider xx being set , A1 being Ordinal, phi1 being Ordinal-Sequence such that
A36: xx = x and
A37: g . x = [A1,phi1] and
dom phi1 = M and
phi1 | A1 is increasing and
A38: rng (phi1 | A1) = f .: xx and
for B being Ordinal st A1 c= B & B in M holds
phi1 . B = {} by A13, A30;
A39: ( A1 = A2 & phi1 = phi2 ) by A32, A37, A34, XTUPLE_0:1;
A40: ex Y being Subset of X st
( x = Y & card Y in M ) by A13, A30;
xx = yy
proof
thus xx c= yy :: according to XBOOLE_0:def 10 :: thesis: yy c= xx
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in xx or z in yy )
assume A41: z in xx ; :: thesis: z in yy
then f . z in f .: xx by A2, A40, FUNCT_1:def 6, A36;
then ex x1 being object st
( x1 in dom f & x1 in yy & f . z = f . x1 ) by A38, A35, A39, FUNCT_1:def 6;
hence z in yy by A1, A2, A40, A41, A36; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in yy or z in xx )
A42: ex Y being Subset of X st
( y = Y & card Y in M ) by A13, A31;
assume A43: z in yy ; :: thesis: z in xx
then f . z in f .: yy by A2, A42, FUNCT_1:def 6, A33;
then ex x1 being object st
( x1 in dom f & x1 in xx & f . z = f . x1 ) by A38, A35, A39, FUNCT_1:def 6;
hence z in xx by A1, A2, A42, A43, A33; :: thesis: verum
end;
hence x = y by A33, A36; :: thesis: verum
end;
then A44: { Y where Y is Subset of X : card Y in M } , rng g are_equipotent by A13, WELLORD2:def 4;
card [:M,(Funcs (M,(card X))):] = card [:M,(card (Funcs (M,(card X)))):] by CARD_2:7
.= M *` (card (Funcs (M,(card X)))) by CARD_2:def 2
.= M *` (exp ((card X),M)) by CARD_2:def 3 ;
hence card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M)) by A44, A29, CARD_1:5; :: thesis: verum