:: Semiring of Sets :: by Roland Coghetto :: :: Received March 31, 2014 :: Copyright (c) 2014-2017 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, TEX_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={} by EQREL_1:32; 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=1 & yyy= 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;