let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being set st P = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } holds
( P is non empty Subset-Family of X & S c= P )
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: for P being set st P = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } holds
( P is non empty Subset-Family of X & S c= P )
let P be set ; :: thesis: ( P = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } implies ( P is non empty Subset-Family of X & S c= P ) )
assume A1: P = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } ; :: thesis: ( P is non empty Subset-Family of X & S c= P )
reconsider E0 = {} as Subset of X by XBOOLE_1:2;
reconsider g0 = <*E0*> as disjoint_valued FinSequence by TTT1;
now :: thesis: for i being Nat st i in dom g0 holds
g0 . i in S
let i be Nat; :: thesis: ( i in dom g0 implies g0 . i in S )
assume i in dom g0 ; :: thesis: g0 . i in S
then i in Seg 1 by FINSEQ_1:38;
then i = 1 by TARSKI:def 1, FINSEQ_1:2;
then g0 . i = E0 by FINSEQ_1:40;
hence g0 . i in S by SETFAM_1:def 8; :: thesis: verum
end;
then reconsider g0 = g0 as disjoint_valued FinSequence of S by FINSEQ_2:12;
Union g0 = union {E0} by FINSEQ_1:38;
then A5: {} in P by A1;
now :: thesis: for x being object st x in P holds
x in bool X
let x be object ; :: thesis: ( x in P implies x in bool X )
assume x in P ; :: thesis: x in bool X
then ex A being Subset of X st
( x = A & ex F being disjoint_valued FinSequence of S st A = Union F ) by A1;
hence x in bool X ; :: thesis: verum
end;
hence P is non empty Subset-Family of X by A5, TARSKI:def 3; :: thesis: S c= P
now :: thesis: for x being object st x in S holds
x in P
let x be object ; :: thesis: ( x in S implies x in P )
assume A5: x in S ; :: thesis: x in P
then reconsider x1 = x as Subset of X ;
set g = <*x1*>;
A3: rng <*x1*> = {x1} by FINSEQ_1:38;
reconsider g = <*x1*> as disjoint_valued FinSequence by TTT1;
now :: thesis: for y being object st y in rng g holds
y in S
let y be object ; :: thesis: ( y in rng g implies y in S )
assume y in rng g ; :: thesis: y in S
then consider i being object such that
B1: ( i in dom g & y = g . i ) by FUNCT_1:def 3;
reconsider i = i as Element of NAT by B1;
i in Seg 1 by B1, FINSEQ_1:38;
then i = 1 by TARSKI:def 1, FINSEQ_1:2;
hence y in S by B1, A5, FINSEQ_1:40; :: thesis: verum
end;
then rng g c= S ;
then reconsider g = g as disjoint_valued FinSequence of S by FINSEQ_1:def 4;
Union g = x by A3;
hence x in P by A1; :: thesis: verum
end;
hence S c= P ; :: thesis: verum