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 S₁[ set , set ] means ex A being Ordinal ex phi being Ordinal-Sequence st
( $2 = [A,phi] & dom phi = M & phi | A is increasing & rng (phi | A) = f .: $1 & ( for B being Ordinal st A c= B & B in M holds
phi . B = {} ) );
A4: for x being set st x in { Y where Y is Subset of X : card Y in M } holds
ex y being set st S₁[x,y]

proof

deffunc H₁( set ) -> set = {} ;
let x be set ; :: thesis: ( x in { Y where Y is Subset of X : card Y in M } implies ex y being set st S₁[x,y] )
set A = order_type_of (RelIncl (f .: x));
consider xi2 being Ordinal-Sequence such that
A5: ( dom xi2 = M -^ (order_type_of (RelIncl (f .: x))) & ( for B being Ordinal st B in M -^ (order_type_of (RelIncl (f .: x))) holds
xi2 . B = H₁(B) ) ) from ORDINAL2:sch 3();
assume x in { Y where Y is Subset of X : card Y in M } ; :: thesis: ex y being set st S₁[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 .: x)))),(RelIncl (f .: x))) and
A7: xi1 is increasing and
A8: dom xi1 = order_type_of (RelIncl (f .: x)) and
A9: rng xi1 = f .: x by A3, Th14, RELAT_1:111;
set phi = xi1 ^ xi2;
take y = [(order_type_of (RelIncl (f .: x))),(xi1 ^ xi2)]; :: thesis: S₁[x,y]
take order_type_of (RelIncl (f .: x)) ; :: thesis: ex phi being Ordinal-Sequence st
( y = [(order_type_of (RelIncl (f .: x))),phi] & dom phi = M & phi | (order_type_of (RelIncl (f .: x))) is increasing & rng (phi | (order_type_of (RelIncl (f .: x)))) = f .: x & ( for B being Ordinal st order_type_of (RelIncl (f .: x)) c= B & B in M holds
phi . B = {} ) )
take xi1 ^ xi2 ; :: thesis: ( y = [(order_type_of (RelIncl (f .: x))),(xi1 ^ xi2)] & dom (xi1 ^ xi2) = M & (xi1 ^ xi2) | (order_type_of (RelIncl (f .: x))) is increasing & rng ((xi1 ^ xi2) | (order_type_of (RelIncl (f .: x)))) = f .: x & ( for B being Ordinal st order_type_of (RelIncl (f .: x)) c= B & B in M holds
(xi1 ^ xi2) . B = {} ) )
card (f .: x) = card (order_type_of (RelIncl (f .: x))) by A3, Th16, RELAT_1:111;
then card (order_type_of (RelIncl (f .: x))) in M by A6, CARD_1:67, ORDINAL1:12;
then order_type_of (RelIncl (f .: x)) in M by CARD_3:44;
then order_type_of (RelIncl (f .: x)) c= M by ORDINAL1:def 2;
then (order_type_of (RelIncl (f .: x))) +^ (M -^ (order_type_of (RelIncl (f .: x)))) = M by ORDINAL3:def 5;
hence ( y = [(order_type_of (RelIncl (f .: x))),(xi1 ^ xi2)] & dom (xi1 ^ xi2) = M & (xi1 ^ xi2) | (order_type_of (RelIncl (f .: x))) is increasing & rng ((xi1 ^ xi2) | (order_type_of (RelIncl (f .: x)))) = f .: x ) by A7, A8, A9, A5, Th21, ORDINAL4:def 1; :: thesis: for B being Ordinal st order_type_of (RelIncl (f .: x)) c= B & B in M holds
(xi1 ^ xi2) . B = {}
let B be Ordinal; :: thesis: ( order_type_of (RelIncl (f .: x)) c= B & B in M implies (xi1 ^ xi2) . B = {} )
assume that
A10: order_type_of (RelIncl (f .: x)) c= B and
A11: B in M ; :: thesis: (xi1 ^ xi2) . B = {}
A12: B -^ (order_type_of (RelIncl (f .: x))) in M -^ (order_type_of (RelIncl (f .: x))) by A10, A11, ORDINAL3:53;
B = (order_type_of (RelIncl (f .: x))) +^ (B -^ (order_type_of (RelIncl (f .: x)))) by A10, ORDINAL3:def 5;
then (xi1 ^ xi2) . B = xi2 . (B -^ (order_type_of (RelIncl (f .: x)))) 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 set st x in { Y where Y is Subset of X : card Y in M } holds
S₁[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 set ; :: 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 set such that
A15: y in dom g and
A16: x = g . y by FUNCT_1:def 3;
consider A being Ordinal, phi being Ordinal-Sequence such that
A17: x = [A,phi] and
A18: dom phi = M and
A19: phi | A is increasing and
A20: rng (phi | A) = f .: y and
A21: for B being Ordinal st A c= B & B in M holds
phi . B = {} by A13, A15, A16;
A22: 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 set ; :: 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 set such that
A23: z in dom phi and
A24: x = phi . z by FUNCT_1:def 3;
reconsider z = z as Ordinal by A23;
( z in A or A c= z ) by ORDINAL1:16;
then ( ( x in f .: y & f .: y c= card X ) or x = {} ) by A3, A18, A20, A21, A23, A24, FUNCT_1:50, RELAT_1:111;
hence x in card X by A14, ORDINAL3:8; :: thesis: verum

end;

then A25: phi in Funcs (M,(card X)) by A18, FUNCT_2:def 2;
A26: ( A c= M or M c= A ) ;
phi | A is one-to-one by A19, Th20;
then dom (phi | A),f .: y are_equipotent by A20, WELLORD2:def 4;
then card (dom (phi | A)) = card (f .: y) by CARD_1:5;
then card (dom (phi | A)) in M by A22, CARD_1:67, ORDINAL1:12;
then A27: dom (phi | A) in M by CARD_3:44;
then dom (phi | A) <> M ;
then A in M by A18, A27, A26, RELAT_1:62, RELAT_1:68;
hence x in [:M,(Funcs (M,(card X))):] by A17, A25, ZFMISC_1:87; :: thesis: verum

end;

then A28: card (rng g) c= card [:M,(Funcs (M,(card X))):] by CARD_1:11;
g is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 g or not b₁ in proj1 g or not g . x = g . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
assume that
A29: x in dom g and
A30: y in dom g and
A31: g . x = g . y ; :: thesis: x = y
consider A2 being Ordinal, phi2 being Ordinal-Sequence such that
A32: g . y = [A2,phi2] and
dom phi2 = M and
phi2 | A2 is increasing and
A33: rng (phi2 | A2) = f .: y and
for B being Ordinal st A2 c= B & B in M holds
phi2 . B = {} by A13, A30;
consider A1 being Ordinal, phi1 being Ordinal-Sequence such that
A34: g . x = [A1,phi1] and
dom phi1 = M and
phi1 | A1 is increasing and
A35: rng (phi1 | A1) = f .: x and
for B being Ordinal st A1 c= B & B in M holds
phi1 . B = {} by A13, A29;
A36: ( A1 = A2 & phi1 = phi2 ) by A31, A34, A32, ZFMISC_1:27;
A37: ex Y being Subset of X st
( x = Y & card Y in M ) by A13, A29;
thus x c= y :: according to XBOOLE_0:def 10 :: thesis: y c= x

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in y )
assume A38: z in x ; :: thesis: z in y
then f . z in f .: x by A2, A37, FUNCT_1:def 6;
then ex x1 being set st
( x1 in dom f & x1 in y & f . z = f . x1 ) by A35, A33, A36, FUNCT_1:def 6;
hence z in y by A1, A2, A37, A38, FUNCT_1:def 4; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in y or z in x )
A39: ex Y being Subset of X st
( y = Y & card Y in M ) by A13, A30;
assume A40: z in y ; :: thesis: z in x
then f . z in f .: y by A2, A39, FUNCT_1:def 6;
then ex x1 being set st
( x1 in dom f & x1 in x & f . z = f . x1 ) by A35, A33, A36, FUNCT_1:def 6;
hence z in x by A1, A2, A39, A40, FUNCT_1:def 4; :: thesis: verum

end;

then A41: { 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 A41, A28, CARD_1:5; :: thesis: verum