let k be Nat; :: thesis: for X being finite set st ( for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) holds

ex C being finite set st

( C = union X & card C = k * (card X) )

let X be finite set ; :: thesis: ( ( for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union X & card C = k * (card X) ) )

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) holds

ex C being finite set st

( C = union X & card C = k * (card X) )

let X be finite set ; :: thesis: ( ( for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union X & card C = k * (card X) ) )

per cases
( X = {} or X <> {} )
;

end;

suppose A1:
X = {}
; :: thesis: ( ( for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union X & card C = k * (card X) ) )

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union X & card C = k * (card X) ) )

reconsider E = {} as finite set ;

assume for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ; :: thesis: ex C being finite set st

( C = union X & card C = k * (card X) )

take E ; :: thesis: ( E = union X & card E = k * (card X) )

thus ( E = union X & card E = k * (card X) ) by A1, CARD_1:27, ZFMISC_1:2; :: thesis: verum

end;assume for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ; :: thesis: ex C being finite set st

( C = union X & card C = k * (card X) )

take E ; :: thesis: ( E = union X & card E = k * (card X) )

thus ( E = union X & card E = k * (card X) ) by A1, CARD_1:27, ZFMISC_1:2; :: thesis: verum

suppose
X <> {}
; :: thesis: ( ( for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union X & card C = k * (card X) ) )

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union X & card C = k * (card X) ) )

then reconsider D = X as non empty set ;

defpred S_{1}[ Element of Fin D] means ( ( for Y being set st Y in $1 holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in $1 & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union $1 & card C = k * (card $1) ) );

A2: for S being Element of Fin D

for s being Element of D st S_{1}[S] & not s in S holds

S_{1}[S \/ {.s.}]

A24: S_{1}[ {}. D]
by ZFMISC_1:2;

for B being Element of Fin D holds S_{1}[B]
from SETWISEO:sch 2(A24, A2);

hence ( ( for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union X & card C = k * (card X) ) ) by A23; :: thesis: verum

end;defpred S

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in $1 & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union $1 & card C = k * (card $1) ) );

A2: for S being Element of Fin D

for s being Element of D st S

S

proof

A23:
X is Element of Fin D
by FINSUB_1:def 5;
let S be Element of Fin D; :: thesis: for s being Element of D st S_{1}[S] & not s in S holds

S_{1}[S \/ {.s.}]

let s be Element of D; :: thesis: ( S_{1}[S] & not s in S implies S_{1}[S \/ {.s.}] )

assume that

A3: ( ( for Y being set st Y in S holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union S & card C = k * (card S) ) ) and

A4: not s in S and

A5: for Y being set st Y in S \/ {s} holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ; :: thesis: ex C being finite set st

( C = union (S \/ {.s.}) & card C = k * (card (S \/ {.s.})) )

A6: card (S \/ {s}) = (card S) + 1 by A4, CARD_2:41;

then s in S \/ {s} by XBOOLE_0:def 3;

then A12: ex B being finite set st

( B = s & card B = k & ( for Z being set st Z in S \/ {s} & s <> Z holds

( s,Z are_equipotent & s misses Z ) ) ) by A5;

then reconsider T = s as finite set ;

A13: union {s} = s by ZFMISC_1:25;

then A14: union (S \/ {s}) = D1 \/ T by ZFMISC_1:78;

then reconsider D2 = union (S \/ {s}) as finite set ;

take D2 ; :: thesis: ( D2 = union (S \/ {.s.}) & card D2 = k * (card (S \/ {.s.})) )

thus D2 = union (S \/ {s}) ; :: thesis: card D2 = k * (card (S \/ {.s.}))

.= k * (card (S \/ {s})) by A6 ;

:: thesis: verum

end;S

let s be Element of D; :: thesis: ( S

assume that

A3: ( ( for Y being set st Y in S holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union S & card C = k * (card S) ) ) and

A4: not s in S and

A5: for Y being set st Y in S \/ {s} holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ; :: thesis: ex C being finite set st

( C = union (S \/ {.s.}) & card C = k * (card (S \/ {.s.})) )

A6: card (S \/ {s}) = (card S) + 1 by A4, CARD_2:41;

now :: thesis: for Y being set st Y in S holds

Y is finite

then reconsider D1 = union S as finite set by FINSET_1:7;Y is finite

let Y be set ; :: thesis: ( Y in S implies Y is finite )

assume Y in S ; :: thesis: Y is finite

then Y in S \/ {s} by XBOOLE_0:def 3;

then ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) by A5;

hence Y is finite ; :: thesis: verum

end;assume Y in S ; :: thesis: Y is finite

then Y in S \/ {s} by XBOOLE_0:def 3;

then ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) by A5;

hence Y is finite ; :: thesis: verum

A7: now :: thesis: for Y, Z being set st Y in S holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

s in {s}
by TARSKI:def 1;ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

let Y, Z be set ; :: thesis: ( Y in S implies ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) )

assume Y in S ; :: thesis: ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

then Y in S \/ {s} by XBOOLE_0:def 3;

then consider B being finite set such that

A8: ( B = Y & card B = k ) and

A9: for Z being set st Z in S \/ {s} & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) by A5;

take B = B; :: thesis: ( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

thus ( B = Y & card B = k ) by A8; :: thesis: for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z )

let Z be set ; :: thesis: ( Z in S & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) )

assume that

A10: Z in S and

A11: Y <> Z ; :: thesis: ( Y,Z are_equipotent & Y misses Z )

Z in S \/ {s} by A10, XBOOLE_0:def 3;

hence ( Y,Z are_equipotent & Y misses Z ) by A9, A11; :: thesis: verum

end;( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) )

assume Y in S ; :: thesis: ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

then Y in S \/ {s} by XBOOLE_0:def 3;

then consider B being finite set such that

A8: ( B = Y & card B = k ) and

A9: for Z being set st Z in S \/ {s} & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) by A5;

take B = B; :: thesis: ( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

thus ( B = Y & card B = k ) by A8; :: thesis: for Z being set st Z in S & Y <> Z holds

( Y,Z are_equipotent & Y misses Z )

let Z be set ; :: thesis: ( Z in S & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) )

assume that

A10: Z in S and

A11: Y <> Z ; :: thesis: ( Y,Z are_equipotent & Y misses Z )

Z in S \/ {s} by A10, XBOOLE_0:def 3;

hence ( Y,Z are_equipotent & Y misses Z ) by A9, A11; :: thesis: verum

then s in S \/ {s} by XBOOLE_0:def 3;

then A12: ex B being finite set st

( B = s & card B = k & ( for Z being set st Z in S \/ {s} & s <> Z holds

( s,Z are_equipotent & s misses Z ) ) ) by A5;

then reconsider T = s as finite set ;

A13: union {s} = s by ZFMISC_1:25;

then A14: union (S \/ {s}) = D1 \/ T by ZFMISC_1:78;

then reconsider D2 = union (S \/ {s}) as finite set ;

take D2 ; :: thesis: ( D2 = union (S \/ {.s.}) & card D2 = k * (card (S \/ {.s.})) )

thus D2 = union (S \/ {s}) ; :: thesis: card D2 = k * (card (S \/ {.s.}))

now :: thesis: not union S meets union {s}

hence card D2 =
(k * (card S)) + (k * 1)
by A3, A13, A12, A14, A7, CARD_2:40
assume
union S meets union {s}
; :: thesis: contradiction

then consider x being object such that

A15: x in union S and

A16: x in union {s} by XBOOLE_0:3;

consider Y being set such that

A17: x in Y and

A18: Y in S by A15, TARSKI:def 4;

consider Z being set such that

A19: x in Z and

A20: Z in {s} by A16, TARSKI:def 4;

A21: Z in S \/ {s} by A20, XBOOLE_0:def 3;

Y in S \/ {s} by A18, XBOOLE_0:def 3;

then A22: ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) by A5;

Z <> Y by A4, A18, A20, TARSKI:def 1;

then Y misses Z by A21, A22;

hence contradiction by A17, A19, XBOOLE_0:3; :: thesis: verum

end;then consider x being object such that

A15: x in union S and

A16: x in union {s} by XBOOLE_0:3;

consider Y being set such that

A17: x in Y and

A18: Y in S by A15, TARSKI:def 4;

consider Z being set such that

A19: x in Z and

A20: Z in {s} by A16, TARSKI:def 4;

A21: Z in S \/ {s} by A20, XBOOLE_0:def 3;

Y in S \/ {s} by A18, XBOOLE_0:def 3;

then A22: ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) by A5;

Z <> Y by A4, A18, A20, TARSKI:def 1;

then Y misses Z by A21, A22;

hence contradiction by A17, A19, XBOOLE_0:3; :: thesis: verum

.= k * (card (S \/ {s})) by A6 ;

:: thesis: verum

A24: S

for B being Element of Fin D holds S

hence ( ( for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st

( C = union X & card C = k * (card X) ) ) by A23; :: thesis: verum