let X be LinearTopSpace; :: thesis: for F being Subset-Family of X st F is finite & F = { P where P is bounded Subset of X : verum } holds
union F is bounded
let F be Subset-Family of X; :: thesis: ( F is finite & F = { P where P is bounded Subset of X : verum } implies union F is bounded )
assume that
A1: F is finite and
A2: F = { P where P is bounded Subset of X : verum } ; :: thesis: union F is bounded
defpred S1[ set ] means ex A being Subset of X st
( A = union $1 & A is bounded );
A3: now :: thesis: for P being Subset of X st P in F holds
P is bounded
let P be Subset of X; :: thesis: ( P in F implies P is bounded )
assume P in F ; :: thesis: P is bounded
then ex A being bounded Subset of X st P = A by A2;
hence P is bounded ; :: thesis: verum
end;
A4: for x, B being set st x in F & B c= F & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in F & B c= F & S1[B] implies S1[B \/ {x}] )
assume that
A5: x in F and
B c= F and
A6: S1[B] ; :: thesis: S1[B \/ {x}]
consider A being Subset of X such that
A7: ( A = union B & A is bounded ) by A6;
reconsider x = x as Subset of X by A5;
A8: union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:78
.= (union B) \/ x by ZFMISC_1:25 ;
A9: x is bounded by A3, A5;
ex Y being Subset of X st
( Y = union (B \/ {x}) & Y is bounded )
proof
take A \/ x ; :: thesis: ( A \/ x = union (B \/ {x}) & A \/ x is bounded )
thus ( A \/ x = union (B \/ {x}) & A \/ x is bounded ) by A7, A8, A9, Th41; :: thesis: verum
end;
hence S1[B \/ {x}] ; :: thesis: verum
end;
{} X = union {} by ZFMISC_1:2;
then A10: S1[ {} ] ;
S1[F] from FINSET_1:sch 2(A1, A10, A4);
hence union F is bounded ; :: thesis: verum