let A be set ; :: thesis: ( A is finite & ( for X being set st X in A holds
X is finite ) implies union A is finite )
assume that
A1: A is finite and
A2: for X being set st X in A holds
X is finite ; :: thesis: union A is finite
defpred S1[ set ] means ex B being set st
( B = $1 & union B is finite );
consider G being set such that
A3: for x being set holds
( x in G iff ( x in bool A & S1[x] ) ) from XFAMILY:sch 1();
 defpred S2[ set ] means $1 in G;
{} c= A ;
then A4: S2[ {} ] by A3, ZFMISC_1:2;
A5: for x, B being set st x in A & B c= A & S2[B] holds
S2[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in A & B c= A & S2[B] implies S2[B \/ {x}] )
assume that
A6: x in A and
B c= A and
A7: B in G ; :: thesis: S2[B \/ {x}]
A8: ex X being set st
( X = B & union X is finite ) by A3, A7;
A9: x is finite by A2, A6;
A10: union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:78
.= (union B) \/ x by ZFMISC_1:25 ;
A11: {x} c= A by A6, ZFMISC_1:31;
B in bool A by A3, A7;
then B \/ {x} c= A by A11, XBOOLE_1:8;
hence S2[B \/ {x}] by A3, A8, A9, A10; :: thesis: verum
end;
S2[A] from FINSET_1:sch 2(A1, A4, A5);
then ex X being set st
( X = A & union X is finite ) by A3;
hence union A is finite ; :: thesis: verum