:: Semiring of Sets
:: by Roland Coghetto
::
:: Received March 31, 2014
:: Copyright (c) 2014-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_1, ARYTM_3, CARD_3, EQREL_1, FINSEQ_1, FINSET_1, FINSUB_1,
FUNCT_1, NAT_1, NAT_LAT, NUMBERS, ORDINAL1, ORDINAL4, RELAT_1, SETFAM_1,
SIMPLEX0, SRINGS_1, SUBSET_1, TARSKI, TAXONOM2, XBOOLE_0, XCMPLX_0,
XXREAL_0, ZFMISC_1, CARD_1, LATTICE7, PARTIT1, TEX_1;
notations TARSKI, XBOOLE_0, SUBSET_1, EQREL_1, SETFAM_1, FINSET_1, ORDINAL1,
CARD_3, RELAT_1, ZFMISC_1, FINSUB_1, FUNCT_1, SIMPLEX0, FINSEQ_1,
NUMBERS, XXREAL_0, FUNCT_2, NAT_LAT, XXREAL_3, RELSET_1, TAXONOM2, NAT_1,
TEX_1, LATTICE7, PARTIT1, CARD_1;
constructors LATTICE5, NAT_LAT, RELSET_1, MEASURE6, TAXONOM2, COHSP_1,
LATTICE7, PARTIT1, TOPGEN_4, TEX_1;
registrations CARD_3, EQREL_1, FINSEQ_1, FINSET_1, FUNCT_1, INT_1, MEMBERED,
NAT_1, NAT_LAT, RELAT_1, RELSET_1, SIMPLEX0, SUBSET_1, XBOOLE_0, XREAL_0,
XXREAL_0, XXREAL_3, SETFAM_1, COHSP_1, ORDINAL1, CARD_1, ZFMISC_1;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions TARSKI, XBOOLE_0, FINSUB_1;
equalities CARD_3, FINSEQ_1, TARSKI, PARTIT1, TEX_1;
expansions XBOOLE_0, FINSUB_1;
theorems CARD_3, CARD_4, CHORD, EQREL_1, FINSEQ_1, FINSET_1, FINSUB_1,
FUNCT_1, FUNCT_2, INT_1, NAT_1, NAT_LAT, ORDINAL1, RELAT_1, RELSET_1,
SETFAM_1, SUBSET_1, TARSKI, TAXONOM2, XBOOLE_0, XBOOLE_1, XREAL_1,
XTUPLE_0, XXREAL_0, ZFMISC_1, CARD_2, COHSP_1, LATTICE7, PARTIT1,
TOPGEN_4;
schemes FINSEQ_2, FUNCT_1, NAT_1;
begin :: Preliminaries
reserve X for set;
reserve S for Subset-Family of X;
theorem Lem1: for X,Y be set holds (X\/Y)\(Y\X)=X
proof
let X,Y be set;
A3: X\/(X/\Y) = X by XBOOLE_1:22;
A4: X\(Y\X)=(X\Y)\/ X/\X by XBOOLE_1:52
.=X by XBOOLE_1:7,8;
Y\(Y\X)=(Y\Y)\/ Y/\X by XBOOLE_1:52
.={} \/ (Y/\X) by XBOOLE_1:37
.=X/\Y;
hence thesis by XBOOLE_1:42,A3,A4;
end;
registration
let X,S;
let S1,S2 be finite Subset of S;
cluster INTERSECTION(S1,S2) -> finite;
coherence
proof
S1 is finite Subset-Family of X & S2 is finite Subset-Family of X
by XBOOLE_1:1;
then card INTERSECTION(S1,S2) c= card [:S1,S2:] by TOPGEN_4:25;
hence thesis;
end;
end;
theorem ThmVAL1:
for S be Subset-Family of X, A be Element of S holds
{x where x is Element of S: x in union (PARTITIONS(A)/\Fin S)} =
union (PARTITIONS(A)/\Fin S)
proof
let S be Subset-Family of X, A be Element of S;
thus {x where x is Element of S: x in union (PARTITIONS(A)/\Fin S)} c=
union (PARTITIONS(A)/\Fin S)
proof
let u be object;
assume u in {x where x is Element of S:
x in union (PARTITIONS(A)/\Fin S)};
then ex x be Element of S st u=x & x in union (PARTITIONS(A)/\Fin S);
hence thesis;
end;
let u be object;
assume
A5A:u in union(PARTITIONS(A)/\Fin S);
then consider v be set such that
A6: u in v and
A7: v in PARTITIONS(A)/\Fin S by TARSKI:def 4;
v in Fin S by A7,XBOOLE_0:def 4;
then v c= S by FINSUB_1:def 5;
hence thesis by A5A,A6;
end;
A4bis: PARTITIONS({})={{}}
proof
thus PARTITIONS({}) c= {{}}
proof
let x be object;
assume x in PARTITIONS({});
then x is a_partition of {} by PARTIT1:def 3;
then x={};
hence thesis by TARSKI:def 1;
end;
let x be object;
{} in PARTITIONS({}) by EQREL_1:45,PARTIT1:def 3;
hence thesis by TARSKI:def 1;
end;
registration
let X,S;
cluster union (PARTITIONS({})/\Fin S) -> empty;
coherence
proof
{{}}/\Fin S = {{}}
proof
thus {{}}/\Fin S c= {{}} by XBOOLE_1:17;
{{}} c= Fin S
proof
let x be object;
assume x in {{}}; then
J1: x={} by TARSKI:def 1;
{} c= S & {} is finite by XBOOLE_1:2;
hence thesis by J1,FINSUB_1:def 5;
end;
hence thesis by XBOOLE_1:19;
end;
hence thesis by A4bis;
end;
end;
registration
let X;
cluster cobool X -> with_empty_element;
coherence
proof
{} in cobool X by TARSKI:def 2;
hence thesis;
end;
end;
Lem3:
for S be Subset-Family of X st
(for A,B be Element of S st A\B is non empty
ex P be finite Subset of S st P is a_partition of A\B)
holds
(for A,B be Element of S
ex P be finite Subset of S st P is a_partition of A\B)
proof
let S be Subset-Family of X;
assume
A1: for A,B be Element of S st A\B is non empty
ex P be finite Subset of S st P is a_partition of A\B;
let S1,S2 be Element of S;
per cases;
suppose
A2: S1\S2 is empty;
{} is finite Subset of S & {} is a_partition of {}
by SUBSET_1:1,EQREL_1:45;
hence thesis by A2;
end;
suppose S1\S2 is non empty;
hence thesis by A1;
end;
end;
Lem4:
(for A,B be Element of cobool X st A/\B is non empty
ex P be finite Subset of cobool X st P is a_partition of A/\B) &
(for A,B be Element of cobool X st B c= A
ex P be finite Subset of cobool X st P is a_partition of A\B) &
(for A,B be Element of cobool X st A\B is non empty
ex P be finite Subset of cobool X st P is a_partition of A\B) &
{X} is countable Subset of cobool X & union {X}=X
proof
set S = cobool X;
A2: ex y be finite Subset of S st y is a_partition of X
proof
per cases;
suppose X is non empty; then
A3: {X} is a_partition of X by EQREL_1:39;
{X} is finite Subset of S by ZFMISC_1:7;
hence thesis by A3;
end;
suppose
A4: X is empty;
{} is finite Subset of {{},{}} by SUBSET_1:1;
hence thesis by EQREL_1:45,A4;
end;
end;
thus for A,B be Element of S st A/\B is non empty holds
ex P be finite Subset of S st P is a_partition of A/\B
proof
let S1,S2 be Element of S;
A7: S1={} or S1=X by TARSKI:def 2;
S2={} or S2=X by TARSKI:def 2;
hence thesis by A2,A7;
end;
for S1,S2 be Element of S st S1\S2 is non empty
ex P be finite Subset of S st P is a_partition of S1\S2
proof
let S1,S2 be Element of S;
A10: S1={} or S1=X by TARSKI:def 2;
S2={} or S2=X by TARSKI:def 2;
hence thesis by A2,A10,XBOOLE_1:37;
end;
hence thesis by ZFMISC_1:7,Lem3;
end;
Lem5:
for A,B be Element of S, p be finite Subset of S st
B<>{} & B c= A & p is a_partition of A\B
holds
{B}\/p is a_partition of A
proof
let A,B be Element of S;
let p be finite Subset of S;
assume
A1: B <>{};
assume
A2: B c= A;
assume
A3: p is a_partition of A\B;
A4: {B}\/p is Subset-Family of A
proof
A5: p c= bool A
proof
bool (A\B) c= bool A by ZFMISC_1:67;
hence thesis by A3,XBOOLE_1:1;
end;
{B} c= bool A
proof
A6: {B} c= bool B by ZFMISC_1:68;
bool B c= bool A by A2,ZFMISC_1:67;
hence thesis by A6,XBOOLE_1:1;
end;
hence thesis by A5,XBOOLE_1:8;
end;
A7: union({B}\/p)=A
proof
union({B}\/p)=union({B})\/union p by ZFMISC_1:78
.=B\/(A\B) by A3,EQREL_1:def 4
.=A\/B by XBOOLE_1:39;
hence thesis by A2,XBOOLE_1:12;
end;
for a be Subset of A st a in {B}\/p holds a<>{} &
for b be Subset of A st b in {B}\/p holds a=b or a misses b
proof
let a be Subset of A;
assume
A8: a in {B}\/p;
then
A9: a in {B} or a in p by XBOOLE_0:def 3;
thus a<>{} by A1,A3,A8;
thus for b be Subset of A st b in {B}\/p holds a=b or a misses b
proof
let b be Subset of A;
assume b in {B}\/p;
then b in {B} or b in p by XBOOLE_0:def 3; then
A10: (a=B & b=B) or (a=B & b in p) or (a in p & b=B) or (a in p & b in p)
by A9,TARSKI:def 1;
A11: a=B & b in p implies a misses b
proof
assume
A12: a=B & b in p;
A\B misses B by XBOOLE_1:85;
hence thesis by A3,A12,XBOOLE_1:63;
end;
a in p & b=B implies a misses b
proof
assume
A14: a in p & b=B;
A\B misses B by XBOOLE_1:85;
hence thesis by A3,A14,XBOOLE_1:63;
end;
hence thesis by A3,A10,A11,EQREL_1:def 4;
end;
end;
hence thesis by A4,A7,EQREL_1:def 4;
end;
theorem thmIL:
for X be set st X is cap-closed cup-closed holds
X is Ring_of_sets
proof
let X be set;
assume X is cap-closed cup-closed;
then for x,y be set st x in X & y in X holds x/\y in X & x\/y in X;
hence thesis by COHSP_1:def 7,LATTICE7:def 8;
end;
begin :: The Existence of Partitions
Lem6:
for S be non empty Subset-Family of X st
(for A,B be Element of S holds
ex P be finite Subset of S st P is a_partition of A/\B) &
(for C,D be Element of S st D c= C holds
ex P be finite Subset of S st P is a_partition of C\D)
holds (for A be Element of S, Q be finite Subset of S st
A is non empty & union Q c= A & Q is a_partition of union Q
ex R be finite Subset of S st union R misses union Q &
Q\/R is a_partition of A)
proof
let S be non empty Subset-Family of X;
assume
A1: for A,B be Element of S holds
ex P be finite Subset of S st P is a_partition of A/\B;
assume
A2: for C,D be Element of S st D c= C holds
ex P be finite Subset of S st P is a_partition of C\D;
let A be Element of S;
let Q be finite Subset of S;
assume that
A3: A is non empty and
A4: union Q c= A and
A5: Q is a_partition of union Q;
consider qq be FinSequence such that
A6: Q = rng qq by FINSEQ_1:52;
A7: for i be set st i in dom qq holds qq.i <> {}
proof
let i be set;
assume i in dom qq;
then qq.i in Q by A6,FUNCT_1:def 3;
hence thesis by A5;
end;
per cases;
suppose
A8: qq={}; then
A9: Q={} by A6;
A10: {A} is finite Subset of S by SUBSET_1:33;
A11: {A} is a_partition of A by A3,EQREL_1:39;
A12: union {A} misses union Q
proof
union Q = {} by A8,A6,ZFMISC_1:2;
hence thesis;
end;
{}\/{A} = {A};
hence thesis by A9,A10,A11,A12;
end;
suppose
A13: qq<>{};
defpred P[Nat] means
for n be Nat st $1=n & 1 <= n & n <= len qq holds
ex R be finite Subset of S st
union R misses union (rng (qq|Seg n)) &
(rng (qq|Seg n))\/R is a_partition of A;
A14: P[1]
proof
let n be Nat;
assume
A15: n=1 & 1<=n & n<=len qq;
A16: 1 in Seg len qq by A15; then
A17: 1 in dom qq by FINSEQ_1:def 3; then
A18: rng (qq|Seg 1) = {qq.1} by FINSEQ_1:2,FUNCT_1:98;
A19: qq.1 c= A
proof
qq.1 in Q by A6,A17,FUNCT_1:def 3;
then qq.1 c= union Q by ZFMISC_1:74;
hence thesis by A4,XBOOLE_1:1;
end;
A20: qq.1 is Element of S
proof
1 in dom qq by A16,FINSEQ_1:def 3;
then qq.1 in rng qq by FUNCT_1:def 3;
hence thesis by A6;
end;
then consider PP be finite Subset of S such that
A21: PP is a_partition of A \ qq.1 by A2,A19;
A21a: union PP misses qq.1
proof
union PP = A \ (qq.1) by A21,EQREL_1:def 4;
hence thesis by XBOOLE_1:79;
end;
{qq.1}\/PP is a_partition of A by A17,A7,A19,A20,A21,Lem5;
hence thesis by A15,A18,A21a;
end;
A23: for j being Nat st 1 <= j holds P[j] implies P[(j+1)]
proof
let j be Nat;
assume that
A24: 1<=j and
A25: P[j];
for n be Nat st j+1=n & 1 <= n & n <= len qq holds
ex R be finite Subset of S st
union R misses union(rng (qq|Seg n)) &
(rng (qq|Seg n))\/R is a_partition of A
proof
let n be Nat;
assume that
A26: j+1=n and
A27: 1<=n and
A28: n<= len qq;
per cases;
suppose j <= len qq;
then consider R1 be finite Subset of S such that
A29: union R1 misses union (rng (qq|Seg j)) and
A30: (rng(qq|Seg j))\/R1 is a_partition of A by A24,A25;
A31: n in Seg len qq by A27,A28;
then
A32: j+1 in dom qq by A26,FINSEQ_1:def 3;
Seg (j+1) = Seg j \/ {j+1} by FINSEQ_1:9;
then qq|Seg (j+1) = qq|Seg j \/ qq|{j+1} by RELAT_1:78;
then
A33: rng (qq|Seg (j+1)) = rng (qq|Seg j) \/ rng (qq|{j+1})
by RELAT_1:12; then
A34: rng (qq|Seg (j+1)) = rng (qq|Seg j) \/ {qq.(j+1)}
by A32,FUNCT_1:98;
per cases;
suppose qq.(j+1) in (rng (qq|Seg j));
then rng (qq|Seg j) \/ {qq.(j+1)}=rng (qq|Seg j)
by ZFMISC_1:31,XBOOLE_1:12;
then
rng(qq|Seg(j+1))=(rng (qq|Seg j)) by A33,A32,FUNCT_1:98;
hence thesis by A26,A29,A30;
end;
suppose
A35: not qq.(j+1) in (rng (qq|Seg j));
A36: qq.(j+1) misses union(rng (qq|Seg j))
proof
assume not qq.(j+1) /\ union(rng (qq|Seg j))={};
then consider x0 be object such that
A37: x0 in qq.(j+1) /\ union(rng (qq|Seg j)) by XBOOLE_0:def 1;
x0 in qq.(j+1) & x0 in Union(qq|Seg j) by A37,XBOOLE_0:def 4;
then consider y0 be set such that
A38: x0 in y0 & y0 in rng(qq|Seg j) by TARSKI:def 4;
consider j0 be object such that
A39: j0 in dom (qq|Seg j) and
A40: y0=(qq|Seg j).j0 by A38,FUNCT_1:def 3;
x0 in qq.j0 & x0 in qq.(j+1)
by A37,XBOOLE_0:def 4,A38,A40,A39,FUNCT_1:47;
then
A41: x0 in qq.j0/\qq.(j+1) by XBOOLE_0:def 4;
dom (qq|Seg j) c= dom qq by RELAT_1:60;
then j0 in dom qq & j+1 in dom qq
by A39,A31,A26,FINSEQ_1:def 3;
then qq.j0 in Q & qq.(j+1) in Q by A6,FUNCT_1:def 3;
then qq.j0=qq.(j+1)
by A5,A41,XBOOLE_0:def 7,EQREL_1:def 4;
hence thesis by A35,A38,A40,A39,FUNCT_1:47;
end;
A42: qq.(j+1) in Q by A32,A6,FUNCT_1:def 3; then
A43: qq.(j+1) c= union Q by ZFMISC_1:74; then
A44: qq.(j+1) c= A by A4,XBOOLE_1:1;
consider RA be finite Subset of S such that
A45: RA is a_partition of A\qq.(j+1)
by A42,A43,A4,XBOOLE_1:1,A2;
A46: for x be set st x in [:R1,RA:] holds
ex x1,x2 be set, px be finite Subset of S st
x=[x1,x2] & x1 in R1 & x2 in RA &
px is a_partition of x1/\x2
proof
let x be set;
assume x in [:R1,RA:];
then consider x1,x2 be object such that
A47: x1 in R1 & x2 in RA & x=[x1,x2] by ZFMISC_1:def 2;
reconsider x1,x2 as set by TARSKI:1;
consider px be finite Subset of S such that
A48: px is a_partition of x1/\x2 by A47,A1;
thus thesis by A47,A48;
end;
defpred H[object,object] means
$1 in [:R1,RA:] &
ex x1,x2 be set, px be finite Subset of S st
$1=[x1,x2] &
x1 in R1 & x2 in RA &
$2 = px &
$2 is a_partition of x1/\x2;
set XA = the set of all x where x is finite Subset of S;
A49: for x be object st x in [:R1,RA:]
ex y be object st y in XA & H[x,y]
proof
let x be object;
assume
A50: x in [:R1,RA:];
then consider x1,x2 be set, px be finite Subset of S such that
A51: x=[x1,x2] and
A52: x1 in R1 & x2 in RA and
A53: px is a_partition of x1/\x2 by A46;
px in XA;
hence thesis by A50,A51,A52,A53;
end;
consider h be Function such that
A55: dom h = [:R1,RA:] & rng h c= XA and
A56: for x being object st x in [:R1,RA:] holds H[x,h.x]
from FUNCT_1:sch 6(A49);
A57: Union h is finite
proof
for x be set st x in rng h holds x is finite
proof
let x be set;
assume x in rng h;
then consider x0 be object such that
A58: x0 in dom h and
A59: x=h.x0 by FUNCT_1:def 3;
consider x1,x2 be set,
px be finite Subset of S such that
x0=[x1,x2] and
x1 in R1 & x2 in RA and
A60: x=px and
x is a_partition of x1/\x2 by A58,A59,A55,A56;
thus thesis by A60;
end;
hence thesis by A55,FINSET_1:7,FINSET_1:8;
end;
A61: rng h c= bool S
proof
let x be object;
assume x in rng h;
then consider x0 be object such that
A62: x0 in dom h and
A63: x=h.x0 by FUNCT_1:def 3;
consider x1,x2 be set,
px be finite Subset of S such that
x0=[x1,x2] and
x1 in R1 & x2 in RA and
A64: x=px and
x is a_partition of x1/\x2 by A62,A63,A55,A56;
thus thesis by A64;
end;
A65: Union h c= S
proof
let x be object;
assume x in Union h;
then ex x0 be set st x in x0 & x0 in rng h by TARSKI:def 4;
hence thesis by A61;
end;
A68: union Union h misses union rng(qq|Seg(n))
proof
union Union h /\ union rng(qq|Seg(j+1)) c= {}
proof
let x be object;
assume x in union Union h /\ union rng(qq|Seg(j+1)); then
A69: x in union Union h & x in union rng(qq|Seg(j+1))
by XBOOLE_0:def 4;
then consider x0 be set such that
A70: x in x0 and
A71: x0 in Union h by TARSKI:def 4;
consider x1 be set such that
A72: x in x1 and
A73: x1 in rng(qq|Seg(j+1)) by A69,TARSKI:def 4;
x0/\x1={}
proof
x0/\x1 c= {}
proof
let u be object;
assume
A74: u in x0/\x1; then
A75: u in x0 & u in x1 by XBOOLE_0:def 4;
consider x0a be set such that
A76: x0 in x0a and
A77: x0a in rng h by A71,TARSKI:def 4;
consider t be object such that
A78: t in dom h and
A79: h.t=x0a by A77,FUNCT_1:def 3;
consider ax1,ax2 be set,
apx be finite Subset of S such that
t=[ax1,ax2] and
A80: ax1 in R1 & ax2 in RA and
A81: x0a = apx and
A82: x0a is a_partition of ax1/\ax2
by A78,A79,A55,A56;
A83: u in x0 & x0 in apx by A74,XBOOLE_0:def 4,A76,A81;
u in ax1 & ax1 in R1
by A83,A82,A81,A80,XBOOLE_0:def 4;
then u in union R1 by TARSKI:def 4; then
A85: not u in union rng (qq|Seg j) by A29,XBOOLE_0:def 4;
u in ax2 & ax2 in RA
by A83,A82,A81,XBOOLE_0:def 4,A80; then
A85a: not u in qq.(j+1) by A45,XBOOLE_0:def 5;
union rng (qq|Seg (j+1)) =
union (rng (qq|Seg j) \/ {qq.(j+1)})
by A33,A32,FUNCT_1:98;
then union rng (qq|Seg (j+1)) =
union (rng (qq|Seg j)) \/ union {qq.(j+1)}
by ZFMISC_1:78; then
not u in union rng(qq|Seg(j+1))
by A85,XBOOLE_0:def 3,A85a;
hence thesis by A75,A73,TARSKI:def 4;
end;
hence thesis;
end;
hence thesis by A70,A72,XBOOLE_0:def 4;
end;
hence thesis by A26;
end;
rng(qq|Seg(n))\/ Union h is a_partition of A
proof
A87: rng(qq|Seg(n))\/ Union h c= bool A
proof
let x be object;
assume
A88: x in rng(qq|Seg(n))\/ Union h;
A89: x in rng(qq|Seg(n)) implies x in bool A
proof
assume x in rng(qq|Seg(n)); then
x in rng(qq|Seg(j)) \/ {qq.(j+1)}
by A26,A33,A32,FUNCT_1:98;
then x in rng(qq|Seg(j)) or x in {qq.(j+1)}
by XBOOLE_0:def 3; then
A90: x in rng(qq|Seg(j)) or x = qq.(j+1) by TARSKI:def 1;
x in rng(qq|Seg j) implies x in bool A
proof
assume x in rng(qq|Seg j);
then x in rng(qq|Seg j)\/R1 by XBOOLE_1:7,TARSKI:def 3;
hence thesis by A30;
end;
hence thesis by A90,A44;
end;
x in Union h implies x in bool A
proof
assume x in Union h;
then consider y be set such that
A91: x in y and
A92: y in rng h by TARSKI:def 4;
consider z be object such that
A93: z in dom h and
A94: y=h.z by A92,FUNCT_1:def 3;
consider x1,x2 be set,
px be finite Subset of S such that
z=[x1,x2] and
A95: x1 in R1 & x2 in RA and
y=px and
A96: y is a_partition of x1/\x2 by A55,A56,A93,A94;
A97: x1/\x2 c= x2 by XBOOLE_1:17;
A\qq.(j+1) c= A by XBOOLE_1:36;
then x2 c= A by A45,A95,XBOOLE_1:1;
then x1/\x2 c= A by A97,XBOOLE_1:1;
then bool (x1/\x2) c= bool A by ZFMISC_1:67;
then y c= bool A by A96,XBOOLE_1:1;
hence thesis by A91;
end;
hence thesis by A88,A89,XBOOLE_0:def 3;
end;
A98: union (rng(qq|Seg(n))\/ Union h)=A
proof
A99: union (rng(qq|Seg(n))\/ Union h) c= A
proof
let x be object;
assume x in union (rng(qq|Seg(n))\/ Union h);
then consider y be set such that
A100: x in y and
A101: y in rng(qq|Seg(n))\/ Union h by TARSKI:def 4;
thus thesis by A100,A87,A101;
end;
A c= union (rng(qq|Seg(n))\/ Union h)
proof
let x be object;
assume x in A;
then x in union (rng(qq|Seg(j))\/ R1) by A30,EQREL_1:def 4;
then
A102: x in (union rng(qq|Seg(j)))\/ union R1 by ZFMISC_1:78;
A103: x in union rng(qq|Seg j) implies
x in union rng(qq|Seg (j+1))
proof
assume
A104: x in union rng(qq|Seg j);
union rng (qq|Seg j) c= union rng (qq|Seg (j+1))
by ZFMISC_1:77,A33,XBOOLE_1:7;
hence thesis by A104;
end;
x in union R1 implies x in union Union h or
x in union rng(qq|Seg(j+1))
proof
assume
A105: x in union R1;
union R1 c= union R1 \/ union rng(qq|Seg j)
by XBOOLE_1:7;
then union R1 c= union (R1\/rng(qq|Seg j))
by ZFMISC_1:78; then
A106: union R1 c= A by A30,EQREL_1:def 4;
A107: x in qq.(j+1) implies x in union rng (qq|Seg(j+1))
proof
assume
A108: x in qq.(j+1);
union rng (qq|Seg (j+1)) =
union (rng (qq|Seg j) \/ {qq.(j+1)})
by A33,A32,FUNCT_1:98; then
A108aa: union (rng (qq|Seg (j+1))) =
union rng (qq|Seg j) \/
union {qq.(j+1)} by ZFMISC_1:78;
qq.(j+1) c= union rng (qq|Seg (j+1))
by A108aa,XBOOLE_1:7;
hence thesis by A108;
end;
not x in qq.(j+1) implies x in union Union h
proof
assume not x in qq.(j+1);
then x in A\qq.(j+1) by A105,A106,XBOOLE_0:def 5;
then x in union RA by A45,EQREL_1:def 4;
then consider y be set such that
A109: x in y and
A110: y in RA by TARSKI:def 4;
consider z be set such that
A111: x in z and
A112: z in R1 by A105,TARSKI:def 4;
consider t be set such that
A113: t=[z,y];
A114: [z,y] in [:R1,RA:] by A110,A112,ZFMISC_1:def 2;
A115: [z,y] in dom h by A110,A112,ZFMISC_1:def 2,A55;
consider x1,x2 be set,
px be finite Subset of S such that
A116: t=[x1,x2] and
x1 in R1 & x2 in RA and
h.t=px and
A117: h.t is a_partition of x1/\x2 by A113,A56,A114;
A118: z=x1 & y=x2 by A113,A116,XTUPLE_0:1;
x in z/\y by A109,A111,XBOOLE_0:def 4; then
A119: x in union (h.t) by A117,A118,EQREL_1:def 4;
h.t in rng h by A113,A115,FUNCT_1:def 3;
then union (h.t) c= union union rng h
by ZFMISC_1:74,ZFMISC_1:77;
hence thesis by A119;
end;
hence thesis by A107;
end;
then x in union rng(qq|Seg(j+1)) \/ union Union h
by A102,A103,XBOOLE_0:def 3;
hence thesis by ZFMISC_1:78,A26;
end;
hence thesis by A99;
end;
for a be Subset of A st a in rng(qq|Seg(n))\/ Union h holds
a<>{} &
for b be Subset of A st b in rng(qq|Seg(n))\/ Union h holds
a=b or a misses b
proof
let a be Subset of A;
assume
A120: a in rng(qq|Seg(n))\/ Union h;
A121: a in rng (qq|Seg j) \/ {qq.(j+1)} or
a in Union h by A34,A120,A26,XBOOLE_0:def 3;
A122: a<>{}
proof
A123: a in rng (qq|Seg (j+1)) implies a<>{}
proof
assume a in rng(qq|Seg(j+1)); then
A124: a in rng (qq|Seg j) \/ {qq.(j+1)} by A33,A32,FUNCT_1:98;
A125: a in rng(qq|Seg j) implies a<>{}
proof
assume
A126: a in rng(qq|Seg j);
rng(qq|Seg j) c= rng(qq|Seg j) \/ R1 by XBOOLE_1:7;
hence thesis by A126,A30;
end;
a in {qq.(j+1)} implies a<>{}
proof
assume a in {qq.(j+1)};
then a=qq.(j+1) by TARSKI:def 1;
hence thesis by A7,A32;
end;
hence thesis by A124,A125,XBOOLE_0:def 3;
end;
a in Union h implies a<>{}
proof
assume a in Union h;
then consider a1 be set such that
A127: a in a1 and
A128: a1 in rng h by TARSKI:def 4;
consider a2 be object such that
A129: a2 in dom h and
A130: a1=h.a2 by A128,FUNCT_1:def 3;
consider x1,x2 be set,
px be finite Subset of S such that
a2=[x1,x2] & x1 in R1 & x2 in RA & a1=px and
A131: a1 is a_partition of x1/\x2 by A129,A55,A56,A130;
thus thesis by A127,A131;
end;
hence thesis by A120,A26,XBOOLE_0:def 3,A123;
end;
for b be Subset of A st
b in rng(qq|Seg(n))\/ Union h holds
a=b or a misses b
proof
let b be Subset of A;
assume b in rng(qq|Seg(n))\/Union h; then
b in rng(qq|Seg(j+1)) or b in Union h
by A26,XBOOLE_0:def 3; then
A132: b in rng (qq|Seg j) \/ {qq.(j+1)} or b in Union h
by A33,A32,FUNCT_1:98;
A133: b in rng (qq|Seg (j)) implies a=b or a misses b
proof
assume
A134: b in rng(qq|Seg j); then
A135: b in rng(qq|Seg j) \/ R1 by XBOOLE_1:7,TARSKI:def 3;
A136: a in rng(qq|Seg j) implies a=b or a misses b
proof
assume a in rng(qq|Seg j);
then a in rng(qq|Seg j) \/ R1
by XBOOLE_1:7,TARSKI:def 3;
hence thesis by A135,A30,EQREL_1:def 4;
end;
A137: a in {qq.(j+1)} implies a=b or a misses b
proof
assume a in {qq.(j+1)}; then
a misses Union (qq|Seg j) by A36,TARSKI:def 1;
hence thesis by XBOOLE_1:63,A134,ZFMISC_1:74;
end;
a in Union h implies a=b or a misses b
proof
assume a in Union h; then
A138: a c= union Union h by ZFMISC_1:74;
rng(qq|Seg j) c= rng (qq|Seg(j+1)) by A33,XBOOLE_1:7;
then b c= union rng(qq|Seg n) by A134,A26,ZFMISC_1:74;
hence thesis by A138,A68,XBOOLE_1:64;
end;
hence thesis by A121,XBOOLE_0:def 3,A136,A137;
end;
A139: b in {qq.(j+1)} implies a=b or a misses b
proof
assume
A140: b in {qq.(j+1)};
A141: a in rng(qq|Seg j) implies a=b or a misses b
proof
assume
A142: a in rng(qq|Seg j);
b misses Union (qq|Seg j) by A140,TARSKI:def 1,A36;
hence thesis by A142,ZFMISC_1:74,XBOOLE_1:63;
end;
A143: a in {qq.(j+1)} implies a=b or a misses b
proof
assume a in {qq.(j+1)};
then a=qq.(j+1) & b=qq.(j+1) by A140,TARSKI:def 1;
hence thesis;
end;
a in Union h implies a=b or a misses b
proof
assume a in Union h;
then consider a1 be set such that
A144: a in a1 and
A145: a1 in rng h by TARSKI:def 4;
consider t be object such that
A146: t in dom h and
A147: a1=h.t by A145,FUNCT_1:def 3;
consider x1,x2 be set,
px be finite Subset of S such that
t=[x1,x2] and
A148: x1 in R1 & x2 in RA and
a1=px and
A149: a1 is a_partition of x1/\x2 by A146,A147,A55,A56;
x1/\x2 c= x2 by XBOOLE_1:17;
then x1/\x2 c= A\qq.(j+1) by A45,A148,XBOOLE_1:1;
then
A150: bool (x1/\x2) c= bool (A\qq.(j+1))
by ZFMISC_1:67;
A151: a1 c= bool (A\qq.(j+1)) by A149,A150,XBOOLE_1:1;
b=qq.(j+1) by A140,TARSKI:def 1;
hence thesis by A151,A144,XBOOLE_1:63,XBOOLE_1:79;
end;
hence thesis by A121,XBOOLE_0:def 3,A141,A143;
end;
b in Union h implies a=b or a misses b
proof
assume
A152: b in Union h;
A153: a in rng(qq|Seg j) implies a=b or a misses b
proof
assume
A154: a in rng(qq|Seg j);
A155: b c= union Union h by A152,ZFMISC_1:74;
rng(qq|Seg j) c= rng (qq|Seg(j+1)) by A33,XBOOLE_1:7;
then a c= union rng(qq|Seg n) by A154,A26,ZFMISC_1:74;
hence thesis by A155,A68,XBOOLE_1:64;
end;
A156: a in {qq.(j+1)} implies a=b or a misses b
proof
assume a in {qq.(j+1)}; then
A157: a=qq.(j+1) by TARSKI:def 1;
consider b1 be set such that
A158: b in b1 and
A159: b1 in rng h by A152,TARSKI:def 4;
consider tb be object such that
A160: tb in dom h and
A161: b1=h.tb by A159,FUNCT_1:def 3;
consider bx1,bx2 be set,
bpx be finite Subset of S such that
tb=[bx1,bx2] and
A162: bx1 in R1 & bx2 in RA and
b1=bpx and
A163: b1 is a_partition of bx1/\bx2 by A160,A161,A55,A56;
A164: bool (bx1/\bx2) c= bool bx2
by XBOOLE_1:17,ZFMISC_1:67;
b1 c= bool bx2 by A163,A164,XBOOLE_1:1;
then b c= A\qq.(j+1) by A45,A162,A158,XBOOLE_1:1;
hence thesis by XBOOLE_1:79,A157,XBOOLE_1:63;
end;
a in Union h implies a=b or a misses b
proof
assume a in Union h;
then consider a1 be set such that
A166: a in a1 and
A167: a1 in rng h by TARSKI:def 4;
consider t be object such that
A168: t in dom h and
A169: a1=h.t by A167,FUNCT_1:def 3;
consider x1,x2 be set,
px be finite Subset of S such that
A170: t=[x1,x2] and
A171: x1 in R1 & x2 in RA and
a1=px and
A172: a1 is a_partition of x1/\x2 by A168,A169,A55,A56;
consider b1 be set such that
A173: b in b1 and
A174: b1 in rng h by A152,TARSKI:def 4;
consider tb be object such that
A175: tb in dom h and
A176: b1=h.tb by A174,FUNCT_1:def 3;
consider bx1,bx2 be set,
bpx be finite Subset of S such that
A177: tb=[bx1,bx2] and
A178: bx1 in R1 & bx2 in RA and
b1=bpx and
A179: b1 is a_partition of bx1/\bx2 by A175,A176,A55,A56;
A180: not x1=bx1 & not x2=bx2 implies thesis
proof
assume
A181: not x1=bx1 & not x2=bx2;
A182: x1 in rng(qq|Seg(j))\/R1 &
bx1 in rng(qq|Seg(j))\/R1
by A171,A178,XBOOLE_1:7,TARSKI:def 3;
A183: bool (x1/\x2) c= bool x1 &
bool (bx1/\bx2) c= bool bx1
by XBOOLE_1:17,ZFMISC_1:67;
a1 c= bool x1 & b1 c= bool bx1
by A172,A179,A183,XBOOLE_1:1;
hence thesis
by A182,A181,A30,EQREL_1:def 4,A166,A173,XBOOLE_1:64;
end;
A184: x1=bx1 & not x2=bx2 implies thesis
proof
assume
A185: x1=bx1 & not x2=bx2;
A186: bool (x1/\x2) c= bool x2 &
bool (bx1/\bx2) c= bool bx2
by XBOOLE_1:17,ZFMISC_1:67;
a1 c= bool x2 & b1 c= bool bx2
by A172,A179,A186,XBOOLE_1:1;
hence thesis by A166,A173,A185,A171,A178,A45,
EQREL_1:def 4,XBOOLE_1:64;
end;
not x1=bx1 & x2=bx2 implies thesis
proof
assume
A187: not x1=bx1 & x2=bx2;
A188: x1 in rng(qq|Seg(j))\/R1 &
bx1 in rng(qq|Seg(j))\/R1
by A171,A178,XBOOLE_1:7,TARSKI:def 3;
A189: bool (x1/\x2) c= bool x1 &
bool (bx1/\bx2) c= bool bx1
by XBOOLE_1:17,ZFMISC_1:67;
a1 c= bool x1 & b1 c= bool bx1
by A172,A179,A189,XBOOLE_1:1;
hence thesis by A166,A173,XBOOLE_1:64,A188,A187,
A30,EQREL_1:def 4;
end;
hence thesis by A169,A176,A170,A177,A166,A173,A172,
EQREL_1:def 4,A180,A184;
end;
hence thesis by A121,XBOOLE_0:def 3,A153,A156;
end;
hence thesis by A132,XBOOLE_0:def 3,A133,A139;
end;
hence thesis by A122;
end;
hence thesis by A87,A98,EQREL_1:def 4;
end;
hence thesis by A65,A57,A68;
end;
end;
suppose not j<=len qq;
hence thesis by A28,A26,XREAL_1:39;
end;
end;
hence thesis;
end;
A190: for i being Nat st 1<=i holds P[i] from NAT_1:sch 8(A14,A23);
A191: len qq is Nat & 1<=len qq by A13,FINSEQ_1:20;
consider R be finite Subset of S such that
A192: union R misses union (rng (qq|Seg len qq)) and
A193: (rng (qq|Seg len qq))\/R is a_partition of A by A190,A191;
rng (qq|Seg len qq)=Q
proof
rng (qq|Seg len qq)=rng (qq|dom qq) by FINSEQ_1:def 3
.=rng qq;
hence thesis by A6;
end;
hence thesis by A193,A192;
end;
end;
definition
let X be set;
let S be Subset-Family of X;
attr S is cap-finite-partition-closed means
:Defcap:
for S1,S2 be Element of S st S1/\S2 is non empty
ex x be finite Subset of S st x is a_partition of S1/\S2;
end;
registration
let X be set;
cluster cobool X -> cap-finite-partition-closed;
coherence by Lem4;
end;
registration
let X be set;
cluster cap-finite-partition-closed for Subset-Family of X;
existence
proof
take cobool X;
thus thesis;
end;
end;
registration
let X be set;
cluster cap-closed -> cap-finite-partition-closed for Subset-Family of X;
coherence
proof
let S be Subset-Family of X;
assume
A1: S is cap-closed;
for S1,S2 be Element of S st S1/\S2 is non empty
ex y be finite Subset of S st
y is a_partition of S1/\S2
proof
let S1,S2 be Element of S;
per cases;
suppose
A2: S is non empty;
assume
A3: S1/\S2 is non empty;
take {S1/\S2};
{S1/\S2} c= S
proof
let x be object;
assume x in {S1/\S2};
then x=S1/\S2 by TARSKI:def 1;
hence thesis by A1,A2;
end;
hence thesis by A3,EQREL_1:39;
end;
suppose S is empty;
then S1 is empty & S2 is empty by SUBSET_1:def 1;
hence thesis;
end;
end;
hence thesis;
end;
end;
Lem7:
for S be cap-finite-partition-closed Subset-Family of X holds
for S1,S2 be Element of S
ex P be finite Subset of S st P is a_partition of S1/\S2
proof
let S be cap-finite-partition-closed Subset-Family of X;
let S1,S2 be Element of S;
per cases;
suppose S1/\S2 is non empty;
then consider P be finite Subset of S such that
A1: P is a_partition of S1/\S2 by Defcap;
thus thesis by A1;
end;
suppose
A2: S1/\S2 is empty;
{} is finite Subset of S by SUBSET_1:1;
hence thesis by A2,EQREL_1:45;
end;
end;
Th1:
for X be set,
S be cap-finite-partition-closed Subset-Family of X,
P1,P2 be finite Subset of S holds
for y be non empty set st y in INTERSECTION(P1,P2)
ex P be finite Subset of S st P is a_partition of y
proof
let X be set,
S be cap-finite-partition-closed Subset-Family of X,
P1,P2 be finite Subset of S;
let y be non empty set;
assume
A1: y in INTERSECTION(P1,P2);
consider p1,p2 be set such that
A2: p1 in P1 & p2 in P2 & y=p1/\p2 by A1,SETFAM_1:def 5;
consider P be finite Subset of S such that
A3: P is a_partition of p1/\p2 by A2,Defcap;
thus thesis by A2,A3;
end;
theorem ThmJ1:
for A be non empty set,
S be cap-finite-partition-closed Subset-Family of X,
P1,P2 be a_partition of A st
P1 is finite Subset of S & P2 is finite Subset of S
ex P be a_partition of A st
P is finite Subset of S &
P '<' P1 '/\' P2
proof
let x be non empty set,
S be cap-finite-partition-closed Subset-Family of X;
let P1,P2 be a_partition of x;
assume that
A1: P1 is finite Subset of S and
A2: P2 is finite Subset of S;
defpred F[object,object] means
$1 in P1 '/\' P2 & $2 is finite Subset of S &
ex A be set st A = $1 & $2 is a_partition of A;
set FOUT={y where y is finite Subset of S: ex t be set st
t in P1 '/\' P2 & y is a_partition of t};
FOUT c= bool bool x
proof
let u be object;
assume u in FOUT;
then consider y be finite Subset of S such that
A3: u=y and
A4: ex t be set st t in P1 '/\' P2 & y is a_partition of t;
consider t0 be set such that
A5: t0 in P1 '/\' P2 and
A6: y is a_partition of t0 by A4;
reconsider u as set by TARSKI:1;
u c= bool x
proof
let v be object;
assume
A7: v in u;
A8: v in bool t0 by A3,A6,A7;
bool t0 c= bool x by A5,ZFMISC_1:67;
hence thesis by A8;
end;
hence thesis;
end;
then
A9: union FOUT c= union bool bool x by ZFMISC_1:77;
A10: for u be object st u in P1 '/\' P2 ex v be object st v in FOUT & F[u,v]
proof
let u be object;
assume
A11: u in P1 '/\' P2;
reconsider u as set by TARSKI:1;
consider P be finite Subset of S such that
A12: P is a_partition of u by A1,A2,A11,Th1;
A13: P in FOUT by A11,A12;
thus thesis by A11,A12,A13;
end;
consider f be Function such that
A14: dom f=P1 '/\' P2 & rng f c= FOUT and
A15: for x be object st x in P1 '/\' P2 holds F[x,f.x] from FUNCT_1:sch 6(A10);
A16: Union f is finite Subset of S
proof
A17: Union f c= S
proof
let u be object;
assume u in Union f;
then consider v be set such that
A18: u in v and
A19: v in rng f by TARSKI:def 4;
consider w be object such that
A20: w in P1 '/\' P2 & v=f.w by A14,A19,FUNCT_1:def 3;
v is Subset of S by A15,A20;
hence thesis by A18;
end;
Union f is finite
proof
for u be object st u in dom f holds f.u is finite by A14,A15;
hence thesis by A1,A2,A14,CARD_2:88;
end;
hence thesis by A17;
end;
A22: Union f is a_partition of x
proof
A23: Union f c= bool x
proof
A24: Union f c= union FOUT by A14,ZFMISC_1:77;
union FOUT c= bool x by A9,ZFMISC_1:81;
hence thesis by A24,XBOOLE_1:1;
end;
A25: union Union f = x
proof
thus union Union f c= x
proof
union Union f c= union bool x by A23,ZFMISC_1:77;
hence thesis by ZFMISC_1:81;
end;
thus x c= union Union f
proof
let a be object;
assume a in x; then
A27: a in union P1 & a in union P2 by EQREL_1:def 4;
consider b1 be set such that
A28: a in b1 and
A29: b1 in P1 by A27,TARSKI:def 4;
consider b2 be set such that
A30: a in b2 and
A31: b2 in P2 by A27,TARSKI:def 4;
A32: b1/\b2 in INTERSECTION(P1,P2) by A29,A31,SETFAM_1:def 5;
not b1/\b2 = {} by A28,A30,XBOOLE_0:def 4;
then
not b1/\b2 in {{}} by TARSKI:def 1;
then
A33: b1/\b2 in P1 '/\' P2 by A32,XBOOLE_0:def 5;
then F[b1/\b2,f.(b1/\b2)] by A15;
then union (f.(b1/\b2))=b1/\b2 by EQREL_1:def 4;
then
A34: a in union (f.(b1/\b2)) by A28,A30,XBOOLE_0:def 4;
A35: f.(b1/\b2) in rng f by A14,A33,FUNCT_1:def 3;
consider bb be set such that
A36: a in bb and
A37: bb in f.(b1/\b2) by A34,TARSKI:def 4;
bb in Union f by A35,A37,TARSKI:def 4;
hence thesis by A36,TARSKI:def 4;
end;
end;
for A be Subset of x st A in Union f holds
A <> {} &
for B be Subset of x st B in Union f holds
A = B or A misses B
proof
let A be Subset of x;
assume A in Union f;
then consider b be set such that
A38: A in b & b in rng f by TARSKI:def 4;
consider c be object such that
A39: c in dom f and
A40: b = f.c by A38,FUNCT_1:def 3;
reconsider c as set by TARSKI:1;
A41: F[c,f.c] by A14,A15,A39;
for B be Subset of x st B in Union f holds A=B or A misses B
proof
let B be Subset of x;
assume B in Union f;
then consider b2 be set such that
A42: B in b2 & b2 in rng f by TARSKI:def 4;
consider c2 be object such that
A43: c2 in dom f and
A44: b2 = f.c2 by A42,FUNCT_1:def 3;
per cases;
suppose c = c2;
hence thesis by A38,A40,A41,A42,A44,EQREL_1:def 4;
end;
suppose
A45: not c = c2;
consider p11,p21 be set such that
A46: p11 in P1 and
A47: p21 in P2 and
A48: c = p11/\p21 by A14,A39,SETFAM_1:def 5;
consider p12,p22 be set such that
A49: p12 in P1 and
A50: p22 in P2 and
A51: c2 = p12/\p22 by A14,A43,SETFAM_1:def 5;
A52: not p11/\p21 c= p12/\p22 implies A=B or A misses B
proof
assume not p11/\p21 c= p12/\p22;
then consider u be object such that
A53: u in p11/\p21 and
A54: not u in p12/\p22 by TARSKI:def 3;
A55: u in p11 & u in p21 & not u in p12 implies A=B or A misses B
proof
assume
A56: u in p11 & u in p21 & not u in p12;
F[c,f.c] & F[c2,f.c2] by A14,A15,A39,A43;
then union (f.c) = p11/\p21 &
union (f.c2) = p12/\p22 by A48,A51,EQREL_1:def 4; then
A57: union (f.c) c= p11 & union (f.c2) c= p12 &
p11 misses p12 by A46,A49,A56,EQREL_1:def 4,XBOOLE_1:17;
A c= union (f.c) &
B c= union (f.c2) by A38,A40,A42,A44,ZFMISC_1:74;
then A c= p11 & B c= p12 & p11 misses p12 by A57,XBOOLE_1:1;
hence thesis by XBOOLE_1:64;
end;
u in p11 & u in p21 & not u in p22 implies A=B or A misses B
proof
assume
A58: u in p11 & u in p21 & not u in p22;
F[c,f.c] & F[c2,f.c2] by A14,A15,A39,A43;
then union (f.c) = p11/\p21 &
union (f.c2) = p12/\p22 by A48,A51,EQREL_1:def 4; then
A59: union (f.c) c= p21 & union (f.c2) c= p22 &
p21 misses p22 by A47,A50,A58,EQREL_1:def 4,XBOOLE_1:17;
A c= union (f.c) &
B c= union (f.c2) by A38,A40,A42,A44,ZFMISC_1:74;
then A c= p21 & B c= p22 & p21 misses p22 by A59,XBOOLE_1:1;
hence thesis by XBOOLE_1:64;
end;
hence thesis by A53,A54,A55,XBOOLE_0:def 4;
end;
not p12/\p22 c= p11/\p21 implies A=B or A misses B
proof
assume not p12/\p22 c= p11/\p21;
then consider u be object such that
A60: u in p12/\p22 and
A61: not u in p11/\p21 by TARSKI:def 3;
A62: u in p12 & u in p22 & not u in p11 implies A=B or A misses B
proof
assume
A63: u in p12 & u in p22 & not u in p11;
F[c,f.c] & F[c2,f.c2] by A14,A15,A39,A43;
then union (f.c) = p11/\p21 &
union (f.c2) = p12/\p22 by A48,A51,EQREL_1:def 4; then
A64: union (f.c) c= p11 & union (f.c2) c= p12 &
p11 misses p12 by A46,A49,A63,EQREL_1:def 4,XBOOLE_1:17;
A c= union (f.c) &
B c= union (f.c2) by A38,A40,A42,A44,ZFMISC_1:74;
then A c= p11 & B c= p12 & p11 misses p12 by A64,XBOOLE_1:1;
hence thesis by XBOOLE_1:64;
end;
u in p12 & u in p22 & not u in p21 implies A=B or A misses B
proof
assume
A65: u in p12 & u in p22 & not u in p21;
F[c,f.c] & F[c2,f.c2] by A14,A15,A39,A43;
then union (f.c) = p11/\p21 &
union (f.c2) = p12/\p22 by A48,A51,EQREL_1:def 4;
then
A66: union (f.c) c= p21 & union (f.c2) c= p22 &
p21 misses p22 by A47,A50,A65,EQREL_1:def 4,XBOOLE_1:17;
A c= union (f.c) &
B c= union (f.c2) by A38,A40,A42,A44,ZFMISC_1:74;
then A c= p21 & B c= p22 & p21 misses p22 by A66,XBOOLE_1:1;
hence thesis by XBOOLE_1:64;
end;
hence thesis by A60,A61,A62,XBOOLE_0:def 4;
end;
hence thesis by A45,A48,A51,A52,XBOOLE_0:def 10;
end;
end;
hence thesis by A38,A40,A41;
end;
hence thesis by A23,A25,EQREL_1:def 4;
end;
Union f '<' P1 '/\' P2
proof
for a be set st a in Union f ex b be set st b in P1 '/\' P2 & a c= b
proof
let a be set;
assume a in Union f;
then consider b be set such that
A67: a in b and
A68: b in rng f by TARSKI:def 4;
consider c be object such that
A69: c in dom f and
A70: b = f.c by A68,FUNCT_1:def 3;
reconsider c as set by TARSKI:1;
F[c,f.c] by A14,A15,A69;
hence thesis by A67,A70;
end;
hence thesis by SETFAM_1:def 2;
end;
hence thesis by A16,A22;
end;
theorem V:
for S be cap-finite-partition-closed Subset-Family of X holds
for A,B be finite Subset of S st A is mutually-disjoint &
B is mutually-disjoint ex P be finite Subset of S st
P is a_partition of union A /\ union B
proof
let S be cap-finite-partition-closed Subset-Family of X;
let A,B be finite Subset of S;
assume that
A1: A is mutually-disjoint and
A2: B is mutually-disjoint;
per cases;
suppose
A3: [:A,B:]<>{};
defpred F[object,object] means
ex a,b be set st a in A & b in B & $1=[a,b] &
ex p be finite Subset of S st p is a_partition of a/\b &
$2=p;
set XIN = the set of all s where s is Element of [:A,B:];
set XOUT={s where s is finite Subset of S:ex a,b be set st
a in A & b in B & s is a_partition of a/\b};
A4: for x be object st x in XIN ex y be object st y in XOUT & F[x,y]
proof
let x be object;
assume x in XIN;
then consider s be Element of [:A,B:] such that
A5: x=s;
consider a0,b0 be object such that
A6: a0 in A & b0 in B and
A7: s=[a0,b0] by A3,ZFMISC_1:def 2;
reconsider a0,b0 as set by TARSKI:1;
per cases;
suppose a0/\b0 is non empty;
then consider P be finite Subset of S such that
A8: P is a_partition of a0/\b0 by A6,Defcap;
P in XOUT by A6,A8;
hence thesis by A5,A6,A7,A8;
end;
suppose a0/\b0 is empty;
then
A9: {} is finite Subset of S & {} is a_partition of a0/\b0
by SUBSET_1:1,EQREL_1:45;
then {} in XOUT by A6;
hence thesis by A5,A6,A7,A9;
end;
end;
consider f be Function such that
A10: dom f = XIN & rng f c= XOUT and
A11: for x be object st x in XIN holds F[x,f.x] from FUNCT_1:sch 6(A4);
A12: Union f is finite
proof
A13: [:A,B:]=XIN
proof
A14: [:A,B:] c= XIN
proof
let x be object;
assume x in [:A,B:];
hence thesis;
end;
XIN c= [:A,B:]
proof
let x be object;
assume x in XIN;
then consider s be Element of [:A,B:] such that
A15: s=x;
thus thesis by A3,A15;
end;
hence thesis by A14;
end;
for z be set st z in rng f holds z is finite
proof
let z be set;
assume z in rng f;
then z in XOUT by A10;
then consider s0 be finite Subset of S such that
A16: s0=z and
ex a,b be set st a in A & b in B & s0 is a_partition of a/\b;
thus thesis by A16;
end;
hence thesis by A13,A10,FINSET_1:8,FINSET_1:7;
end;
A17: Union f c= S
proof
let x be object;
assume x in Union f;
then consider y be set such that
A18: x in y & y in rng f by TARSKI:def 4;
y in XOUT by A18,A10;
then consider s0 be finite Subset of S such that
A19: y=s0 and
ex a,b be set st a in A & b in B & s0 is a_partition of a/\b;
thus thesis by A18,A19;
end;
A20: Union f c= bool (union A /\ union B)
proof
let x be object;
assume x in Union f;
then consider y be set such that
A21: x in y and
A22: y in rng f by TARSKI:def 4;
y in XOUT by A22,A10;
then consider s0 be finite Subset of S such that
A23: y=s0 and
A24: ex a,b be set st a in A & b in B & s0 is a_partition of a/\b;
reconsider x as set by TARSKI:1;
consider a0, b0 be set such that
A25: a0 in A & b0 in B and
A26: s0 is a_partition of a0/\b0 by A24;
a0 c= union A & b0 c= union B by A25,ZFMISC_1:74;
then a0/\b0 c= union A /\ union B by XBOOLE_1:27;
then x c= union A /\ union B by XBOOLE_1:1,A21,A23,A26;
hence thesis;
end;
A27: union Union f = union A /\ union B
proof
A28: union Union f c= union A /\ union B
proof
union Union f c= union bool (union A /\ union B) by A20,ZFMISC_1:77;
hence thesis by ZFMISC_1:81;
end;
union A/\union B c= union Union f
proof
let x be object;
assume x in union A/\union B; then
A29: x in union A & x in union B by XBOOLE_0:def 4;
then consider a be set such that
A30: x in a & a in A by TARSKI:def 4;
consider b be set such that
A31: x in b & b in B by A29,TARSKI:def 4;
[a,b] in [:A,B:] by A30,A31,ZFMISC_1:def 2;
then
A32: [a,b] in XIN;
then F[[a,b],f.([a,b])] by A11;
then consider a0,b0 be set such that
a0 in A & b0 in B and
A33: [a,b]=[a0,b0] and
A34: ex p be finite Subset of S st p is a_partition of a0/\b0 &
f.([a0,b0])=p;
consider p be finite Subset of S such that
A35: p is a_partition of a0/\b0 and
A36: f.([a0,b0])=p by A34;
A37: a0=a & b0=b by A33,XTUPLE_0:1;
f.([a,b]) in rng f by A32,A10,FUNCT_1:def 3;
then
A38: union (f.([a,b])) c= union union rng f by ZFMISC_1:77,ZFMISC_1:74;
x in a/\b by A30,A31,XBOOLE_0:def 4;
then x in union (f.([a,b])) by A35,A36,A37,EQREL_1:def 4;
hence thesis by A38;
end;
hence thesis by A28;
end;
for u be Subset of union A /\ union B st u in Union f holds
u<>{} &
for v be Subset of union A /\ union B st v in Union f holds u=v or
u misses v
proof
let u be Subset of union A /\ union B;
assume u in Union f;
then consider v be set such that
A39: u in v and
A40: v in rng f by TARSKI:def 4;
consider w be object such that
A41: w in dom f and
A42: v=f.w by A40,FUNCT_1:def 3;
consider x be Element of [:A,B:] such that
A43: w=x by A41,A10;
reconsider w as Element of [:A,B:] by A43;
consider wa,wb be object such that
wa in A & wb in B and
A44: w=[wa,wb] by A3,ZFMISC_1:def 2;
consider a,b be set such that
A45: a in A & b in B and
A46: [wa,wb]=[a,b] and
A47: ex p be finite Subset of S st p is a_partition of a/\b &
f.w=p by A41,A10,A11,A44;
consider p be finite Subset of S such that
A48: p is a_partition of a/\b and
A49: f.w=p by A47;
v in XOUT by A40,A10;
then consider s0 be finite Subset of S such that
A50: v=s0 and
A51: ex a,b be set st a in A & b in B & s0 is a_partition of a/\b;
consider a0,b0 be set such that
a0 in A & b0 in B and
A52: s0 is a_partition of a0/\b0 by A51;
thus u<>{} by A39,A50,A52;
thus for v be Subset of union A /\ union B st v in Union f holds
u=v or u misses v
proof
let jw be Subset of union A /\ union B;
assume jw in Union f;
then consider lw0 be set such that
A53: jw in lw0 and
A54: lw0 in rng f by TARSKI:def 4;
consider lw be object such that
A55: lw in dom f and
A56: lw0=f.lw by A54,FUNCT_1:def 3;
consider lx be Element of [:A,B:] such that
A57: lw=lx by A55,A10;
reconsider lw as Element of [:A,B:] by A57;
consider lwa,lwb be object such that
lwa in A & lwb in B and
A58: lw=[lwa,lwb] by A3,ZFMISC_1:def 2;
consider la,lb be set such that
A59: la in A & lb in B and
A60: [lwa,lwb]=[la,lb] and
A61: ex p be finite Subset of S st p is a_partition of la/\lb &
f.lw=p by A55,A10,A11,A58;
consider lp be finite Subset of S such that
A62: lp is a_partition of la/\lb and
A63: f.lw=lp by A61;
per cases;
suppose a=la & b=lb;
hence thesis
by A39,A42,A44,A46,A56,A58,A60,A63,A62,A53,EQREL_1:def 4;
end;
suppose
A64: a<>la or b<>lb;
a/\b c= b & la/\lb c= lb & a/\b c= a & la/\lb c= la by XBOOLE_1:17;
then
a/\b misses la/\lb by A64,A45,A59,A1,A2,TAXONOM2:def 5,XBOOLE_1:64;
hence thesis by A39,A49,A48,A42,A56,A63,A62,A53,XBOOLE_1:64;
end;
end;
end;
then Union f is a_partition of union A /\ union B
by A20,A27,EQREL_1:def 4;
hence thesis by A12,A17;
end;
suppose [:A,B:]={};
then A={} or B={};
hence thesis by ZFMISC_1:2,EQREL_1:45;
end;
end;
Lem8:
for S be cap-finite-partition-closed Subset-Family of X holds
for SM be FinSequence of S
ex P be finite Subset of S st P is a_partition of meet rng SM
proof
let S be cap-finite-partition-closed Subset-Family of X;
let SM be FinSequence of S;
per cases;
suppose
A1: S is empty;
then meet rng SM={} by SETFAM_1:1;
hence thesis by A1,EQREL_1:45;
end;
suppose
A3: S is non empty;
defpred P[FinSequence] means
ex p be finite Subset of S st p is a_partition of meet rng $1;
A4: for p be FinSequence of S,x be Element of S st P[p] holds P[p^<*x*>]
proof
let p be FinSequence of S;
let x be Element of S;
assume
A5: P[p];
per cases;
suppose
A6: rng p ={};
rng (p^<*x*>)=(rng p) \/ rng(<*x*>) by FINSEQ_1:31;
then
A7: rng (p^<*x*>)={x} by A6,FINSEQ_1:38;
then
A8: meet rng (p^<*x*>)=x by SETFAM_1:10;
per cases;
suppose x is non empty;
then {x} is finite Subset of S &
{x} is a_partition of x by A3,SUBSET_1:33,EQREL_1:39;
hence thesis by A8;
end;
suppose x is empty;
then
A9: meet rng (p^<*x*>) = {} by A7,SETFAM_1:10;
{} is finite Subset of S &
{} is a_partition of {} by SUBSET_1:1,EQREL_1:45;
hence thesis by A9;
end;
end;
suppose
A10: rng p <>{};
consider pp be finite Subset of S such that
A11: pp is a_partition of meet rng p by A5;
defpred F[object,object] means
ex A1 being set st A1 = $1 & $1 is Element of S &
$2 is finite Subset of S & $2 is a_partition of A1/\x;
set XIN={s where s is Element of S:s in pp};
A15: XIN c= pp
proof
let a be object;
assume a in XIN;
then ex a0 be Element of S st a=a0 & a0 in pp;
hence thesis;
end;
set XOUT={s where s is finite Subset of S:
ex y be set st y in pp & s is a_partition of y/\x};
A17: for a being object st a in XIN
ex b be object st b in XOUT & F[a,b]
proof
let a be object;
assume a in XIN;
then consider s0 be Element of S such that
A18: a=s0 and
A19: s0 in pp;
per cases;
suppose s0/\x <>{};
then consider ps be finite Subset of S such that
A20: ps is a_partition of s0/\x by Defcap;
ps in XOUT & F[a,ps] by A18,A19,A20;
hence thesis;
end;
suppose
A21: s0/\x={};
{} is finite Subset of S & {} is a_partition of {}
by SUBSET_1:1,EQREL_1:45;
then {} in XOUT & F[a,{}] by A18,A19,A21;
hence thesis;
end;
end;
consider f be Function such that
A22: dom f =XIN & rng f c= XOUT and
A23: for x being object st x in XIN holds F[x,f.x]
from FUNCT_1:sch 6(A17);
Union f is finite Subset of S &
Union f is a_partition of meet(rng(p^<*x*>))
proof
A24: Union f is finite
proof
for z be set st z in rng f holds z is finite
proof
let z be set;
assume z in rng f;
then consider z0 be object such that
A25: z0 in XIN & z=f.z0 by A22,FUNCT_1:def 3;
F[z0,f.z0] by A23,A25;
hence thesis by A25;
end;
hence thesis by A22,A15,FINSET_1:7,FINSET_1:8;
end;
A26: Union f c= S
proof
let a be object;
assume a in Union f;
then consider b be set such that
A27: a in b and
A28: b in rng f by TARSKI:def 4;
consider c be object such that
A29: c in XIN & b=f.c by A22,A28,FUNCT_1:def 3;
F[c,f.c] by A23,A29;
hence thesis by A27,A29;
end;
A30: Union f c= bool meet(rng(p^<*x*>))
proof
let a be object;
assume a in Union f;
then consider b be set such that
A31: a in b and
A32: b in rng f by TARSKI:def 4;
reconsider a as set by TARSKI:1;
b in XOUT by A22,A32;
then consider b0 be finite Subset of S such that
A33: b=b0 and
A34: ex y be set st y in pp & b0 is a_partition of y/\x;
consider y0 be set such that
A35: y0 in pp and
A36: b0 is a_partition of y0/\x by A34;
y0/\x c= meet rng p /\ x by A35,A11,XBOOLE_1:26;
then
A37: y0/\x c= meet rng p /\ meet({x}) by SETFAM_1:10;
A38: a c= meet rng p /\ meet({x}) by A31,A33,A36,A37,XBOOLE_1:1;
a c= meet(rng p \/ {x}) by A10,A38,SETFAM_1:9;
then a c= meet(rng p \/ rng <*x*>) by FINSEQ_1:38;
then a c= meet(rng(p^<*x*>)) by FINSEQ_1:31;
hence thesis;
end;
A39: union Union f = meet(rng(p^<*x*>))
proof
A40: union Union f c= meet rng (p^<*x*>)
proof
union Union f c= union bool meet rng (p^<*x*>)
by A30,ZFMISC_1:77;
hence thesis by ZFMISC_1:81;
end;
meet rng (p^<*x*>) c= union Union f
proof
let a be object;
assume
A41: a in meet rng (p^<*x*>);
rng (p^<*x*>)=rng p \/ rng (<*x*>) by FINSEQ_1:31;
then
A42: meet rng (p^<*x*>)=meet (rng p \/ {x}) by FINSEQ_1:38;
meet rng (p^<*x*>)=meet (rng p) /\ meet {x}
by A10,A42,SETFAM_1:9;
then meet rng (p^<*x*>)=meet (rng p) /\ x by SETFAM_1:10;
then a in union pp /\x by A11,EQREL_1:def 4,A41;
then
A43: a in union pp & a in x by XBOOLE_0:def 4;
then consider a0 be set such that
A44: a in a0 & a0 in pp by TARSKI:def 4;
A45: a0 in XIN by A44;
then F[a0,f.a0] by A23;
then
A46: union (f.a0)=a0/\x by EQREL_1:def 4;
a in a0/\x by A44,A43,XBOOLE_0:def 4;
then consider c0 be set such that
A47: a in c0 and
A48: c0 in f.a0 by A46,TARSKI:def 4;
A49: a in union (f.a0) by A47,A48,TARSKI:def 4;
f.a0 c= Union f
proof
let b be object;
assume b in f.a0;
then b in f.a0 & f.a0 in rng f by A22,A45,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
then union (f.a0) c= union Union f by ZFMISC_1:77;
hence thesis by A49;
end;
hence thesis by A40;
end;
for A be Subset of meet(rng(p^<*x*>)) st A in Union f holds
A<>{} &
for B be Subset of meet(rng(p^<*x*>)) st B in Union f holds
A=B or A misses B
proof
let A be Subset of meet(rng(p^<*x*>));
assume
A51: A in Union f;
consider a0 be set such that
A52: A in a0 & a0 in rng f by A51,TARSKI:def 4;
consider b0 be object such that
A53: b0 in XIN and
A54: a0=f.b0 by A52,A22,FUNCT_1:def 3;
reconsider b0 as set by TARSKI:1;
A55: F[b0,f.b0] by A23,A53;
hence A<>{} by A52,A54;
thus for B be Subset of meet(rng(p^<*x*>)) st B in Union f
holds A=B or A misses B
proof
let B be Subset of meet(rng(p^<*x*>));
assume B in Union f;
then consider d0 be set such that
A56: B in d0 & d0 in rng f by TARSKI:def 4;
consider e0 be object such that
A57: e0 in XIN and
A58: d0=f.e0 by A56,A22,FUNCT_1:def 3;
reconsider e0 as set by TARSKI:1;
B02: F[e0,f.e0] by A23,A57;
consider b00 be Element of S such that
A59: b0=b00 and
A60: b00 in pp by A53;
consider e00 be Element of S such that
A61: e0=e00 and
A62: e00 in pp by A57;
per cases;
suppose e00=b00;
hence thesis by A52,A54,A56,A58,A59,A61,A55,
EQREL_1:def 4;
end;
suppose
A63: not e00=b00;
union (f.b0) = b0/\x & union (f.e0) = e0/\x
by EQREL_1:def 4,A55,B02;
then union (f.b0) c= b0 & union (f.e0) c= e0
by XBOOLE_1:17;
then
A64: union (f.b0) misses union (f.e0)
by A63,A59,A61,A60,A62,A11,EQREL_1:def 4,XBOOLE_1:64;
A /\ B c= {}
proof
let t be object;
assume t in A/\B;
then t in A & t in B by XBOOLE_0:def 4;
then t in union (f.b0) & t in union (f.e0)
by A52,A54,A56,A58,TARSKI:def 4;
hence thesis by A64,XBOOLE_0:def 4;
end;
hence thesis;
end;
end;
end;
hence thesis by A24,A26,A30,A39,EQREL_1:def 4;
end;
hence thesis;
end;
end;
A65: P[<*>S]
proof
{} is Subset of S & {} is a_partition of {} by SUBSET_1:1,EQREL_1:45;
hence thesis by SETFAM_1:1;
end;
for p be FinSequence of S holds P[p]
from FINSEQ_2:sch 2(A65,A4);
then consider P be finite Subset of S such that
A66: P is a_partition of meet rng SM;
thus thesis by A66;
end;
end;
theorem
for S be cap-finite-partition-closed Subset-Family of X holds
for SM be finite Subset of S ex P be finite Subset of S st
P is a_partition of meet SM
proof
let S be cap-finite-partition-closed Subset-Family of X;
let SM be finite Subset of S;
consider SF be FinSequence such that
A1: rng SF = SM by FINSEQ_1:52;
SF is FinSequence of S by A1,FINSEQ_1:def 4;
hence thesis by A1,Lem8;
end;
theorem Thm86:
for S be cap-finite-partition-closed Subset-Family of X
holds
{union x where x is finite Subset of S:x is mutually-disjoint}
is cap-closed
proof
let S be cap-finite-partition-closed Subset-Family of X;
set Y={union x where x is finite Subset of S:x is mutually-disjoint};
let a,b be set such that
H3: a in Y and
H4: b in Y;
a /\ b in Y
proof
consider xa be finite Subset of S such that
V1: a=union xa and
V2: xa is mutually-disjoint by H3;
consider xb be finite Subset of S such that
V3: b=union xb and
V4: xb is mutually-disjoint by H4;
consider p be finite Subset of S such that
K2: p is a_partition of union xa /\ union xb by V2,V4,V;
K3: union p = a /\ b by V1,V3,K2,EQREL_1:def 4;
for x,y be set st x in p & y in p & x<>y holds x misses y
by K2,EQREL_1:def 4;
then p is mutually-disjoint by TAXONOM2:def 5;
hence thesis by K3;
end;
hence thesis;
end;
definition
let X be set;
let S be Subset-Family of X;
attr S is diff-finite-partition-closed means
:Defdiff:
for S1,S2 be Element of S st S1\S2 is non empty
ex x be finite Subset of S st x is a_partition of S1\S2;
end;
registration
let X be set;
cluster cobool X -> diff-finite-partition-closed;
coherence by Lem4;
end;
registration
let X be set;
cluster diff-finite-partition-closed for Subset-Family of X;
existence
proof
take cobool X;
thus thesis;
end;
end;
registration
let X be set;
cluster diff-closed -> diff-finite-partition-closed for Subset-Family of X;
coherence
proof
let S be Subset-Family of X;
assume
A1: S is diff-closed;
for S1,S2 be Element of S st S1\S2 is non empty
ex y be finite Subset of S st
y is a_partition of S1\S2
proof
let S1,S2 be Element of S;
per cases;
suppose
A2: S is non empty;
assume
A3: S1\S2 is non empty;
take {S1\S2};
{S1\S2} c= S
proof
let x be object;
S1\S2 in S by A1,A2;
hence thesis by TARSKI:def 1;
end;
hence thesis by A3,EQREL_1:39;
end;
suppose S is empty;
hence thesis by SUBSET_1:def 1;
end;
end;
hence thesis;
end;
end;
theorem Thm1:
for S be diff-finite-partition-closed Subset-Family of X,
S1 be Element of S, T be finite Subset of S holds
ex P be finite Subset of S st P is a_partition of S1 \ union T
proof
let S be diff-finite-partition-closed Subset-Family of X;
let S1 be Element of S;
let TT be finite Subset of S;
consider T be FinSequence such that
A0: TT=rng T by FINSEQ_1:52;
reconsider T as FinSequence of S by A0,FINSEQ_1:def 4;
defpred P[FinSequence] means
ex pa be finite Subset of S st pa is a_partition of S1\union(rng $1);
A1: for p be FinSequence of S,x be Element of S st P[p] holds P[p^<*x*>]
proof
let p be FinSequence of S;
let x be Element of S;
assume P[p];
then consider pa be finite Subset of S such that
A2: pa is a_partition of S1\union(rng p);
A3: S1\union(rng (p^<*x*>))=S1\union(rng p \/ rng <*x*>) by FINSEQ_1:31
.=S1\(union (rng p) \/ union(rng <*x*>)) by ZFMISC_1:78
.=(S1\(union(rng p)))\(Union <*x*>) by XBOOLE_1:41
.=(S1\(union(rng p)))\(union {x}) by FINSEQ_1:38
.=(S1\(union(rng p)))\x;
ex pb be finite Subset of S st
pb is a_partition of S1\union(rng(p^<*x*>))
proof
defpred PP1[set] means
$1 is Element of S & $1\x is non empty & $1 in pa;
defpred G[object,object] means
ex A1 being set st A1 = $1 & $1 is Element of S &
$2 is finite Subset of S & A1\x is non empty &
$1 in pa & $2 is a_partition of A1\x;
set XX1={s where s is Element of S:PP1[s]};
set YY1={s where s is finite Subset of S:
ex y be Element of S st PP1[y] & s is a_partition of y\x};
A4: for a being object st a in XX1
ex y be object st y in YY1 & G[a,y]
proof
let a be object;
assume a in XX1;
then consider s be Element of S such that
A5: a=s & PP1[s];
reconsider a as set by TARSKI:1;
consider aa be finite Subset of S such that
A6: aa is a_partition of a\x by A5,Defdiff;
aa in YY1 & G[a,aa] by A5,A6;
hence thesis;
end;
consider gg be Function such that
A7: dom gg=XX1 & rng gg c=YY1 and
A8: for x being object st x in XX1 holds
G[x,gg.x] from FUNCT_1:sch 6(A4);
A9: XX1 is finite
proof
XX1 c= pa
proof
let u be object;
assume u in XX1;
then consider s be Element of S such that
A10: u=s & PP1[s];
thus thesis by A10;
end;
hence thesis;
end;
Union gg is finite Subset of S &
Union gg is a_partition of (S1\union(rng(p)))\x
proof
A11: Union gg is finite
proof
Union gg is finite
proof
for zz be set st zz in rng gg holds zz is finite
proof
let zz be set;
assume zz in rng gg;
then consider z0 be object such that
A12: z0 in XX1 & zz=gg.z0 by A7,FUNCT_1:def 3;
ex A1 being set st A1 = z0 & z0 is Element of S &
gg.z0 is finite Subset of S & A1\x is non empty &
z0 in pa & gg.z0 is a_partition of A1\x by A8,A12;
hence thesis by A12;
end;
hence thesis by A7,A9,FINSET_1:8,FINSET_1:7;
end;
hence thesis;
end;
A13: Union gg c= S
proof
let x be object;
assume x in Union gg;
then consider u be set such that
A14: x in u and
A15: u in rng gg by TARSKI:def 4;
consider u0 be object such that
A16: u0 in XX1 & u=gg.u0 by A7,A15,FUNCT_1:def 3;
G[u0,gg.u0] by A8,A16;
hence thesis by A14,A16;
end;
Union gg is a_partition of (S1\union(rng(p)))\x
proof
A17: Union gg c= bool ((S1\union(rng(p)))\x)
proof
let u be object;
assume
A18: u in Union gg;
reconsider u as set by TARSKI:1;
consider v be set such that
A19: u in v & v in rng gg by A18,TARSKI:def 4;
consider w be object such that
A20: w in dom gg and
A21: gg.w=v by A19,FUNCT_1:def 3;
reconsider w as set by TARSKI:1;
A22: G[w,gg.w] by A7,A8,A20;
then
w\x c= (S1\union(rng(p)))\x by A2,XBOOLE_1:33;
then u c= ((S1\union(rng(p)))\x) by A19,A21,A22,XBOOLE_1:1;
hence thesis;
end;
A23: union Union gg = ((S1\union(rng(p)))\x)
proof
A24: union Union gg c= union bool ((S1\union(rng(p)))\x)
by A17,ZFMISC_1:77;
(S1\Union p)\x c= union Union gg
proof
let a be object;
assume
A25: a in (S1\Union p)\x;
A26: a in (union pa)\x by A2,A25,EQREL_1:def 4;
then
A27: a in union pa & not a in x by XBOOLE_0:def 5;
consider p11 be set such that
A28: a in p11 & p11 in pa by A26,TARSKI:def 4;
p11\x is non empty & p11 is Element of S &
x is Element of S by A27,A28,XBOOLE_0:def 5;
then
A29: p11 in XX1 by A28;
then G[p11,gg.p11] by A8;
then union (gg.p11) = p11\x by EQREL_1:def 4;
then a in union (gg.p11) by A27,A28,XBOOLE_0:def 5;
then consider d be set such that
A30: a in d & d in gg.p11 by TARSKI:def 4;
a in d & d in gg.p11 &
gg.p11 in rng gg
by A7,A29,A30,FUNCT_1:3;
then a in d & d in union(rng gg) by TARSKI:def 4;
hence thesis by TARSKI:def 4;
end;
hence thesis by A24,ZFMISC_1:81;
end;
for A be Subset of (S1\union(rng(p)))\x st
A in Union gg holds A<>{} &
for B be Subset of (S1\union(rng(p)))\x st
B in Union gg holds A=B or (A misses B)
proof
let A be Subset of (S1\union(rng(p)))\x;
assume
A31: A in Union gg;
consider a0 be set such that
A32: A in a0 & a0 in rng gg by A31,TARSKI:def 4;
consider a1 be object such that
A33: a1 in XX1 & a0=gg.a1 by A7,A32,FUNCT_1:def 3;
reconsider a1 as set by TARSKI:1;
A<>{} & for B be Subset of (S1\union(rng(p)))\x st
B in Union gg holds A=B or (A misses B)
proof
thus A<>{}
proof
assume
A34: A={};
G[a1,gg.a1] by A8,A33;
hence thesis by A32,A33,A34;
end;
thus for B be Subset of (S1\union(rng p))\x st
B in Union gg holds A=B or (A misses B)
proof
let B be Subset of (S1\union(rng p))\x;
assume B in Union gg;
then consider x0 be set such that
A35: B in x0 & x0 in rng gg by TARSKI:def 4;
consider y0 be object such that
A36: y0 in XX1 & gg.y0=x0 by A7,A35,FUNCT_1:def 3;
reconsider y0 as set by TARSKI:1;
A=B or A misses B
proof
per cases;
suppose
A37: a1=y0;
then G[a1,gg.a1] by A8,A36;
hence thesis by A32,A33,A35,A36,A37,EQREL_1:def 4;
end;
suppose
A38: not a1=y0;
consider sx be Element of S such that
A39: a1=sx & PP1[sx] by A33;
consider sd be Element of S such that
A40: y0=sd & PP1[sd] by A36;
A41: a1\x misses y0\x
by A2,A38,A39,A40,EQREL_1:def 4,XBOOLE_1:64;
A42: G[y0,gg.y0] by A8,A36;
G[a1,gg.a1] by A8,A33;
hence thesis by A32,A33,A35,A36,A41,A42,XBOOLE_1:64;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by A17,A23,EQREL_1:def 4;
end;
hence thesis by A11,A13;
end;
hence thesis by A3;
end;
hence thesis;
end;
A44: P[<*>S]
proof
A45: S1={} implies ex pa be finite Subset of S st
pa is a_partition of S1\union (rng {})
proof
{} is Subset of S by SUBSET_1:1;
hence thesis by EQREL_1:45;
end;
S1<>{} implies ex pa be finite Subset of S st
pa is a_partition of S1\union(rng{})
proof
assume
A47: S1<>{};
per cases;
suppose S is non empty;
then
A48: {S1} is Subset of S by SUBSET_1:41;
{S1} is a_partition of S1 by A47,EQREL_1:39;
hence thesis by A48,ZFMISC_1:2;
end;
suppose S is empty;
hence thesis by A47,SUBSET_1:def 1;
end;
end;
hence thesis by A45;
end;
for p be FinSequence of S holds P[p] from FINSEQ_2:sch 2(A44,A1);
then ex P be finite Subset of S st
P is a_partition of S1 \ Union T;
hence thesis by A0;
end;
begin :: Partitions in a Difference of Sets
definition
let X be set;
let S be Subset-Family of X;
attr S is diff-c=-finite-partition-closed means
:Defdiff2:
for S1,S2 be Element of S st S2 c= S1 holds
ex x be finite Subset of S st x is a_partition of S1\S2;
end;
theorem Thm2:
for S be Subset-Family of X st
S is diff-finite-partition-closed holds
S is diff-c=-finite-partition-closed
proof
let S be Subset-Family of X;
assume
A1: S is diff-finite-partition-closed;
let S1,S2 be Element of S;
assume S2 c= S1;
per cases;
suppose
A2: S1\S2 is empty;
{} is finite Subset of S & {} is a_partition of {}
by SUBSET_1:1,EQREL_1:45;
hence thesis by A2;
end;
suppose S1\S2 is non empty;
then consider x be finite Subset of S such that
A3: x is a_partition of S1\S2 by A1;
thus thesis by A3;
end;
end;
registration
let X;
cluster diff-finite-partition-closed -> diff-c=-finite-partition-closed for
Subset-Family of X;
coherence by Thm2;
end;
registration
let X;
cluster cobool X -> diff-c=-finite-partition-closed;
coherence;
end;
registration
let X;
cluster diff-c=-finite-partition-closed diff-finite-partition-closed
cap-finite-partition-closed with_empty_element for Subset-Family of X;
existence
proof
take cobool X;
thus thesis;
end;
end;
theorem
for S be diff-finite-partition-closed Subset-Family of X holds
{union x where x is finite Subset of S:x is mutually-disjoint} is
diff-closed
proof
let S be diff-finite-partition-closed Subset-Family of X;
set Y={union x where x is finite Subset of S:x is mutually-disjoint};
for A,B be set st A in Y & B in Y holds A\B in Y
proof
let A,B be set;
assume that
A1: A in Y and
A2: B in Y;
consider a be finite Subset of S such that
A3: A=union a and
A4: a is mutually-disjoint by A1;
consider b be finite Subset of S such that
A5: B=union b and
b is mutually-disjoint by A2;
consider SFA be FinSequence such that
A7: a=rng SFA by FINSEQ_1:52;
consider SFB be FinSequence such that
A8: b=rng SFB by FINSEQ_1:52;
defpred F[object,object] means
ex A be set st A = $1 &
$1 in a & $2 is a_partition of A\Union SFB;
set XOUT= the set of all s where s is finite Subset of S;
A12: for x be object st x in a ex y be object st y in XOUT & F[x,y]
proof
let x be object;
assume
A: x in a;
reconsider x as set by TARSKI:1;
consider P be finite Subset of S such that
B: P is a_partition of x\Union SFB by A,A8,Thm1;
P in XOUT & F[x,P] by A,B;
hence thesis;
end;
consider f be Function such that
F1: dom f = a & rng f c= XOUT and
F2: for x be object st x in a holds F[x,f.x] from FUNCT_1:sch 6(A12);
V1: Union f is finite Subset of S
proof
W1: Union f is finite
proof
for x be set st x in rng f holds x is finite
proof
let x be set;
assume x in rng f;
then x in XOUT by F1;
then consider s be finite Subset of S such that
V: x=s;
thus thesis by V;
end;
hence thesis by F1,FINSET_1:8,FINSET_1:7;
end;
Union f c= S
proof
let x be object;
assume x in Union f;
then consider y be set such that
H: x in y & y in rng f by TARSKI:def 4;
y in XOUT by H,F1;
then consider s be finite Subset of S such that
I: y=s;
thus thesis by H,I;
end;
hence thesis by W1;
end;
V1a: Union f is a_partition of Union SFA \ Union SFB
proof
Z1: Union f c= bool (Union SFA \ Union SFB)
proof
let x be object;
assume x in Union f;
then consider y be set such that
R1: x in y and
R2: y in rng f by TARSKI:def 4;
consider x0 be object such that
R3: x0 in dom f and
R4: y=f.x0 by R2,FUNCT_1:def 3;
reconsider x0 as set by TARSKI:1;
R5: F[x0,f.x0] by R3,F1,F2;
x0\Union SFB c= Union SFA \ Union SFB
by A7,R3,F1,ZFMISC_1:74,XBOOLE_1:33;
then bool(x0\Union SFB) c= bool (Union SFA\Union SFB)
by ZFMISC_1:67;
then f.x0 c= bool (Union SFA\Union SFB) by R5,XBOOLE_1:1;
hence thesis by R1,R4;
end;
Z2: union Union f = Union SFA \ Union SFB
proof
ZE: union Union f c= Union SFA \ Union SFB
proof
let x be object;
assume
A: x in union Union f;
union Union f c= union bool (Union SFA\Union SFB)
by Z1,ZFMISC_1:77;
then x in union bool (Union SFA \ Union SFB) by A;
hence thesis by ZFMISC_1:81;
end;
Union SFA \ Union SFB c= union Union f
proof
let x be object;
assume
U1: x in Union SFA \ Union SFB;
consider y be set such that
U2: x in y and
U3: y in rng SFA by U1,TARSKI:def 4;
U4a: x in y & not x in Union SFB by U2,U1,XBOOLE_0:def 5;
F[y,f.y] by F2,U3,A7;
then union (f.y) = y\Union SFB by EQREL_1:def 4;
then
U6: x in union (f.y) by U4a,XBOOLE_0:def 5;
f.y in rng f by F1,U3,A7,FUNCT_1:def 3;
then union (f.y) c= union Union f by ZFMISC_1:74,ZFMISC_1:77;
hence thesis by U6;
end;
hence thesis by ZE;
end;
for m be Subset of Union SFA \ Union SFB st m in Union f holds m<>{} &
for n be Subset of Union SFA \ Union SFB st n in Union f holds
n=m or n misses m
proof
let m be Subset of Union SFA \ Union SFB;
assume
L0: m in Union f;
consider m0 be set such that
L2: m in m0 and
L3: m0 in rng f by L0,TARSKI:def 4;
consider m1 be object such that
L4: m1 in a and
L5: m0=f.m1 by L3,F1,FUNCT_1:def 3;
reconsider m1 as set by TARSKI:1;
L6: F[m1,f.m1] by F2,L4;
for n be Subset of Union SFA \ Union SFB st n in Union f holds
n=m or n misses m
proof
let n be Subset of Union SFA \ Union SFB;
assume
CL0: n in Union f;
n=m or n misses m
proof
consider n0 be set such that
CL2: n in n0 and
CL3: n0 in rng f by CL0,TARSKI:def 4;
consider n1 be object such that
CL4: n1 in a and
CL5: n0=f.n1 by CL3,F1,FUNCT_1:def 3;
reconsider n1 as set by TARSKI:1;
CL6: F[n1,f.n1] by F2,CL4;
per cases;
suppose m1=n1;
hence thesis by L2,L5,CL2,CL5,CL6,EQREL_1:def 4;
end;
suppose
KKA: not m1=n1;
m1\Union SFB misses n1\Union SFB
by KKA,A4,L4,CL4,TAXONOM2:def 5,XBOOLE_1:64;
hence thesis by L6,CL6,L2,L5,CL2,CL5,XBOOLE_1:64;
end;
end;
hence thesis;
end;
hence thesis by L2,L5,L6;
end;
hence thesis by Z1,Z2,EQREL_1:def 4;
end;
V2: Union f is mutually-disjoint
proof
for n,m be set st n in Union f & m in Union f & n<>m holds
n misses m by V1a,EQREL_1:def 4;
hence thesis by TAXONOM2:def 5;
end;
A\B = union Union f by V1a,A3,A5,A7,A8,EQREL_1:def 4;
hence thesis by V1,V2;
end;
hence thesis;
end;
theorem Thm5:
for S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X holds (for A be Element of S, Q be finite Subset of S st
union Q c= A & Q is a_partition of union Q ex R be finite
Subset of S st union R misses union Q & Q\/R is a_partition of A)
proof
let S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X;
A1: (for A,B be Element of S holds
ex P be finite Subset of S st P is a_partition of A/\B) by Lem7;
A2: (for C,D be Element of S st D c= C holds
ex P be finite Subset of S st P is a_partition of C\D) by Defdiff2;
let A be Element of S;
let Q be finite Subset of S;
assume that
A3: union Q c= A and
A4: Q is a_partition of union Q;
per cases;
suppose
A5: S is empty;
then
A6: A is empty by SUBSET_1:def 1;
A7: union Q misses union {} by ZFMISC_1:2;
A8: {} is finite Subset of {} &
{} is a_partition of {} by SUBSET_1:1,EQREL_1:45;
Q\/{} is a_partition of A by A5,A6,EQREL_1:45;
hence thesis by A5,A7,A8;
end;
suppose
A9: not S is empty;
per cases;
suppose
A10: A is empty;
A20: union Q misses union {} by ZFMISC_1:2;
A21: {} is finite Subset of S &
{} is a_partition of {} by XBOOLE_1:2,EQREL_1:45;
Q\/{} is a_partition of A by A4,A10,A3;
hence thesis by A21,A20;
end;
suppose not A is empty;
hence thesis by A1,A2,A3,A4,A9,Lem6;
end;
end;
end;
theorem Thm6:
for S be diff-c=-finite-partition-closed cap-finite-partition-closed
Subset-Family of X holds S is diff-finite-partition-closed
proof
let S be diff-c=-finite-partition-closed
cap-finite-partition-closed Subset-Family of X;
for S1,S2 be Element of S st S1\S2 is non empty holds
ex P0 be finite Subset of S st P0 is a_partition of S1\S2
proof
let S1,S2 be Element of S;
assume
S1\S2 is non empty;
consider P0 be finite Subset of S such that
A1: P0 is a_partition of S1/\S2 by Lem7;
A2: union P0 c= S1
proof
let x be object;
assume x in union P0;
then consider x0 be set such that
A3: x in x0 & x0 in P0 by TARSKI:def 4;
S1/\S2 c= S1 by XBOOLE_1:17;
then x0 c= S1 by A1,A3,XBOOLE_1:1;
hence thesis by A3;
end;
P0 is a_partition of union P0 by A1,EQREL_1:def 4;
then consider R be finite Subset of S such that
union R misses union P0 and
A4: P0\/R is a_partition of S1 by A2,Thm5;
A5: R/\bool(S1\S2) is finite Subset of S &
R/\bool(S1\S2) is a_partition of S1 \ S2
proof
A6: R/\bool(S1\S2) is Subset-Family of S1 \ S2 by XBOOLE_1:17;
A7: union (R/\bool(S1\S2)) = S1\S2
proof
A8: union (R/\bool(S1\S2)) c= S1\S2
proof
union (R/\bool(S1\S2)) c= union bool (S1\S2)
by XBOOLE_1:17,ZFMISC_1:77;
hence thesis by ZFMISC_1:81;
end;
S1\S2 c= union(R/\bool(S1\S2))
proof
let x be object;
assume
A9: x in S1\S2;
then
x in S1 & not x in S2 by XBOOLE_0:def 5;
then x in union (P0\/R) by A4,EQREL_1:def 4;
then consider X0 be set such that
A10: x in X0 and
A11: X0 in P0\/R by TARSKI:def 4;
A12: X0 in P0 implies X0 in bool S2
proof
assume
A13: X0 in P0;
S1/\S2 c= S2 by XBOOLE_1:17;
then X0 c= S2 by A13,A1,XBOOLE_1:1;
hence thesis;
end;
X0 in R/\bool(S1\S2)
proof
A14: X0 in R by A12,A9,XBOOLE_0:def 5,A10,A11,XBOOLE_0:def 3;
X0 c= S1\S2
proof
assume not X0 c= S1\S2;
then consider xx be object such that
A15: xx in X0 and
A16: not xx in S1\S2 by TARSKI:def 3;
xx in X0 & X0 in R
by A12,A9,XBOOLE_0:def 5,A10,A11,XBOOLE_0:def 3,A15;
then
A17: xx in union R by TARSKI:def 4;
union R c= union (P0\/R) by XBOOLE_1:7,ZFMISC_1:77;
then
A18: union R c= S1 by A4,EQREL_1:def 4;
A19: not xx in S1 or xx in S2 by A16,XBOOLE_0:def 5;
X0 in P0
proof
A20: xx in S1/\S2 by A18,A17,A19,XBOOLE_0:def 4;
union P0=S1/\S2 by A1,EQREL_1:def 4;
then consider PP be set such that
A21: xx in PP and
A22: PP in P0 by A20,TARSKI:def 4;
A23: xx in PP/\X0 by A21,A15,XBOOLE_0:def 4;
PP in P0\/R & X0 in P0\/R by A22,XBOOLE_0:def 3,A11;
hence thesis by A22,A4,A23,XBOOLE_0:def 7,EQREL_1:def 4;
end;
hence thesis by A10,A12,A9,XBOOLE_0:def 5;
end;
hence thesis by A14,XBOOLE_0:def 4;
end;
hence thesis by A10,TARSKI:def 4;
end;
hence thesis by A8;
end;
for A be Subset of S1\S2 st A in R/\bool(S1\S2) holds A<>{} &
for B be Subset of S1\S2 st B in R/\bool(S1\S2) holds A=B or A misses B
proof
let A be Subset of S1\S2 such that
A24: A in R/\bool(S1\S2);
A in R by A24,XBOOLE_0:def 4;
then
A25: A in P0\/R by XBOOLE_0:def 3;
now
let B be Subset of S1\S2 such that
A26: B in R/\bool(S1\S2);
B in R by A26,XBOOLE_0:def 4;
then B in P0\/R by XBOOLE_0:def 3;
hence A=B or A misses B by A25,A4,EQREL_1:def 4;
end;
hence thesis by A25,A4;
end;
hence thesis by A6,A7,EQREL_1:def 4;
end;
thus thesis by A5;
end;
hence thesis;
end;
registration
let X be set;
cluster diff-c=-finite-partition-closed -> diff-finite-partition-closed for
cap-finite-partition-closed Subset-Family of X;
coherence by Thm6;
end;
Lem9:
for S be cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of X, SM,T be FinSequence of S holds
ex P be finite Subset of S st P is a_partition of (meet rng SM) \ Union T
proof
let S be cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of X;
let SM be FinSequence of S;
let T be FinSequence of S;
defpred P[FinSequence] means
ex pa be finite Subset of S st
pa is a_partition of (meet (rng $1))\(union(rng T));
A1: for p be FinSequence of S,x be Element of S st P[p] holds P[p^<*x*>]
proof
let p be FinSequence of S;
let x be Element of S;
assume P[p];
then consider pa be finite Subset of S such that
A2: pa is a_partition of (meet (rng p))\union(rng T);
A3: (meet rng (p^<*x*>))\union(rng T)=
(meet (rng p \/ rng <*x*>))\union(rng T) by FINSEQ_1:31
.=(meet ((rng p) \/ {x}))\union(rng T) by FINSEQ_1:38;
A4: rng p<>{} implies (meet (rng p \/ {x}))\union(rng T)=
((meet (rng p))\union(rng T))/\x
proof
assume rng p<>{};
then (meet (rng p \/ {x}))\union(rng T)=
(meet (rng p) /\ meet {x})\union(rng T) by SETFAM_1:9
.=(meet (rng p) /\ x)\union(rng T) by SETFAM_1:10
.=((meet (rng p))\union(rng T))/\x by XBOOLE_1:49;
hence thesis;
end;
ex pb be finite Subset of S st
pb is a_partition of meet(rng (p^<*x*>))\union(rng(T))
proof
defpred PP1[set] means
$1 is Element of S & $1/\x is non empty & $1 in pa;
defpred G[object,object] means
ex A1 being set st A1 = $1 & $1 is Element of S &
$2 is finite Subset of S & A1/\x is non empty &
$1 in pa & $2 is a_partition of A1/\x;
set XX1={s where s is Element of S:PP1[s]};
set YY1={s where s is finite Subset of S:
ex y be Element of S st PP1[y] & s is a_partition of y/\x};
A5: for a being object st a in XX1 ex y be object st y in YY1 & G[a,y]
proof
let a be object;
assume a in XX1;
then consider s be Element of S such that
A6: a=s & PP1[s];
reconsider a as set by TARSKI:1;
consider aa be finite Subset of S such that
A7: aa is a_partition of a/\x by A6,Defcap;
aa in YY1 & G[a,aa] by A6,A7;
hence thesis;
end;
consider gg be Function such that
A8: dom gg=XX1 & rng gg c=YY1 and
A9: for x being object st x in XX1 holds
G[x,gg.x] from FUNCT_1:sch 6(A5);
A10: XX1 is finite
proof
XX1 c= pa
proof
let u be object;
assume u in XX1;
then consider s be Element of S such that
A11: u=s & PP1[s];
thus thesis by A11;
end;
hence thesis;
end;
A12: Union gg is finite Subset of S &
Union gg is a_partition of (meet(rng(p))\union(rng(T)))/\x
proof
A13: Union gg is finite
proof
Union gg is finite
proof
for zz be set st zz in rng gg holds zz is finite
proof
let zz be set;
assume zz in rng gg;
then consider z0 be object such that
A14: z0 in XX1 & zz=gg.z0 by FUNCT_1:def 3,A8;
G[z0,gg.z0] by A9,A14;
hence thesis by A14;
end;
hence thesis by A10,A8,FINSET_1:8,FINSET_1:7;
end;
hence thesis;
end;
A15: Union gg c= S
proof
let x be object;
assume x in Union gg;
then consider u be set such that
A16: x in u and
A17: u in rng gg by TARSKI:def 4;
consider u0 be object such that
A18: u0 in XX1 & u=gg.u0 by A8,A17,FUNCT_1:def 3;
G[u0,gg.u0] by A9,A18;
hence thesis by A16,A18;
end;
Union gg is a_partition of (meet(rng(p))\union(rng(T)))/\x
proof
A19: Union gg c= bool (((meet(rng(p)))\union(rng(T)))/\x)
proof
let u be object;
assume
A20: u in Union gg;
consider v be set such that
A21: u in v & v in rng gg by TARSKI:def 4,A20;
consider w be object such that
A22: w in dom gg and
A23: gg.w=v by FUNCT_1:def 3,A21;
reconsider u,w as set by TARSKI:1;
A24: G[w,gg.w] by A22,A8,A9;
then w/\x c= ((meet(rng(p)))\union(rng(T))) /\ x
by A2,XBOOLE_1:26;
then u c= ((meet(rng(p)))\union(rng(T)))/\x
by A23,A21,A24,XBOOLE_1:1;
hence thesis;
end;
A25: union Union gg = ((meet(rng(p))\union(rng(T)))/\x)
proof
A26: union Union gg c= union bool ((meet(rng(p))\union(rng(T)))/\x)
by A19,ZFMISC_1:77;
((meet(rng(p))\union(rng(T)))/\x) c= union Union gg
proof
let a be object;
assume a in ((meet(rng(p))\union(rng(T)))/\x);
then a in (union pa)/\x by A2,EQREL_1:def 4;
then
A28: a in union pa & a in x by XBOOLE_0:def 4;
then consider p11 be set such that
A29: a in p11 & p11 in pa by TARSKI:def 4;
A30: p11/\x is non empty & p11 is Element of S &
x is Element of S by A28,A29,XBOOLE_0:def 4;
A31: p11 in XX1 by A29,A30;
then G[p11,gg.p11] by A9;
then union (gg.p11) = p11/\x by EQREL_1:def 4;
then a in union (gg.p11) by A28,A29,XBOOLE_0:def 4;
then consider d be set such that
A32: a in d & d in gg.p11 by TARSKI:def 4;
a in d & d in gg.p11 &
gg.p11 in rng gg by A32,A8,A31,FUNCT_1:3;
then a in d & d in union(rng gg) by TARSKI:def 4;
hence thesis by TARSKI:def 4;
end;
hence thesis by A26,ZFMISC_1:81;
end;
for A be Subset of ((meet(rng(p))\union(rng(T)))/\x) st
A in Union gg holds A<>{} &
for B be Subset of ((meet(rng(p))\union(rng(T)))/\x) st
B in Union gg holds A=B or (A misses B)
proof
let A be Subset of ((meet(rng(p))\union(rng(T)))/\x);
assume A in Union gg;
then consider a0 be set such that
A33: A in a0 & a0 in rng gg by TARSKI:def 4;
consider a1 be object such that
A34: a1 in XX1 & a0=gg.a1 by A33,A8,FUNCT_1:def 3;
reconsider a1 as set by TARSKI:1;
A<>{} & for B be Subset of ((meet(rng(p))\union(rng(T)))/\x) st
B in Union gg holds A=B or (A misses B)
proof
thus A<>{}
proof
assume
A35: A={};
G[a1,gg.a1] by A9,A34;
hence thesis by A33,A34,A35;
end;
thus for B be Subset of ((meet(rng(p))\union(rng(T)))/\x) st
B in Union gg holds A=B or (A misses B)
proof
let B be Subset of ((meet(rng(p))\union(rng(T)))/\x);
assume B in Union gg;
then consider x0 be set such that
A36: B in x0 & x0 in rng gg by TARSKI:def 4;
consider y0 be object such that
A37: y0 in XX1 & gg.y0=x0 by A8,A36,FUNCT_1:def 3;
reconsider y0 as set by TARSKI:1;
A=B or A misses B
proof
per cases;
suppose
A38: a1=y0;
then G[a1,gg.a1] by A9,A37;
hence thesis by EQREL_1:def 4,A36,A37,A33,A34,A38;
end;
suppose
A39: not a1=y0;
consider sx be Element of S such that
A40: a1=sx & PP1[sx] by A34;
consider sd be Element of S such that
A41: y0=sd & PP1[sd] by A37;
a1 misses y0 &
a1/\x c= a1 & y0/\x c= y0
by A40,A41,XBOOLE_1:17,A39,A2,EQREL_1:def 4;
then
A42: a1/\x misses y0/\x by XBOOLE_1:64;
A43: G[y0,gg.y0] by A9,A37;
G[a1,gg.a1] by A9,A34;
hence thesis by A43,A36,A37,A33,A34,A42,XBOOLE_1:64;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by EQREL_1:def 4,A19,A25;
end;
hence thesis by A13,A15;
end;
rng p={} implies ex ZZ be finite Subset of S st
ZZ is a_partition of ((meet(rng(p^<*x*>))\union(rng(T))))
proof
assume rng p={};
then p={};
then p^<*x*>=<*x*> by FINSEQ_1:34;
then rng(p^<*x*>)={x} by FINSEQ_1:39;
then
A44: ((meet(rng(p^<*x*>))\union(rng(T))))=x\union(rng(T))
by SETFAM_1:10;
thus thesis by A44,Thm1;
end;
hence thesis by A4,A12,A3;
end;
hence thesis;
end;
A45: P[<*>S]
proof
{} is finite Subset of S & {} is a_partition of {}
by SUBSET_1:1,EQREL_1:45;
hence thesis by SETFAM_1:1;
end;
for p be FinSequence of S holds P[p] from FINSEQ_2:sch 2(A45,A1);
hence thesis;
end;
theorem Thm3:
for S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X, SM,T be finite Subset of S holds
ex P be finite Subset of S st P is a_partition of (meet SM) \ union T
proof
let S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X;
let SM,T be finite Subset of S;
consider RSM be FinSequence such that
A: SM=rng RSM by FINSEQ_1:52;
consider RT be FinSequence such that
B: T=rng RT by FINSEQ_1:52;
C: RSM is FinSequence of S by A,FINSEQ_1:def 4;
RT is FinSequence of S by B,FINSEQ_1:def 4;
then consider P be finite Subset of S such that
D: P is a_partition of (meet rng RSM) \ Union RT
by C,Lem9;
thus thesis by A,B,D;
end;
Lem10:
for S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X,
SM be FinSequence of S holds
ex P be finite Subset of S st P is a_partition of Union SM &
for n be Nat st n in dom SM holds
SM.n = union {s where s is Element of S:s in P & s c= SM.n}
proof
let S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X;
let SM be FinSequence of S;
per cases;
suppose
A0: S is empty;
{} is finite Subset of S &
{} is a_partition of Union SM & for n be Nat st n in dom SM holds
SM.n = union {s where s is Element of S:s in {} & s c= SM.n}
by A0,ZFMISC_1:2,EQREL_1:45;
hence thesis;
end;
suppose
A1: S is non empty;
defpred FF[object,object] means
ex A1 being set st A1 = $1 & A1 c= rng SM &
$2 is finite Subset of S &
$2 is a_partition of (meet A1)\union((rng SM)\A1);
set FFIN={s where s is Subset of S:s c= rng SM};
set FFOUT={s where s is finite Subset of S:ex K be set st
K c= rng SM & s is a_partition of
(meet K \ union ((rng SM)\K))};
A5: for x being object st x in FFIN holds
ex y be object st y in FFOUT & FF[x,y]
proof
let x be object;
assume x in FFIN;
then consider s0 be Subset of S such that
A6: x=s0 & s0 c= rng SM;
consider PK be finite Subset of S such that
A7: PK is a_partition of
(meet s0 \ union ((rng SM)\s0)) by A6,Thm3;
PK in FFOUT by A6,A7;
hence thesis by A6,A7;
end;
consider ff be Function such that
A8: dom ff=FFIN & rng ff c= FFOUT and
A9: for x being object st x in FFIN holds
FF[x,ff.x] from FUNCT_1:sch 6(A5);
set FFALL=Union ff;
A10: for x be set st x in FFALL ex x0 be set st
x0 in dom ff & x in ff.x0 & x0 c= rng SM & ff.x0 is finite Subset of S &
ff.x0 is a_partition of (meet x0)\union((rng SM)\x0)
proof
let x be set;
assume x in FFALL;
then consider x0 be set such that
A11: x in x0 & x0 in rng ff by TARSKI:def 4;
consider a0 be object such that
A12: a0 in dom ff & x0=ff.a0 by A11,FUNCT_1:def 3;
FF[a0,ff.a0] by A8,A9,A12;
hence thesis by A11,A12;
end;
A13: FFALL is finite Subset of S
proof
A14: FFALL c= S
proof
let x be object;
assume x in FFALL;
then consider x0 be set such that
A15: x in x0 & x0 in rng ff by TARSKI:def 4;
consider a0 be object such that
A16: a0 in dom ff & x0=ff.a0 by A15,FUNCT_1:def 3;
FF[a0,ff.a0] by A8,A9,A16;
hence thesis by A15,A16;
end;
FFALL is finite
proof
A18: FFIN is finite
proof
FFIN c= bool rng SM
proof
let x be object;
assume x in FFIN;
then consider s0 be Subset of S such that
A19: x=s0 & s0 c= rng SM;
thus thesis by A19;
end;
hence thesis;
end;
Union ff is finite
proof
for zz be set st zz in rng ff holds zz is finite
proof
let zz be set;
assume zz in rng ff;
then consider z0 be object such that
A20: z0 in FFIN & zz=ff.z0 by A8,FUNCT_1:def 3;
FF[z0,ff.z0] by A9,A20;
hence thesis by A20;
end;
hence thesis by A8,A18,FINSET_1:8,FINSET_1:7;
end;
hence thesis;
end;
hence thesis by A14;
end;
A21: for x be set st x in FFALL holds x c= union (rng SM)
proof
let x be set;
assume x in FFALL;
then consider x0 be set such that
A22: x in x0 & x0 in rng ff by TARSKI:def 4;
consider a0 be object such that
A23: a0 in dom ff & x0=ff.a0 by A22,FUNCT_1:def 3;
reconsider a0 as set by TARSKI:1;
A24: FF[a0,ff.a0] by A8,A9,A23;
meet(a0)\union((rng SM)\a0) c= union (rng SM)
proof
let x be object;
assume
A25: x in meet(a0)\union((rng SM)\a0);
x in Union SM
proof
per cases;
suppose a0 is empty;
hence thesis by A25,SETFAM_1:1;
end;
suppose not a0 is empty;
then consider y0 be object such that
A26: y0 in a0;
reconsider y0 as set by TARSKI:1;
x in y0 & y0 in rng SM by A24,A25,A26,SETFAM_1:def 1;
hence thesis by TARSKI:def 4;
end;
end;
hence thesis;
end;
hence thesis by A22,A23,A24,XBOOLE_1:1;
end;
A27: FFALL is a_partition of union (rng SM)
proof
A28: FFALL c= bool union(rng SM)
proof
let x be object;
assume
B01: x in FFALL;
reconsider x as set by TARSKI:1;
x c= Union SM by B01,A21;
hence thesis;
end;
A29: union FFALL = union (rng SM)
proof
A30: union FFALL c= union (rng SM)
proof
union FFALL c= union bool union (rng SM) by A28,ZFMISC_1:77;
hence thesis by ZFMISC_1:81;
end;
union (rng SM) c= union FFALL
proof
let x be object;
assume
A31: x in union (rng SM);
for x be set st x in union (rng SM) holds
ex aa be set st aa in dom ff & x in meet(aa)\union((rng SM)\aa)
proof
let x be set;
assume
A32: x in union (rng SM);
defpred PP[FinSequence] means
for x be set st x in union (rng $1) holds
ex aa be Subset of S st aa c= rng $1 &
x in meet(aa)\union((rng $1)\aa);
A33: for p be FinSequence of S,t be Element of S st
PP[p] holds PP[p^<*t*>]
proof
let p be FinSequence of S;
let t be Element of S;
assume
A34: PP[p];
for x be set st x in union (rng (p^<*t*>)) holds
ex aa be Subset of S st aa c= rng (p^<*t*>) &
x in meet(aa)\union((rng (p^<*t*>))\aa)
proof
let x be set;
assume x in union(rng(p^<*t*>));
then x in union (rng p \/ rng <*t*>) by FINSEQ_1:31;
then x in Union p \/ Union <*t*> by ZFMISC_1:78;
then
A34a: x in Union p \/ union {t} by FINSEQ_1:38;
A36: (x in Union p & x in t) implies
ex aa be Subset of S st aa c= rng (p^<*t*>) &
x in meet(aa)\union((rng (p^<*t*>))\aa)
proof
assume
A37: x in Union p;
assume
A38: x in t;
consider aa1 be Subset of S such that
A39: aa1 c= rng p &
x in meet(aa1)\union((rng p)\aa1) by A34,A37;
set aa=aa1\/{t};
take aa;
A40: {t} is Subset of S & aa1 is Subset of S by A1,SUBSET_1:33;
A41: aa c= rng (p^<*t*>)
proof
rng (p^<*t*>)=rng p \/ rng <*t*> by FINSEQ_1:31;
then
A42: rng (p^<*t*>)=rng p \/ {t} by FINSEQ_1:38;
A43: aa1 c= rng p \/ {t} by A39,XBOOLE_1:10;
{t} c= rng p \/ {t} by XBOOLE_1:7;
hence thesis by A42,A43,XBOOLE_1:8;
end;
aa1<>{} implies x in meet(aa)\union(rng(p^<*t*>)\aa)
proof
assume
A44: aa1<>{};
x in meet(aa1) & x in meet({t}) by A38,A39,SETFAM_1:10;
then
A45: x in meet(aa1)/\meet({t}) by XBOOLE_0:def 4;
A46: rng (p^<*t*>)=rng p \/ rng <*t*> by FINSEQ_1:31;
(rng p \/ {t})\(aa1\/{t})=
(rng p \(aa1\/{t})) \/ ({t}\(aa1\/{t}))
by XBOOLE_1:42;
then (rng p \/ {t})\(aa1\/{t})=
(rng p \(aa1\/{t})) \/ {} by XBOOLE_1:46;
then rng(p^<*t*>)\aa=rng p\(aa1\/{t}) by A46,FINSEQ_1:38;
then rng(p^<*t*>)\aa=((rng p)\aa1)/\ ((rng p)\{t})
by XBOOLE_1:53;
then
A47: union (rng(p^<*t*>)\aa) c= union((rng p)\aa1)
by ZFMISC_1:77,XBOOLE_1:17;
not x in union (rng(p^<*t*>)\aa) & x in meet aa
by A39,A44,A45,A47,SETFAM_1:9,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by A39,A40,A41,XBOOLE_1:8,SETFAM_1:1;
end;
A48: (x in Union p & not x in t) implies
ex aa be Subset of S st aa c= rng (p^<*t*>) &
x in meet(aa)\union((rng (p^<*t*>))\aa)
proof
assume
A49: x in Union p;
assume
A50: not x in t;
consider aa1 be Subset of S such that
A51: aa1 c= rng p &
x in meet(aa1)\union((rng p)\aa1) by A34,A49;
set aa=aa1\{t};
A52: aa c= rng (p^<*t*>)
proof
A53: rng (p^<*t*>)=rng p \/ rng <*t*> by FINSEQ_1:31;
A54: aa1 c= rng p \/ {t} by A51,XBOOLE_1:10;
aa1\{t} c= aa1 by XBOOLE_1:36;
then aa1\{t} c= rng p \/ {t} by A54,XBOOLE_1:1;
hence thesis by A53,FINSEQ_1:38;
end;
A55: aa1 <> {} & aa1\{t}={} implies
ex aa be Subset of S st aa c= rng (p^<*t*>) &
x in meet(aa)\union(rng(p^<*t*>)\aa)
proof
assume
A56: aa1<>{};
assume aa1\{t}={};
then
A57: {t}=aa1 by A56,ZFMISC_1:58;
set aa=aa1;
A58: rng(p^<*t*>)=rng p \/ rng<*t*> by FINSEQ_1:31
.= rng p \/ {t} by FINSEQ_1:38;
A59: (rng p \/{t})\{t}=rng p \ {t} by XBOOLE_1:40;
thus thesis
by A51,A57,A58,A59,XBOOLE_1:11;
end;
aa1 <> {} & aa1\{t}<>{} implies
ex aa be Subset of S st aa c= rng (p^<*t*>) &
x in meet(aa)\union(rng(p^<*t*>)\aa)
proof
assume aa1<>{};
assume
A60: aa1\{t}<>{};
A61: for y be set st y in aa1 holds x in y\t
proof
let y be set;
assume y in aa1;
then x in y & not x in t by A50,A51,SETFAM_1:def 1;
hence thesis by XBOOLE_0:def 5;
end;
for y be set st y in aa holds x in y
proof
let y be set;
assume y in aa;
then y in aa1 & not y in {t} by XBOOLE_0:def 5;
then x in y\t & not y=t by A61,TARSKI:def 1;
hence thesis;
end;
then
A62: x in meet(aa) by A60,SETFAM_1:def 1;
rng (p^<*t*>)=rng p \/ rng <*t*> by FINSEQ_1:31;
then
A63: rng(p^<*t*>)\aa=(rng p\/ {t})\aa by FINSEQ_1:38;
A64: ({t}\aa1)\/{t} = {t} by XBOOLE_1:7,8;
rng(p^<*t*>)\aa=
(rng p \(aa1\{t})) \/ ({t}\(aa1\{t})) by A63,XBOOLE_1:42
.= (rng p \(aa1\{t})) \/ (({t}\aa1)\/({t}/\{t}))
by XBOOLE_1:52
.= ((rng p\aa1)\/(rng p /\ {t})) \/ {t}
by A64,XBOOLE_1:52
.= (rng p\aa1)\/((rng p /\ {t}) \/ {t}) by XBOOLE_1:4
.= (rng p\aa1)\/ {t} by XBOOLE_1:22;
then
A66: union(rng(p^<*t*>)\aa)
= union(rng p\aa1)\/ union({t}) by ZFMISC_1:78
.= union(rng p\aa1)\/ t;
A67: not x in t & not x in union(rng p\aa1)
implies not x in union(rng (p^<*t*>)\aa)
by A66,XBOOLE_0:def 3;
x in meet(aa)\union(rng(p^<*t*>)\aa)
by A50,A51,A62,A67,XBOOLE_0:def 5;
hence thesis by A52;
end;
then consider aa be Subset of S such that
A68: aa c= rng (p^<*t*>) &
x in meet(aa)\union((rng(p^<*t*>))\aa) by A51,A55,SETFAM_1:1;
thus thesis by A68;
end;
(not x in Union p & x in t) implies
ex aa be Subset of S st aa c= rng (p^<*t*>) &
x in meet(aa)\union((rng (p^<*t*>))\aa)
proof
assume
A69: not x in Union p;
assume
A70: x in t;
A71: rng (p^<*t*>)=rng p \/ rng <*t*> by FINSEQ_1:31
.=rng p \/ {t} by FINSEQ_1:38;
set aa={t}\(rng p);
A72: aa is Subset of S
proof
{t} is Subset of S &
rng p is Subset of S by A1,SUBSET_1:33;
hence thesis by XBOOLE_1:1;
end;
x in meet(aa)\union((rng(p^<*t*>))\aa)
proof
A73: x in meet({t}\rng p)
proof
per cases;
suppose
A74: {t}\rng p <>{};
for y be set st y in {t}\rng p holds x in y
by A70,TARSKI:def 1;
hence thesis by A74,SETFAM_1:def 1;
end;
suppose {t}\rng p={};
then {t} is Subset of rng p by SUBSET_1:41,ZFMISC_1:60;
then union {t} c= Union p by ZFMISC_1:77;
hence thesis by A69,A70;
end;
end;
not x in union((rng(p^<*t*>))\aa) by A69,A71,Lem1;
hence thesis by A73,XBOOLE_0:def 5;
end;
hence thesis by A72,A71,XBOOLE_1:10;
end;
hence thesis by A34a,A36,A48,XBOOLE_0:def 3;
end;
hence thesis;
end;
A75: PP[<*>S] by ZFMISC_1:2;
for p be FinSequence of S holds
PP[p] from FINSEQ_2:sch 2(A75,A33);
then
consider aa be Subset of S such that
A76: aa c= rng SM & x in meet(aa)\union((rng SM)\aa) by A32;
take aa;
thus thesis by A8,A76;
end;
then consider aa be set such that
A77: aa in dom ff & x in meet(aa)\union((rng SM)\aa) by A31;
FF[aa,ff.aa] by A8,A9,A77;
then
A78: x in union(ff.aa) by A77,EQREL_1:def 4;
ff.aa c= Union ff
proof
let x be object;
ff.aa in rng ff by A77,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
then union (ff.aa) c= union Union ff by ZFMISC_1:77;
hence thesis by A78;
end;
hence thesis by A30;
end;
for A be Subset of union (rng SM) st A in FFALL holds
A<>{} &
for B be Subset of union (rng SM) st B in FFALL holds A=B or A misses B
proof
let A be Subset of union (rng SM);
assume
A80: A in FFALL;
consider a0 be set such that
A81: a0 in dom ff & A in ff.a0 &
a0 c= rng SM & ff.a0 is finite Subset of S &
ff.a0 is a_partition of (meet a0)\union((rng SM)\a0) by A10,A80;
for B be Subset of union (rng SM) st B in FFALL holds
A=B or A misses B
proof
let B be Subset of union (rng SM);
assume
A82: B in FFALL;
consider b0 be set such that
A83: b0 in dom ff & B in ff.b0 &
b0 c= rng SM & ff.b0 is finite Subset of S &
ff.b0 is a_partition of (meet b0)\union((rng SM)\b0) by A10,A82;
A84: a0<>b0 implies
(meet b0)\union((rng SM)\b0) misses (meet a0)\union((rng SM)\a0)
proof
assume
A85: a0<>b0;
((meet b0)\union((rng SM)\b0)) /\
((meet a0)\union((rng SM)\a0))c={}
proof
let q be object;
assume
A87: q in ((meet b0)\union((rng SM)\b0)) /\
((meet a0)\union((rng SM)\a0));
A88: (q in (meet b0) \ union((rng SM)\b0)) &
(q in (meet a0)\union((rng SM)\a0)) by A87,XBOOLE_0:def 4;
then
A89: q in meet(b0) & not q in union((rng SM)\b0) &
q in meet(a0) & not q in union((rng SM)\a0) by XBOOLE_0:def 5;
A90: not (a0 c= b0) implies q in {}
proof
assume not a0 c= b0;
then consider y0 be object such that
A91: y0 in a0 & not y0 in b0 by TARSKI:def 3;
reconsider y0 as set by TARSKI:1;
A92: q in y0 by A87,A91,SETFAM_1:def 1;
y0 in (rng SM)\b0 by A81,A91,XBOOLE_0:def 5;
hence thesis by A89,A92,TARSKI:def 4;
end;
not (b0 c= a0) implies q in {}
proof
assume not (b0 c= a0);
then consider y0 be object such that
A99: y0 in b0 & not y0 in a0 by TARSKI:def 3;
reconsider y0 as set by TARSKI:1;
A100: q in y0 by A88,A99,SETFAM_1:def 1;
y0 in (rng SM)\a0 by A83,A99,XBOOLE_0:def 5;
hence thesis by A89,A100,TARSKI:def 4;
end;
hence thesis by A85,A90;
end;
hence thesis;
end;
thus thesis by A81,A83,A84,EQREL_1:def 4,XBOOLE_1:64;
end;
hence thesis by A81;
end;
hence thesis by A28,A29,EQREL_1:def 4;
end;
for n be Nat st n in dom SM holds
SM.n = union {s where s is Element of S:s in FFALL & s c= SM.n}
proof
let n be Nat;
assume
A101: n in dom SM;
A102: SM.n c= union {s where s is Element of S:s in FFALL & s c= SM.n}
proof
let x be object;
assume
A103: x in SM.n;
A104: union(FFALL)=union(rng SM) by A27,EQREL_1:def 4;
x in SM.n & SM.n in rng SM by A101,A103,FUNCT_1:def 3;
then
A105: x in union(rng SM) by TARSKI:def 4;
consider y0 be set such that
A106: x in y0 & y0 in FFALL by A104,A105,TARSKI:def 4;
consider d0 be set such that
A107: d0 in dom ff & y0 in ff.d0 &
d0 c= rng SM & ff.d0 is finite Subset of S &
ff.d0 is a_partition of (meet d0)\union((rng SM)\d0) by A10,A106;
y0 c= SM.n
proof
let u be object;
assume u in y0;
then
A108: u in (meet d0)\union((rng SM)\d0) by A107;
A109: {SM.n} c= d0 implies u in SM.n
proof
assume
A110: {SM.n} c= d0;
A111: SM.n in {SM.n} by TARSKI:def 1;
thus thesis by A108,A110,A111,SETFAM_1:def 1;
end;
not {SM.n} c= d0 implies u in SM.n
proof
assume not {SM.n} c= d0;
then consider yy be object such that
A112: yy in {SM.n} & not yy in d0 by TARSKI:def 3;
SM.n in rng SM & not SM.n in d0
by A101,A112,FUNCT_1:def 3,TARSKI:def 1;
then SM.n in rng SM \ d0 by XBOOLE_0:def 5;
then x in union (rng SM\d0) by A103,TARSKI:def 4;
hence thesis by A106,A107,XBOOLE_0:def 5;
end;
hence thesis by A109;
end;
then x in y0 & y0 in {s where s is Element of S:s in FFALL &
s c= SM.n} by A106,A107;
hence thesis by TARSKI:def 4;
end;
union {s where s is Element of S:s in FFALL & s c= SM.n} c= SM.n
proof
let x be object;
assume x in union {s where s is Element of S:s in FFALL & s c= SM.n};
then consider y be set such that
A113: x in y &
y in {s where s is Element of S:s in FFALL & s c= SM.n}
by TARSKI:def 4;
consider s0 be Element of S such that
A114: y=s0 & s0 in FFALL & s0 c= SM.n by A113;
thus thesis by A113,A114;
end;
hence thesis by A102;
end;
hence thesis by A13,A27;
end;
end;
theorem Thm87:
for S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X, SM be finite Subset of S holds
ex P be finite Subset of S st P is a_partition of union SM &
for Y be Element of SM holds
Y=union {s where s is Element of S:s in P & s c= Y}
proof
let S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X;
let SM be finite Subset of S;
per cases;
suppose
A1: SM is empty;
for Y be Element of SM holds
Y=union{s where s is Element of S:s in {} & s c= Y}
proof
let Y be Element of SM;
A2: Y={} by A1,SUBSET_1:def 1;
union{s where s is Element of S:s in {} & s c= Y} c= {}
proof
let x be object;
assume x in union{s where s is Element of S:s in {} & s c= Y};
then consider y be set such that
x in y and
A3: y in {s where s is Element of S:s in {} & s c= Y} by TARSKI:def 4;
consider s be Element of S such that
y=s and
A4: s in {} and
s c= Y by A3;
thus thesis by A4;
end;
hence thesis by A2;
end;
hence thesis by A1,ZFMISC_1:2,EQREL_1:45;
end;
suppose
A5: SM is non empty;
consider FSM be FinSequence such that
A6: SM=rng FSM by FINSEQ_1:52;
FSM is FinSequence of S by A6,FINSEQ_1:def 4;
then consider P be finite Subset of S such that
A7: P is a_partition of Union FSM and
A8: for n be Nat st n in dom FSM holds FSM.n=union{s where s is Element of S:
s in P & s c= FSM.n} by Lem10;
for Y be Element of SM holds
Y=union{s where s is Element of S:s in P & s c= Y}
proof
let Y be Element of SM;
consider i be object such that
A9: i in dom FSM and
A10: Y=FSM.i by A5,A6,FUNCT_1:def 3;
thus Y c= union {s where s is Element of S:s in P & s c= Y}
by A9,A10,A8;
thus union {s where s is Element of S:s in P & s c= Y} c= Y
by A9,A10,A8;
end;
hence thesis by A6,A7;
end;
end;
Lem11:
for S be cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of X,
SM be Function of NATPLUS, S,
n be NatPlus,x be set st
x in SM.n holds
ex n0 be NatPlus, np be Nat st n0 <= n &
np=n0-1 & x in (SM.n0)\Union(SM|Seg np)
proof
let S be cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of X;
let SM be Function of NATPLUS, S;
let n be NatPlus;
let x be set;
assume
A1: x in SM.n;
defpred Q[Nat] means
$1 is NatPlus & for y be set st y in SM.$1 holds
(ex n1,n0 be NatPlus,np be Nat st
$1=n1 & n0 <= n1 & np=n0-1 &
y in (SM.n0)\Union(SM|Seg np));
A2: for k be Nat st k >=1 &
(for l be Nat st l >=1 & l < k holds Q[l]) holds Q[k]
proof
let k be Nat;
assume
A3: k>=1;
assume
A4: for l be Nat st l>=1 & l<k holds Q[l];
A5: k is NatPlus by A3,NAT_LAT:def 6;
for y be set st y in SM.k holds
(ex n1,n0 be NatPlus,np be Nat st
k=n1 & n0 <= n1 & np=n0-1 &
y in (SM.n0)\Union(SM|Seg np))
proof
let y be set;
assume
A6: y in SM.k;
set k0=k-1;
reconsider k0 as Nat by A3,CHORD:1;
set n1=k;
A7: SM.k=((SM.k)\(Union(SM|Seg k0)))\/ ((SM.k)/\(Union(SM|Seg k0)))
by XBOOLE_1:51;
A8: y in SM.k\Union(SM|Seg k0) implies
(ex n1,n0 be NatPlus,np be Nat st
k=n1 & n0 <= n1 & np=n0-1 &
y in (SM.n0)\Union(SM|Seg np))
proof
assume
A9: y in SM.k\Union(SM|Seg k0);
n1 is NatPlus by A3,NAT_LAT:def 6;
hence thesis by A9;
end;
y in SM.k/\Union(SM|Seg k0) implies
(ex n1,n0 be NatPlus,np be Nat st
k=n1 & n0 <= n1 & np=n0-1 &
y in (SM.n0)\Union(SM|Seg np))
proof
assume y in SM.k/\Union(SM|Seg k0);
then y in Union(SM|Seg k0) by XBOOLE_0:def 4;
then consider yy be set such that
A10: y in yy & yy in rng(SM|Seg k0) by TARSKI:def 4;
consider yyy be object such that
A11: yyy in dom (SM|Seg k0)& yy=(SM|Seg k0).yyy
by A10,FUNCT_1:def 3;
reconsider yyy as Nat by A11;
A12: y in SM.yyy by A10,A11,FUNCT_1:47;
A13: 1 <= yyy & yyy <= k0 by A11,FINSEQ_1:1;
set kk=k-1;
A14: kk is Nat by A3,CHORD:1;
yyy <= kk by A11,FINSEQ_1:1;
then yyy < k - 1 + 1 & k = k - 1 + 1 by A14,NAT_1:13;
then yyy>=1 & yyy<k by A11,FINSEQ_1:1;
then consider n1,n0 be NatPlus,np be Nat such that
A15: yyy=n1 & n0 <= n1 & np=n0-1 &
y in (SM.n0)\Union(SM|Seg np) by A4,A12;
A16: n0 <= k - 1 by A13,A15,XXREAL_0:2;
k - 1 + 1 = k;
then
A17: k - 1 <= k by INT_1:6;
set n2=k;
thus thesis by A5,A15,A16,A17,XXREAL_0:2;
end;
hence thesis by A6,A7,A8,XBOOLE_0:def 3;
end;
hence thesis by A3,NAT_LAT:def 6;
end;
A18: for k be Nat st k >= 1 holds Q[k] from NAT_1:sch 9(A2);
for k be NatPlus holds Q[k]
proof
let k be NatPlus;
k>=1 by CHORD:1;
hence thesis by A18;
end;
then consider n1,n0 be NatPlus,np be Nat such that
A19: n=n1 & n0 <= n1 & np=n0-1 &
x in (SM.n0)\Union(SM|Seg np) by A1;
thus thesis by A19;
end;
theorem Thm4:
for S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X,SM be Function of NATPLUS,S holds
ex P be countable Subset of S st P is a_partition of Union SM &
for n be NatPlus holds Union (SM|Seg n)= union{s where s is Element of S:
s in P & s c= Union (SM|Seg n)}
proof
let S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X;
let SM be Function of NATPLUS,S;
per cases;
suppose
A1: S ={};
then
A2: Union SM ={} by ZFMISC_1:2;
set P={};
A3: P is finite Subset of S & P is a_partition of {}
by SUBSET_1:1,EQREL_1:45;
for n be NatPlus holds Union (SM|Seg n)= union{s where s is Element of S:
s in P & s c= Union (SM|Seg n)}
proof
let n be NatPlus;
thus Union (SM|Seg n) c= union{s where s is Element of S:
s in P & s c= Union (SM|Seg n)}
proof
let x be object;
assume x in Union (SM|Seg n);
hence thesis by A1,ZFMISC_1:2;
end;
thus union{s where s is Element of S: s in P &
s c= Union (SM|Seg n)} c= Union (SM|Seg n)
proof
let x be object;
assume x in union{s where s is Element of S: s in P &
s c= Union (SM|Seg n)};
then consider y be set such that
A5: x in y and
A6: y in {s where s is Element of S: s in P & s c= Union (SM|Seg n)}
by TARSKI:def 4;
consider s0 be Element of S such that
A7: y=s0 and
s0 in P and
A8: s0 c= Union (SM|Seg n) by A6;
thus thesis by A5,A7,A8;
end;
end;
hence thesis by A2,A3;
end;
suppose
A9: not S = {};
then
A10: dom SM = NATPLUS by FUNCT_2:def 1;
A11: for x be NatPlus ex x1 be Nat st x1=x-1 &
ex Px be finite Subset of S st
Px is a_partition of SM.x\Union (SM|Seg x1)
proof
let x be NatPlus;
set x1=x-1;
reconsider x1 as Nat by CHORD:1;
rng (SM|(Seg x1)) is finite Subset of S;
then ex P be finite Subset of S
st P is a_partition of SM.x\Union (SM|Seg x1) by Thm1;
hence thesis;
end;
defpred FH[object,object] means
ex x,xp be Nat st $1=x & xp=x-1 &
$2 is finite Subset of S &
$2 is a_partition of (SM.x)\Union (SM|Seg xp);
A12: for n be object st n in NATPLUS
ex y be object st y in bool S & FH[n,y]
proof
let n be object;
assume n in NATPLUS;
then consider n1 be NatPlus such that
A13: n=n1;
reconsider n as NatPlus by A13;
consider x1 be Nat such that
A14: x1=n-1 & ex Px be finite Subset of S st
Px is a_partition of SM.n\Union (SM|Seg x1) by A11;
thus thesis by A14;
end;
consider fi be Function such that
A15: dom fi=NATPLUS & rng fi c= bool S and
A16: for n be object st n in NATPLUS holds FH[n,fi.n] from FUNCT_1:sch 6(A12);
A17: Union fi is countable Subset of S &
Union fi is a_partition of Union SM
proof
A18: Union fi is countable Subset of S
proof
A19: Union fi is countable
proof
for v be set st v in dom fi holds fi.v is countable
proof
let v be set;
assume v in dom fi;
then FH[v,fi.v] by A15,A16;
hence thesis;
end;
hence thesis by A15,CARD_4:11;
end;
Union fi c= S
proof
let u be object;
assume u in Union fi;
then ex v be set st u in v & v in rng fi by TARSKI:def 4;
hence thesis by A15;
end;
hence thesis by A19;
end;
A21: Union fi is a_partition of Union SM
proof
A22: Union fi c= bool Union SM
proof
let w be object;
assume w in Union fi;
then consider w0 be set such that
A23: w in w0 & w0 in rng fi by TARSKI:def 4;
consider v0 be object such that
A24: v0 in dom fi & w0=fi.v0 by A23,FUNCT_1:def 3;
reconsider w as set by TARSKI:1;
w c= union (rng SM)
proof
let v be object;
assume
A25: v in w;
consider mx,mxp be Nat such that
A26: v0=mx & mxp=mx-1 &
fi.v0 is finite Subset of S &
fi.v0 is a_partition of (SM.mx)\Union (SM|Seg mxp)
by A15,A16,A24;
A27: v in (SM.mx)\Union (SM|Seg mxp) by A23,A24,A25,A26;
mx in dom SM by A9,A15,A24,A26,FUNCT_2:def 1;
then SM.mx in rng SM by FUNCT_1:def 3;
hence thesis by A27,TARSKI:def 4;
end;
hence thesis;
end;
A28: union Union fi = Union SM
proof
thus union Union fi c= Union SM
proof
union Union fi c= union bool Union SM by A22,ZFMISC_1:77;
hence thesis by ZFMISC_1:81;
end;
let v be object;
assume v in Union SM;
then consider v0 be set such that
A30: v in v0 & v0 in rng SM by TARSKI:def 4;
consider v1 be object such that
A31: v1 in dom SM &
v0=SM.v1 by A30,FUNCT_1:def 3;
reconsider v1 as NatPlus by A31;
consider n0 be NatPlus, np be Nat such that
A32: n0<= v1 & np=n0-1 & v in (SM.n0)\Union(SM|Seg np)
by A30,A31,Lem11;
FH[n0,fi.n0] by A16;
then consider x,xp be Nat such that
A33: n0=x & xp=x-1 &
fi.n0 is finite Subset of S &
fi.n0 is a_partition of (SM.n0)\Union (SM|Seg xp);
A34: union (fi.n0)=(SM.n0)\Union(SM|Seg xp) by A33,EQREL_1:def 4;
fi.n0 c= Union fi
proof
fi.n0 in rng fi by A15,FUNCT_1:def 3;
hence thesis by ZFMISC_1:74;
end;
then union (fi.n0) c= union Union fi by ZFMISC_1:77;
hence thesis by A32,A33,A34;
end;
for A be Subset of Union SM st A in Union fi holds A<>{} &
for B be Subset of Union SM st B in Union fi holds
A = B or A misses B
proof
let A be Subset of Union SM;
assume A in Union fi;
then consider a0 be set such that
A35: A in a0 & a0 in rng fi by TARSKI:def 4;
consider a1 be object such that
A36: a1 in dom fi & a0=fi.a1 by A35,FUNCT_1:def 3;
FH[a1,fi.a1] by A15,A16,A36;
then consider xa,xap be Nat such that
A37: a1=xa & xap=xa-1 &
fi.a1 is finite Subset of S &
fi.a1 is a_partition of (SM.a1)\Union (SM|Seg xap);
for B be Subset of Union SM st B in Union fi holds
A=B or A misses B
proof
let B be Subset of Union SM;
assume B in Union fi;
then consider b0 be set such that
A38: B in b0 & b0 in rng fi by TARSKI:def 4;
consider b1 be object such that
A39: b1 in dom fi & b0=fi.b1 by A38,FUNCT_1:def 3;
FH[b1,fi.b1] by A15,A16,A39;
then consider xb,xbp be Nat such that
A40: b1=xb & xbp=xb-1 &
fi.b1 is finite Subset of S &
fi.b1 is a_partition of (SM.b1)\Union (SM|Seg xbp);
not a1=b1 implies A=B or A misses B
proof
assume
A41: not a1=b1;
reconsider a1 as NatPlus by A15,A36;
reconsider b1 as NatPlus by A15,A39;
(SM.a1)\Union(SM|Seg xap) misses (SM.b1)\Union(SM|Seg xbp)
proof
A42: a1 < b1 implies (SM.a1)\Union(SM|Seg xap)
misses (SM.b1)\Union(SM|Seg xbp)
proof
assume
A43: a1 < b1;
assume not (((SM.a1)\Union(SM|Seg xap))
misses ((SM.b1)\Union(SM|Seg xbp)));
then consider u be object such that
A44: u in ((SM.a1)\Union(SM|Seg xap)) /\
((SM.b1)\Union(SM|Seg xbp)) by XBOOLE_0:def 1;
A45: u in ((SM.a1)\Union(SM|Seg xap)) & u in
((SM.b1)\Union(SM|Seg xbp))
by A44,XBOOLE_0:def 4;
u in SM.a1 implies u in Union (SM|Seg xbp)
proof
assume
A46: u in SM.a1;
A47: 1 <= a1 by CHORD:1;
xa < xbp+1 by A37,A40,A43;
then xa <= xbp by NAT_1:13;
then
A48: xa in Seg xbp by A37,A47;
A49: a1 in dom (SM|Seg xbp) by A10,A37,A48,RELAT_1:57;
then (SM|Seg xbp).a1 in rng (SM|Seg xbp)
by FUNCT_1:def 3;
then SM.a1 in rng (SM|Seg xbp) by A49,FUNCT_1:47;
then SM.a1 c= Union (SM|Seg xbp) by ZFMISC_1:74;
hence thesis by A46;
end;
hence thesis by A45,XBOOLE_0:def 5;
end;
b1 < a1 implies (SM.a1)\Union(SM|Seg xap) misses
(SM.b1)\Union(SM|Seg xbp)
proof
assume
A50: b1 < a1;
assume
A51: not (((SM.a1)\Union(SM|Seg xap)) misses
((SM.b1)\Union(SM|Seg xbp)));
A52: not ((SM.a1)\Union(SM|Seg xap)) /\
((SM.b1)\Union(SM|Seg xbp)) is empty by A51;
consider u be object such that
A53: u in ((SM.a1)\Union(SM|Seg xap)) /\
((SM.b1)\Union(SM|Seg xbp)) by A52;
A54: u in ((SM.a1)\Union(SM|Seg xap)) &
u in((SM.b1)\Union(SM|Seg xbp))
by A53,XBOOLE_0:def 4;
u in SM.b1 implies u in Union (SM|Seg xap)
proof
assume
A55: u in SM.b1;
A56: 1 <= b1 by CHORD:1;
xb < xap+1 by A37,A40,A50;
then xb <= xap by NAT_1:13;
then
A57: b1 in Seg xap by A40,A56;
A58: b1 in dom (SM|Seg xap) by A10,A57,RELAT_1:57;
then (SM|Seg xap).b1 in rng (SM|Seg xap)
by FUNCT_1:def 3;
then SM.b1 in rng (SM|Seg xap) by A58,FUNCT_1:47;
then SM.b1 c= Union (SM|Seg xap) by ZFMISC_1:74;
hence thesis by A55;
end;
hence thesis by A54,XBOOLE_0:def 5;
end;
hence thesis by A41,A42,XXREAL_0:1;
end;
hence thesis by A35,A36,A37,A38,A39,A40,XBOOLE_1:64;
end;
hence thesis by A35,A36,A37,A38,A39,EQREL_1:def 4;
end;
hence thesis by A35,A36,A37;
end;
hence thesis by A22,A28,EQREL_1:def 4;
end;
thus thesis by A18,A21;
end;
A59: for l be Nat holds
{s where s is Element of S:s in Union fi & s c= Union (SM|Seg l)}=
Union fi /\ bool (Union(SM|Seg l))
proof
let l be Nat;
A60: {s where s is Element of S:s in Union fi & s c= Union (SM|Seg l)} c=
Union fi /\ bool (Union(SM|Seg l))
proof
let v be object;
assume v in {s where s is Element of S:s in Union fi &
s c= Union (SM|Seg l)};
then consider s0 be Element of S such that
A61: v=s0 &
s0 in Union fi & s0 c= Union(SM|Seg l);
thus thesis by A61,XBOOLE_0:def 4;
end;
Union fi /\ bool (Union(SM|Seg l)) c=
{s where s is Element of S:s in Union fi & s c= Union (SM|Seg l)}
proof
let v be object;
assume
A62: v in Union fi /\ bool (Union(SM|Seg l));
then v in Union fi & v in bool (Union(SM|Seg l)) by XBOOLE_0:def 4;
then consider v0 be set such that
A63: v in v0 &
v0 in rng fi by TARSKI:def 4;
consider n0 be object such that
A64: n0 in dom fi & v0=fi.n0 by A63,FUNCT_1:def 3;
FH[n0,fi.n0] by A15,A16,A64;
then consider x,xp be Nat such that
A65: n0=x & xp=x-1 &
fi.n0 is finite Subset of S &
fi.n0 is a_partition of (SM.n0)\Union (SM|Seg xp);
v in S & v in Union fi & v in bool (Union(SM|Seg l))
by A62,A63,A64,A65,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by A60;
end;
for n be NatPlus holds
Union (SM|Seg n)=
union{s where s is Element of S:s in Union fi & s c= Union (SM|Seg n)}
proof
let n be NatPlus;
A66: Union (SM|Seg n) c= Union SM by ZFMISC_1:77,RELAT_1:70;
Union (SM|Seg n) = union(Union fi /\ bool (Union(SM|Seg n)))
proof
A67: Union (SM|Seg n) c= union(Union fi /\ bool (Union(SM|Seg n)))
proof
let v be object;
assume
A68: v in Union (SM|Seg n);
then v in Union SM by A66;
then v in union Union fi by A17,EQREL_1:def 4;
then consider v0 be set such that
A69: v in v0 & v0 in Union fi by TARSKI:def 4;
v0 c= Union(SM|Seg n)
proof
consider v1 be set such that
A70: v0 in v1 & v1 in rng fi by A69,TARSKI:def 4;
consider v2 be object such that
A71: v2 in dom fi & v1=fi.v2 by A70,FUNCT_1:def 3;
FH[v2,fi.v2] by A15,A16,A71;
then consider x2,x2p be Nat such that
A72: v2=x2 & x2p=x2-1 &
fi.v2 is finite Subset of S &
fi.v2 is a_partition of (SM.v2)\Union (SM|Seg x2p);
not v in Union(SM|Seg x2p) &
v in Union(SM|Seg n) by A68,A69,A70,A71,A72,XBOOLE_0:def 5;
then
A73: v in Union(SM|Seg n) \ Union(SM|Seg x2p) by XBOOLE_0:def 5;
A74: for n1,n2 be Nat st n1<=n2 holds
Union(SM|Seg n1) c= Union(SM|Seg n2)
proof
let n1,n2 be Nat;
assume n1<=n2;
then SM|Seg n1 c= SM|Seg n2 by FINSEQ_1:5,RELAT_1:75;
hence thesis by RELAT_1:11,ZFMISC_1:77;
end;
A75: for n1,n2 be Nat st n1<=n2 holds
Union(SM|Seg n1) \ Union(SM|Seg n2) ={}
proof
let n1,n2 be Nat;
assume n1<=n2;
then
A76: SM|Seg n1 c= SM|Seg n2 by FINSEQ_1:5,RELAT_1:75;
Union(SM|Seg n1) c= Union(SM|Seg n2)
by A76,RELAT_1:11,ZFMISC_1:77;
hence thesis by XBOOLE_1:37;
end;
(x2 - 1) + 1 <= n + 1 by XREAL_1:6,A72,A73,A75;
then
A77: x2 <= n or x2 = n+1 by NAT_1:8;
reconsider v2 as Nat by A72;
A78: v0 c= SM.v2 by A70,A71,A72,XBOOLE_1:1;
for x be set,i,j be Nat st x c= SM.i & i<=j holds
x c= Union (SM|Seg j)
proof
let x be set;
let i,j be Nat;
assume
A79: x c= SM.i;
assume
A80: i<=j;
A81: (SM.i) c= Union (SM|Seg i)
proof
let y be object;
assume
A82: y in SM.i;
per cases;
suppose i is zero;
then not i in dom SM;
hence thesis by A82,FUNCT_1:def 2;
end;
suppose i is non zero;
then
A83: 1<=i & i <= i by CHORD:1;
Seg i c= dom SM
proof
let o be object;
assume
A84: o in Seg i;
then reconsider o as Nat;
o is non zero by A84,FINSEQ_1:1;
hence thesis by A10,NAT_LAT:def 6;
end;
then
A85: dom (SM|Seg i)=Seg i by RELAT_1:62;
A86: SM.i=(SM|Seg i).i by A83,A85,FINSEQ_1:1,FUNCT_1:47;
(SM|Seg i).i in rng (SM|Seg i)
by A83,A85,FINSEQ_1:1,FUNCT_1:3;
then
SM.i c= Union (SM|Seg i) by A86,ZFMISC_1:74;
hence thesis by A82;
end;
end;
Union (SM|Seg i) c= Union (SM|Seg j) by A74,A80;
then (SM.i) c= Union (SM|Seg j) by A81,XBOOLE_1:1;
hence thesis by A79,XBOOLE_1:1;
end;
hence thesis by A77,A72,A68,A69,A70,A71,A78,XBOOLE_0:def 5;
end;
then v in v0 & v0 in Union fi /\ bool (Union (SM|Seg n))
by A69,XBOOLE_0:def 4;
hence thesis by TARSKI:def 4;
end;
union(Union fi /\ bool (Union(SM|Seg n))) c=
Union (SM|Seg n)
proof
A87: union Union fi /\ union bool (Union(SM|Seg n))=
union Union fi /\ Union (SM|Seg n) by ZFMISC_1:81;
union Union fi = Union SM by A17,EQREL_1:def 4;
then union(Union fi /\ bool (Union(SM|Seg n))) c=
Union SM /\ Union(SM|Seg n) by A87,ZFMISC_1:79;
hence thesis by A66,XBOOLE_1:28;
end;
hence thesis by A67;
end;
hence thesis by A59;
end;
hence thesis by A17;
end;
end;
begin :: Countable Covers
definition
let X be set;
let S be Subset-Family of X;
attr S is with_countable_Cover means
ex XX be countable Subset of S st XX is Cover of X;
end;
Lem6a:
for X be set, S be Subset-Family of X, XX be Subset of S holds union XX=X
iff XX is Cover of X
proof
let X be set, S be Subset-Family of X, XX be Subset of S;
XX is Subset-Family of X by XBOOLE_1:1;
hence thesis by SETFAM_1:45;
end;
registration
let X;
cluster cobool X -> with_countable_Cover;
coherence
proof
{X} is countable Subset of cobool X & union {X}=X by ZFMISC_1:7;
hence thesis by Lem6a;
end;
end;
registration
let X;
cluster diff-c=-finite-partition-closed diff-finite-partition-closed
cap-finite-partition-closed with_empty_element with_countable_Cover
for Subset-Family of X;
existence
proof
take cobool X;
thus thesis;
end;
end;
theorem
for S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X st S is with_countable_Cover holds
ex P be countable Subset of S st P is a_partition of X
proof
let S be cap-finite-partition-closed diff-c=-finite-partition-closed
Subset-Family of X;
assume S is with_countable_Cover;
then consider XX be countable Subset of S such that
A1: XX is Cover of X;
per cases;
suppose
C1: S is empty;
X c= union XX by A1,SETFAM_1:def 11;
then
C2: X is empty by C1,ZFMISC_1:2;
set P={};
P is countable Subset of S by SUBSET_1:1;
hence thesis by C2,EQREL_1:45;
end;
suppose
B0: S is non empty;
A2: X c= union XX by A1,SETFAM_1:def 11;
per cases;
suppose
A3: X is empty;
{} is countable Subset of S by SUBSET_1:1;
hence thesis by A3,EQREL_1:45;
end;
suppose
A5: not X is empty;
A6: ex g be Function of NATPLUS,S st rng g=XX
proof
consider f be Function of omega,XX such that
A7: rng f=XX by A5,A2,ZFMISC_1:2,CARD_3:96;
reconsider f as Function of NAT,XX;
defpred G[object,object] means
$1 in NATPLUS &
ex xx be Nat st xx+1=$1 & $2=f.xx;
A8: for x, y1,y2 be object st x in NATPLUS & G[x,y1] & G[x,y2] holds y1=y2;
A9: for x be object st x in NATPLUS ex y be object st G[x,y]
proof
let x be object;
assume
A10: x in NATPLUS;
then reconsider x as Nat;
A11: x-1 is Nat by A10,CHORD:1;
x-1+1=x;
then consider xx be Nat such that
A12: xx+1=x by A11;
set y=f.xx;
x in NATPLUS & ex xx be Nat st xx+1 =x & y=f.xx by A10,A12;
hence thesis;
end;
consider g being Function such that
A13: dom g = NATPLUS &
for a be object st a in NATPLUS holds G[a,g.a]
from FUNCT_1:sch 2(A8,A9);
A14: rng g =XX
proof
A15: rng g c= XX
proof
let x be object;
assume x in rng g;
then consider y be object such that
A16: y in dom g & x=g.y by FUNCT_1:def 3;
consider xx be Nat such that
A17: xx+1=y &g.y=f.xx by A13,A16;
xx is Nat & dom f=NAT by A5,A2,ZFMISC_1:2,FUNCT_2:def 1;
then xx in dom f by ORDINAL1:def 12;
then x in rng f by A16,A17,FUNCT_1:def 3;
hence thesis;
end;
XX c= rng g
proof
let x be object;
assume x in XX;
then consider y be object such that
A18: y in dom f & x=f.y by A7,FUNCT_1:def 3;
reconsider y as Nat by A18;
A19: y+1 in dom g & x=f.y by A13,A18,NAT_LAT:def 6;
g.(y+1)=f.y
proof
consider xx be Nat such that
A20: xx+1=y+1 & g.(y+1)=f.xx by A13,A19;
thus thesis by A20;
end;
hence thesis by A19,FUNCT_1:def 3;
end;
hence thesis by A15;
end;
g is Function of NATPLUS,S by B0,A13,A14,FUNCT_2:def 1,RELSET_1:4;
hence thesis by A14;
end;
ex P be countable Subset of S
st P is a_partition of X
proof
consider g be Function of NATPLUS,S such that
A21: rng g=XX by A6;
consider P be countable Subset of S such that
A22: P is a_partition of Union g &
for n be NatPlus holds
Union (g|Seg n)=
union{s where s is Element of S:s in P & s c= Union (g|Seg n)}
by Thm4;
Union g c= X
proof
let y be object;
assume y in Union g;
then consider z be set such that
A24: y in z & z in rng g by TARSKI:def 4;
y in union S by A24,TARSKI:def 4;
hence thesis;
end;
then X=Union g by A1,A21,SETFAM_1:def 11;
hence thesis by A22;
end;
hence thesis;
end;
end;
end;
definition
let X be set;
mode semiring_of_sets of X is cap-finite-partition-closed
diff-c=-finite-partition-closed with_empty_element Subset-Family of X;
end;
LemPO:
for S be Subset of X, A be Element of S
holds union (PARTITIONS(A)/\Fin S) is with_non-empty_elements
proof
let S be Subset of X, A be Element of S;
assume not union (PARTITIONS(A)/\Fin S) is with_non-empty_elements;
then {} in union (PARTITIONS(A)/\Fin S) by SETFAM_1:def 8;
then consider x be set such that
A2: {} in x and
A3: x in PARTITIONS(A)/\Fin S by TARSKI:def 4;
x in PARTITIONS(A) & x in Fin S by A3,XBOOLE_0:def 4;
then x is a_partition of A by PARTIT1:def 3;
hence thesis by A2;
end;
theorem ThmVAL0:
for S be cap-finite-partition-closed Subset-Family of X, A be Element of S
holds {x where x is Element of S: x in union (PARTITIONS(A)/\Fin S)}
is
cap-finite-partition-closed Subset-Family of A
proof
let S be cap-finite-partition-closed Subset-Family of X;
let A be Element of S;
set B={x where x is Element of S:x in union (PARTITIONS(A)/\Fin S)};
per cases;
suppose
H0: A is empty;
T1: B c= {}
proof
let t be object;
assume t in B;
then consider t0 be Element of S such that
t=t0 and
ZE2: t0 in union (PARTITIONS(A)/\Fin S);
consider u0 be set such that
ZE3: t0 in u0 and
ZE4: u0 in PARTITIONS(A)/\Fin S by ZE2,TARSKI:def 4;
u0 in {{}} by A4bis,ZE4,XBOOLE_0:def 4,H0;
hence thesis by ZE3,TARSKI:def 1;
end;
{} is Subset-Family of {} by XBOOLE_1:2;
then reconsider B as Subset-Family of {} by T1;
for a,b be Element of B st a/\b is non empty
ex P be finite Subset of B st P is a_partition of a/\b
proof
let a,b be Element of B;
assume
VA: a/\b is non empty;
a={} & b={} by T1,SUBSET_1:def 1;
hence thesis by VA;
end;
hence thesis by H0,Defcap;
end;
suppose
H1: A is non empty;
AA: B c= bool A
proof
let x be object;
assume x in B;
then consider x0 be Element of S such that
B1: x=x0 and
B2: x0 in union (PARTITIONS(A)/\Fin S);
consider x1 be set such that
B3: x0 in x1 and
B4: x1 in PARTITIONS(A)/\Fin S by B2,TARSKI:def 4;
x1 in PARTITIONS(A) by B4,XBOOLE_0:def 4;
then x1 is a_partition of A by PARTIT1:def 3;
hence x in bool A by B1,B3;
end;
per cases;
suppose
U0: B is empty;
then reconsider B as Subset-Family of A by XBOOLE_1:2;
B is cap-finite-partition-closed by U0;
hence thesis;
end;
suppose B is non empty;
then reconsider B as non empty set;
for x,y be Element of B st x/\y is non empty
ex P be finite Subset of B st P is a_partition of x/\y
proof
let x,y be Element of B;
assume
V1: x/\y is non empty;
x in B;
then consider x0 be Element of S such that
A1: x=x0 and
A2: x0 in union (PARTITIONS(A)/\Fin S);
consider x1 be set such that
C1: x0 in x1 and
C2: x1 in PARTITIONS(A)/\Fin S by A2,TARSKI:def 4;
y in B;
then consider y0 be Element of S such that
A3: y=y0 and
A4: y0 in union (PARTITIONS(A)/\Fin S);
consider y1 be set such that
C3: y0 in y1 and
C4: y1 in PARTITIONS(A)/\Fin S by A4,TARSKI:def 4;
C4a: x1 in PARTITIONS(A) & x1 in Fin S & y1 in PARTITIONS(A) &
y1 in Fin S by C2,C4,XBOOLE_0:def 4;
then
C5: x1 is a_partition of A & x1 is finite Subset of S &
y1 is a_partition of A & y1 is finite Subset of S
by PARTIT1:def 3,FINSUB_1:def 5;
reconsider A as non empty set by H1;
reconsider x1 as a_partition of A
by C4a,PARTIT1:def 3;
reconsider y1 as a_partition of A
by C4a,PARTIT1:def 3;
consider P be a_partition of A such that
D1: P is finite Subset of S and
D2: P '<' x1 '/\' y1 by C5,ThmJ1;
consider P1 be finite Subset of S such that
F1: P1 is a_partition of x/\y by A1,A3,V1,Defcap;
P1 is finite Subset of B
proof
P1 c= B
proof
let d be object;
assume
UP: d in P1;
UJ: x0 in x1 & x1 is a_partition of A by C1;
KK2: x/\y c= A by A1,UJ,XBOOLE_1:108;
set PP={p where p is Element of P: p misses x/\y}\/P1;
GH2: PP is finite Subset of S
proof
GHAA: PP c= P\/P1
proof
let z be object;
assume z in PP;
then
UU: z in {p where p is Element of P: p misses x/\y}
or z in P1 by XBOOLE_0:def 3;
{p where p is Element of P: p misses x/\y} c= P
proof
let a be object;
assume a in {p where p is Element of P: p misses x/\y};
then consider p be Element of P such that
UU2: a=p and
p misses x/\y;
thus thesis by UU2;
end;
hence thesis by UU,XBOOLE_0:def 3;
end;
PP c= S
proof
let a be object;
assume a in PP;
then
GHAA: a in {p where p is Element of P: p misses x/\y} or a in P1
by XBOOLE_0:def 3;
{p where p is Element of P: p misses x/\y} c= S
proof
let b be object;
assume b in {p where p is Element of P:
p misses x/\y};
then consider p be Element of P such that
GHC: b=p and
p misses x/\y;
b in P by GHC;
hence thesis by D1;
end;
hence thesis by GHAA;
end;
hence thesis by GHAA,D1;
end;
PP is a_partition of A
proof
FD1: PP c= bool A
proof
let z be object;
assume z in PP;
then
O1: z in {p where p is Element of P: p misses x/\y}
or z in P1 by XBOOLE_0:def 3;
O2: {p where p is Element of P: p misses x/\y} c= bool A
proof
let t be object;
assume t in
{p where p is Element of P: p misses x/\y};
then consider t0 be Element of P such that
O3: t=t0 & t0 misses x/\y;
thus thesis by O3;
end;
P1 c= bool A
proof
let t be object;
assume
X1: t in P1;
bool (x/\y) c= bool A
proof
X3: x in B;
x/\y c= x by XBOOLE_1:17;
then x/\y c= A by AA,X3,XBOOLE_1:1;
hence thesis by ZFMISC_1:67;
end;
then P1 c= bool A by F1,XBOOLE_1:1;
hence thesis by X1;
end;
hence thesis by O1,O2;
end;
FD2: union PP = A
proof
thus union PP c= A
proof
let a be object;
assume
S0: a in union PP;
S1: union PP=
union {p where p is Element of P: p misses x/\y} \/
union P1
by ZFMISC_1:78;
S5: union P1 c= A by KK2,F1,EQREL_1:def 4;
union {p where p is Element of P: p misses x/\y} c= A
proof
S5a: {p where p is Element of P: p misses x/\y} c= P
proof
let a be object;
assume a in
{p where p is Element of P: p misses x/\y};
then consider b be Element of P such that
S6: a=b and
b misses x/\y;
thus thesis by S6;
end;
union P = A by EQREL_1:def 4;
hence thesis by S5a,ZFMISC_1:77;
end;
then union {p where p is Element of P:
p misses x/\y} \/ union P1 c= A
by S5,XBOOLE_1:8;
hence thesis by S0,S1;
end;
let a be object;
assume
PO0: a in A;
per cases;
suppose
PO1: a in x/\y;
a in union P1 by PO1,F1,EQREL_1:def 4;
then a in union P1 \/ union
{p where p is Element of P: p misses x/\y}
by XBOOLE_1:7,TARSKI:def 3;
hence thesis by ZFMISC_1:78;
end;
suppose
I0: not a in x/\y;
union P = A by EQREL_1:def 4;
then consider b be set such that
I1: a in b and
I2: b in P by PO0,TARSKI:def 4;
consider u be set such that
W1: u in x1 '/\' y1 and
W2: b c= u by I2,D2,SETFAM_1:def 2;
consider xx1,yy1 be set such that
W3: xx1 in x1 & yy1 in y1 and
W4: u=xx1/\yy1 by W1,SETFAM_1:def 5;
W5W: xx1/\yy1 misses x/\y
proof
assume not xx1/\yy1 misses x/\y;
then consider i be object such that
W5A: i in (xx1/\yy1)/\(x/\y) by XBOOLE_0:def 1;
i in xx1/\yy1 & i in x/\y by W5A,XBOOLE_0:def 4;
then i in xx1 & i in yy1 & i in x & i in y
by XBOOLE_0:def 4;
then i in xx1/\x & i in yy1/\y by XBOOLE_0:def 4;
then xx1=x & yy1=y
by A1,C1,A3,C3,W3,EQREL_1:def 4,XBOOLE_0:def 7;
hence thesis by I0,I1,W2,W4;
end;
b misses x/\y
proof
assume not b misses x/\y;
then consider b0 be object such that
W6: b0 in b/\(x/\y) by XBOOLE_0:def 1;
b0 in b & b0 in x/\y by W6,XBOOLE_0:def 4;
hence thesis by W5W,W2,W4,XBOOLE_0:def 4;
end;
then b in {p where p is Element of P:
p misses x/\y} by I2;
then a in union {p where p is Element of P:
p misses x/\y} by I1,TARSKI:def 4;
then a in union {p where p is Element of P:
p misses x/\y} \/ union P1
by XBOOLE_1:7,TARSKI:def 3;
hence thesis by ZFMISC_1:78;
end;
end;
for a be Subset of A st a in PP holds a <> {} &
for b be Subset of A st b in PP holds a=b or a misses b
proof
let a be Subset of A;
assume a in PP;
then
DF1: a in {p where p is Element of P: p misses x/\y} or
a in P1 by XBOOLE_0:def 3;
DF1A: {p where p is Element of P: p misses x/\y} c= P
proof
let a be object;
assume a in {p where p is Element of P: p misses x/\y};
then consider p be Element of P such that
UU2: a=p and
p misses x/\y;
thus thesis by UU2;
end;
for b be Subset of A st b in PP holds a=b or a misses b
proof
let b be Subset of A;
assume b in PP;
then
DF5: b in {p where p is Element of P:
p misses x/\y} or
b in P1 by XBOOLE_0:def 3;
DF7A: a in {p where p is Element of P:
p misses x/\y} &
b in P1 implies a misses b
proof
assume that
QW1: a in {p where p is Element of P:
p misses x/\y} and
QW2: b in P1;
consider a0 be Element of P such that
QW3: a=a0 & a0 misses x/\y by QW1;
thus thesis by QW3,QW2,F1,XBOOLE_1:63;
end;
b in {p where p is Element of P:
p misses x/\y} &
a in P1 implies a misses b
proof
assume that
QW1: b in {p where p is Element of P:
p misses x/\y} and
QW2: a in P1;
consider b0 be Element of P such that
QW3: b=b0 & b0 misses x/\y by QW1;
thus thesis by QW3,QW2,F1,XBOOLE_1:63;
end;
hence thesis by DF1,DF5,DF1A,DF7A,F1,EQREL_1:def 4;
end;
hence thesis by F1,DF1A,DF1;
end;
hence thesis by FD1,FD2,EQREL_1:def 4;
end;
then d in PP & PP in PARTITIONS(A) & PP in Fin S
by UP,XBOOLE_0:def 3,GH2,PARTIT1:def 3,FINSUB_1:def 5;
then d in PP & PP in PARTITIONS(A) /\ Fin S
by XBOOLE_0:def 4;
then d in union (PARTITIONS(A)/\Fin S) by TARSKI:def 4;
hence thesis by UP;
end;
hence thesis;
end;
hence thesis by F1;
end;
hence thesis by AA,Defcap;
end;
end;
end;
theorem ThmVAL2:
for S be cap-finite-partition-closed Subset-Family of X,
A be Element of S
holds {x where x is Element of S: x in union (PARTITIONS(A)/\Fin S)} is
diff-c=-finite-partition-closed Subset-Family of A
proof
let S be cap-finite-partition-closed Subset-Family of X,
A be Element of S;
set B={x where x is Element of S:x in union (PARTITIONS(A)/\Fin S)};
per cases;
suppose
H0: A is empty;
T1: B c= {}
proof
let t be object;
assume t in B;
then consider t0 be Element of S such that
t=t0 and
ZE2: t0 in union (PARTITIONS(A)/\Fin S);
consider u0 be set such that
ZE3: t0 in u0 and
ZE4: u0 in PARTITIONS(A)/\Fin S by ZE2,TARSKI:def 4;
u0 in PARTITIONS(A) by ZE4,XBOOLE_0:def 4;
hence thesis by H0,ZE3,A4bis,TARSKI:def 1;
end;
{} is Subset-Family of {} by XBOOLE_1:2;
then reconsider B as Subset-Family of {} by T1;
for a,b be Element of B st a\b is non empty
ex P be finite Subset of B st P is a_partition of a\b
by T1,SUBSET_1:def 1;
then B is diff-finite-partition-closed;
hence thesis by H0;
end;
suppose
H1: A is non empty;
AA: B c= bool A
proof
let x be object;
assume x in B;
then consider x0 be Element of S such that
B1: x=x0 and
B2: x0 in union (PARTITIONS(A)/\Fin S);
consider x1 be set such that
B3: x0 in x1 and
B4: x1 in PARTITIONS(A)/\Fin S by B2,TARSKI:def 4;
x1 in PARTITIONS(A) & x1 in Fin S by B4,XBOOLE_0:def 4;
then x1 is a_partition of A by PARTIT1:def 3;
hence x in bool A by B1,B3;
end;
per cases;
suppose
U0: B is empty;
then reconsider B as Subset-Family of A by XBOOLE_1:2;
for S1,S2 be Element of B st S1\S2 is non empty holds
ex P be finite Subset of B st P is a_partition of S1\S2
by U0,SUBSET_1:def 1;
then B is diff-finite-partition-closed;
hence thesis;
end;
suppose B is non empty;
then reconsider B as non empty set;
for x,y be Element of B st y c= x
ex P be finite Subset of B st P is a_partition of x\y
proof
let x,y be Element of B;
assume y c= x;
x in B;
then consider x0 be Element of S such that
A1: x=x0 and
A2: x0 in union (PARTITIONS(A)/\Fin S);
consider x1 be set such that
C1: x0 in x1 and
C2: x1 in PARTITIONS(A)/\Fin S by A2,TARSKI:def 4;
y in B;
then consider y0 be Element of S such that
A3: y=y0 and
A4: y0 in union (PARTITIONS(A)/\Fin S);
consider y1 be set such that
C3: y0 in y1 and
C4: y1 in PARTITIONS(A)/\Fin S by A4,TARSKI:def 4;
C4A: x1 in PARTITIONS(A) & x1 in Fin S & y1 in PARTITIONS(A) &
y1 in Fin S by C2,C4,XBOOLE_0:def 4;
then
C5: x1 is a_partition of A & x1 is finite Subset of S &
y1 is a_partition of A & y1 is finite Subset of S
by PARTIT1:def 3,FINSUB_1:def 5;
reconsider A as non empty set by H1;
reconsider x1,y1 as a_partition of A by C4A,PARTIT1:def 3;
consider P be a_partition of A such that
D1: P is finite Subset of S and
D2: P '<' x1 '/\' y1 by C5,ThmJ1;
set P1={p where p is Element of P:p is Subset of x & p misses y};
T1: P1 is finite Subset of B
proof
T1A: P1 is finite
proof
P1 c= P
proof
let a be object;
assume a in P1;
then ex p be Element of P st
a=p & p is Subset of x & p misses y;
hence thesis;
end;
hence thesis by D1;
end;
P1 c= B
proof
let a be object;
assume
a in P1;
then consider p be Element of P such that
EZ2: a=p and
p is Subset of x and
p misses y;
a in P & P in PARTITIONS(A) & P in Fin S
by EZ2,D1,FINSUB_1:def 5,PARTIT1:def 3;
then a in P & P in PARTITIONS(A)/\Fin S by XBOOLE_0:def 4;
then
EZ6: a in union (PARTITIONS(A)/\Fin S) by TARSKI:def 4;
a in P by EZ2;
hence thesis by D1,EZ6;
end;
hence thesis by T1A;
end;
P1 is a_partition of x\y
proof
Y1: P1 c= bool (x\y)
proof
let a be object;
assume a in P1;
then consider p be Element of P such that
EZ7: a=p and
EZ8: p is Subset of x and
EZ9: p misses y;
reconsider a as set by TARSKI:1;
a c= x\y by EZ7,EZ8,EZ9,XBOOLE_1:86;
hence thesis;
end;
Y2: union P1=x\y
proof
thus union P1 c= x\y
proof
let a be object;
assume a in union P1;
then consider b be set such that
EZ11: a in b and
EZ12: b in P1 by TARSKI:def 4;
consider p be Element of P such that
EZ13: b=p and
EZ14: p is Subset of x and
EZ15: p misses y by EZ12;
b c= x\y by EZ13,EZ14,EZ15,XBOOLE_1:86;
hence thesis by EZ11;
end;
let a be object;
assume
AS0: a in x\y;
then
U0: a in x;
U00: x in x1 & x1 is a_partition of A by A1,C1;
U1: a in A by U0,U00;
a in union P by U1,EQREL_1:def 4;
then consider b be set such that
U2: a in b and
U3: b in P by TARSKI:def 4;
consider u be set such that
U4: u in x1 '/\' y1 and
U5: b c= u by U3,D2,SETFAM_1:def 2;
consider xx1,yy1 be set such that
W3: xx1 in x1 & yy1 in y1 and
W4: u=xx1/\yy1 by U4,SETFAM_1:def 5;
UU1: b is Subset of x
proof
LI1A: b c= xx1/\yy1 & xx1/\yy1 c= xx1 by U5,W4,XBOOLE_1:17;
then
LI1: b c= xx1 by XBOOLE_1:1;
xx1=x
proof
assume not xx1=x;
then b misses x
by A1,C1,W3,LI1,EQREL_1:def 4,XBOOLE_1:63;
hence thesis by AS0,U2,XBOOLE_0:def 4;
end;
hence thesis by LI1A,XBOOLE_1:1;
end;
b misses y
proof
assume not b misses y;
then consider z be object such that
WA1: z in b/\y by XBOOLE_0:def 1;
consider v be set such that
K1: v in x1 '/\' y1 and
K2: b c= v by U3,D2,SETFAM_1:def 2;
consider xx1,yy1 be set such that
W3: xx1 in x1 & yy1 in y1 and
W4: v=xx1/\yy1 by K1,SETFAM_1:def 5;
LEM: not xx1/\yy1 = x/\y
proof
assume xx1/\yy1=x/\y;
then a in y by U2,W4,K2,XBOOLE_0:def 4;
hence thesis by AS0,XBOOLE_0:def 5;
end;
z in b/\y & b/\y c= xx1/\yy1/\y by WA1,K2,W4,XBOOLE_1:26;
then z in xx1/\yy1 & z in y by XBOOLE_0:def 4;
then z in xx1 & z in yy1 & z in y by XBOOLE_0:def 4;
then
AS2: z in yy1/\y by XBOOLE_0:def 4;
AS2A: yy1=y by A3,C3,W3,EQREL_1:def 4,AS2,XBOOLE_0:def 7;
a in xx1 & a in x
by U2,K2,W4,AS0,XBOOLE_0:def 4;
then a in xx1/\x by XBOOLE_0:def 4;
hence thesis
by A1,C1,W3,EQREL_1:def 4,LEM,AS2A,XBOOLE_0:def 7;
end;
then b in P1 by UU1,U3;
hence thesis by U2,TARSKI:def 4;
end;
for a be Subset of x\y st a in P1 holds a<>{} &
for b be Subset of x\y st b in P1 holds a=b or a misses b
proof
let a be Subset of x\y;
assume a in P1;
then
CC: ex a0 be Element of P st
a=a0 & a0 is Subset of x & a0 misses y;
hence a<>{};
for b be Subset of x\y st b in P1 holds a=b or a misses b
proof
let b be Subset of x\y;
assume b in P1;
then ex b0 be Element of P st
b=b0 & b0 is Subset of x & b0 misses y;
hence thesis by CC,EQREL_1:def 4;
end;
hence thesis;
end;
hence thesis by Y1,Y2,EQREL_1:def 4;
end;
hence thesis by T1;
end;
hence thesis by AA,Defdiff2;
end;
end;
end;
theorem Thm99:
for S be cap-finite-partition-closed Subset-Family of X,
A be Element of S
holds union (PARTITIONS(A)/\Fin S) is cap-finite-partition-closed
diff-finite-partition-closed Subset-Family of A &
union (PARTITIONS(A)/\Fin S) is with_non-empty_elements
proof
let S be cap-finite-partition-closed Subset-Family of X,
A be Element of S;
A1: union (PARTITIONS(A)/\Fin S)=
{x where x is Element of S: x in union (PARTITIONS(A)/\Fin S)} by ThmVAL1;
then
A2: union (PARTITIONS(A)/\Fin S) is
cap-finite-partition-closed Subset-Family of A by ThmVAL0;
union (PARTITIONS(A)/\Fin S) is diff-c=-finite-partition-closed
Subset-Family of A by A1,ThmVAL2;
hence thesis by A2,LemPO;
end;
theorem
for S be cap-finite-partition-closed Subset-Family of X,
A be Element of S
holds {{}}\/union (PARTITIONS(A)/\Fin S) is semiring_of_sets of A
proof
let S be cap-finite-partition-closed Subset-Family of X,
A be Element of S;
set A1=union (PARTITIONS(A)/\Fin S);
set B=union (PARTITIONS(A)/\Fin S)\/{{}};
A1: A1 is cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of A by Thm99;
A2: {{}} c= B & {} in {{}} by XBOOLE_1:7,TARSKI:def 1;
B c= bool A
proof
let x be object;
assume x in B;
then x in A1 or x in {{}} by XBOOLE_0:def 3;
then
A3: x in A1 or x = {} by TARSKI:def 1;
{} c= A by XBOOLE_1:2;
hence thesis by A1,A3;
end;
then reconsider B as Subset-Family of A;
A4: B is cap-finite-partition-closed
proof
let S1,S2 be Element of B such that
F1: S1/\S2 is non empty;
reconsider A1 as Subset-Family of A by Thm99;
(S1 in A1 or S1 in {{}}) &
(S2 in A1 or S2 in {{}}) by XBOOLE_0:def 3;
then (S1 in A1 or S1 = {}) &
(S2 in A1 or S2 = {}) by TARSKI:def 1;
then S1 is Element of A1 &
S2 is Element of A1 & S1/\S2 is non empty &
A1 is cap-finite-partition-closed by F1,Thm99;
then consider P be finite Subset of A1 such that
SOL: P is a_partition of S1/\S2;
reconsider P as finite Subset of B by XBOOLE_1:10;
P is finite Subset of B & P is a_partition of S1/\S2 by SOL;
hence thesis;
end;
B is diff-finite-partition-closed
proof
let S1,S2 be Element of B such that
F1: S1\S2 is non empty;
reconsider A1 as Subset-Family of A by Thm99;
F2aa: (S1 in A1 or S1 in {{}}) &
(S2 in A1 or S2 in {{}}) by XBOOLE_0:def 3;
V1: S2={} implies ex P be finite Subset of B st
P is a_partition of S1\S2
proof
assume
D0: S2={};
D3: {S1} c= B
proof
let x be object;
assume x in {S1};
then x=S1 by TARSKI:def 1;
hence thesis;
end;
{S1} is a_partition of S1 by F1,EQREL_1:39;
hence thesis by D0,D3;
end;
S2 in A1 implies ex P be finite Subset of B st
P is a_partition of S1\S2
proof
assume S2 in A1;
then S1 is Element of A1 &
S2 is Element of A1 & S1\S2 is non empty &
A1 is diff-finite-partition-closed by Thm99,F1,F2aa,TARSKI:def 1;
then
consider P be finite Subset of A1 such that
SOL: P is a_partition of S1\S2;
reconsider P as finite Subset of B by XBOOLE_1:10;
P is finite Subset of B & P is a_partition of S1\S2 by SOL;
hence thesis;
end;
hence thesis by V1,F2aa,TARSKI:def 1;
end;
hence thesis by A2,A4;
end;
theorem thmCup:
for S be cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of X holds
{union x where x is finite Subset of S:x is mutually-disjoint}
is cup-closed
proof
let S be cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of X;
set Y={union x where x is finite Subset of S:x is mutually-disjoint};
let a,b be set;
assume
A: a in Y & b in Y;
then consider a0 be finite Subset of S such that
B: a = union a0 & a0 is mutually-disjoint;
consider b0 be finite Subset of S such that
C: b = union b0 & b0 is mutually-disjoint by A;
consider SM be FinSequence such that
F1: rng SM=a0\/b0 by FINSEQ_1:52;
consider P be finite Subset of S such that
VU: P is a_partition of Union SM and
for Y be Element of (rng SM) holds
Y = union {s where s is Element of S: s in P & s c= Y} by F1,Thm87;
Union SM=union a0 \/ union b0 by F1,ZFMISC_1:78;
then
VB: union P = a\/b by B,C,VU,EQREL_1:def 4;
for x,y be set st x in P & y in P & x<>y holds x misses y
by VU,EQREL_1:def 4;
then P is mutually-disjoint by TAXONOM2:def 5;
hence thesis by VB;
end;
theorem
for S be cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of X holds
{union x where x is finite Subset of S:x is mutually-disjoint} is
Ring_of_sets
proof
let S be cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of X;
{union x where x is finite Subset of S:x is mutually-disjoint}
is cap-closed cup-closed by Thm86,thmCup;
hence thesis by thmIL;
end;