:: Semiring of Sets: Examples
:: by Roland Coghetto
::
:: Received March 31, 2014
:: Copyright (c) 2014-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CARD_1, CARD_3, EQREL_1, FINSET_1, FINSUB_1, FUNCT_1, MCART_1,
NUMBERS, PROB_1, RELAT_1, SETFAM_1, SIMPLEX0, SRINGS_1, SUBSET_1, TARSKI,
XBOOLE_0, ZFMISC_1, ARYTM_1, ARYTM_3, COMPLEX1, MEASURE5, ORDINAL1,
REAL_1, SUPINF_1, XREAL_0, XXREAL_0, XXREAL_1, SRINGS_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, SETFAM_1, FINSET_1,
CARD_1, CARD_3, RELAT_1, FINSUB_1, PROB_1, FUNCT_1, SIMPLEX0, XTUPLE_0,
WELLORD2, MCART_1, SRINGS_1, ORDINAL1, COMPLEX1, NUMBERS, XXREAL_0,
XREAL_0, XXREAL_1, XXREAL_3, MEASURE5, RCOMP_1, SUPINF_1, ENUMSET1;
constructors SRINGS_1, TOPGEN_4, COMPLEX1, RELSET_1, SIMPLEX0, FINSUB_1,
SUPINF_1, RCOMP_1, MEASURE5, TOPGEN_3, ARYTM_2, ENUMSET1, PARTIT1;
registrations CARD_1, CARD_3, EQREL_1, FINSET_1, FINSUB_1, MEASURE1, PROB_1,
SIMPLEX0, SRINGS_1, SUBSET_1, XBOOLE_0, XTUPLE_0, ZFMISC_1, SETFAM_1,
MEMBERED, NAT_1, RELSET_1, XREAL_0, XXREAL_1, XXREAL_3;
requirements BOOLE, SUBSET, ARITHM, NUMERALS, REAL;
definitions FINSUB_1, FUNCT_1, SRINGS_1, TARSKI, XBOOLE_0;
equalities CARD_3, RCOMP_1, XXREAL_0, XXREAL_1;
expansions TARSKI, XBOOLE_0;
theorems CARD_1, CARD_3, CARD_4, DILWORTH, EQREL_1, FINSUB_1, LATTICE5,
PARTIT1, PROB_1, PUA2MSS1, SETFAM_1, SRINGS_1, SUBSET_1, TARSKI,
XBOOLE_0, XBOOLE_1, XTUPLE_0, YELLOW_8, ZFMISC_1, ABSVALUE, CARD_5,
FUNCT_1, FUNCT_2, MEASURE5, MESFUNC1, NUMBERS, ORDINAL1, RELSET_1,
TOPGEN_4, XREAL_0, XREAL_1, XXREAL_0, XXREAL_1, ENUMSET1;
schemes FUNCT_1, XBOOLE_0;
begin :: Preliminaries
reserve X for set;
reserve S for Subset-Family of X;
theorem
for X1,X2 be set, S1 be Subset-Family of X1, S2 be Subset-Family of X2
holds {[:a,b:] where a is Element of S1, b is Element of S2:a in S1 &
b in S2} = {s where s is Subset of [:X1,X2:] : ex a,b be set st a in S1 &
b in S2 & s=[:a,b:]}
proof
let X1,X2 be set;
let S1 be Subset-Family of X1;
let S2 be Subset-Family of X2;
thus {[:a,b:] where a is Element of S1, b is Element of S2:a in S1 &
b in S2} c= {s where s is Subset of [:X1,X2:] : ex a,b be set st
a in S1 & b in S2 & s=[:a,b:]}
proof
let x be object;
assume x in {[:a,b:] where a is Element of S1, b is Element of
S2: a in S1 & b in S2};
then consider a be Element of S1, b be Element of S2 such that
A1: x=[:a,b:] & a in S1 & b in S2;
[:a,b:] c= [:X1,X2:] by A1,ZFMISC_1:96;
hence thesis by A1;
end;
let x be object;
assume x in {s where s is Subset of [:X1,X2:] : ex a,b be set st
a in S1 & b in S2 & s=[:a,b:]};
then ex s0 be Subset of [:X1,X2:] st x=s0 & ex a0,b0 be set st
a0 in S1 & b0 in S2 & s0=[:a0,b0:];
hence thesis;
end;
theorem
for X1,X2 be set, S1 be non empty Subset-Family of X1,
S2 be non empty Subset-Family of X2 holds
{s where s is Subset of [:X1,X2:]: ex x1,x2 be set st x1 in S1 & x2 in S2 &
s=[:x1,x2:]} =
the set of all [:x1,x2:] where x1 is Element of S1, x2 is Element of S2
proof
let X1,X2 be set;
let S1 be non empty Subset-Family of X1;
let S2 be non empty Subset-Family of X2;
A1: for x be object st x in {s where s is Subset of [:X1,X2:]: ex
x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]} holds x in
the set of all [:x1,x2:] where x1 is Element of S1, x2 is Element of S2
proof
let x be object;
assume x in {s where s is Subset of [:X1,X2:]: ex
x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]};
then ex s be Subset of [:X1,X2:] st
x=s & ex x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:];
hence thesis;
end;
for x be object st x in the set of all [:x1,x2:] where x1 is Element of S1,
x2 is Element of S2 holds
x in {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st
x1 in S1 & x2 in S2 & s=[:x1,x2:]}
proof
let x be object;
assume x in the set of all [:x1,x2:] where x1 is Element of S1,
x2 is Element of S2;
then ex x1 be Element of S1, x2 be Element of S2 st x=[:x1,x2:];
hence thesis;
end;
hence thesis by A1,TARSKI:2;
end;
theorem
for X1,X2 be set,S1 be Subset-Family of X1,S2 be Subset-Family of X2 st
S1 is cap-closed & S2 is cap-closed holds
{s where s is Subset of [:X1,X2:]: ex x1,x2 be set st x1 in S1 & x2 in S2 &
s=[:x1,x2:]} is cap-closed
proof
let X1,X2 be set, S1 be Subset-Family of X1,
S2 be Subset-Family of X2;
assume
A1: S1 is cap-closed;
assume
A2: S2 is cap-closed;
set Y= {s where s is Subset of [:X1,X2:]: ex
x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]};
Y is cap-closed
proof
let W1,W2 be set;
assume
A3: W1 in Y;
assume
A4: W2 in Y;
consider s1 be Subset of [:X1,X2:] such that
A5: W1=s1 & ex xs1,xs2 be set st xs1 in S1 & xs2 in S2 &
s1=[:xs1,xs2:] by A3;
consider xs1,xs2 be set such that
A6: xs1 in S1 & xs2 in S2 & s1=[:xs1,xs2:] by A5;
consider s2 be Subset of [:X1,X2:] such that
A7: W2=s2 & ex ys1,ys2 be set st ys1 in S1 & ys2 in S2 &
s2=[:ys1,ys2:] by A4;
consider ys1,ys2 be set such that
A8: ys1 in S1 & ys2 in S2 & s2=[:ys1,ys2:] by A7;
A9: [:xs1,xs2:]/\[:ys1,ys2:]=[:xs1/\ys1,xs2/\ys2:] by ZFMISC_1:100;
A10: xs1/\ys1 in S1 & xs2/\ys2 in S2 by A6,A8,A1,A2,FINSUB_1:def 2;
s1/\s2 in Y by A6,A8,A9,A10;
hence thesis by A5,A7;
end;
hence thesis;
end;
Lem3:
for X1,X2 be set,
S1 be Subset-Family of X1,
S2 be Subset-Family of X2 holds
{s where s is Subset of [:X1,X2:]: ex s1,s2 be set st s1 in S1 & s2 in S2 &
s=[:s1,s2:]} is Subset-Family of [:X1,X2:]
proof
let X1,X2 be set;
let S1 be Subset-Family of X1;
let S2 be Subset-Family of X2;
set S = {s where s is Subset of [:X1,X2:]:
ex s1,s2 be set st s1 in S1 & s2 in S2 & s=[:s1,s2:]};
S c= bool [:X1,X2:]
proof
let x be object;
assume x in S;
then consider s0 be Subset of [:X1,X2:] such that
A1: x=s0 & ex s1,s2 be set st s1 in S1 & s2 in S2 & s0=[:s1,s2:];
thus thesis by A1;
end;
hence thesis;
end;
Lem4:
for X1,X2,Y1,Y2 be set holds
[:X1,X2:]\[:Y1,Y2:]= [:X1\Y1,X2:]\/[:X1/\Y1,X2\Y2:] &
[:X1\Y1,X2:] misses [:X1/\Y1,X2\Y2:]
proof
let X1,X2,Y1,Y2 be set;
A2: [:X1\Y1,X2:]\/[:X1,X2\Y2:] c= [:X1\Y1,X2:]\/[:X1/\Y1,X2\Y2:]
proof
let x be object;
assume
A3: x in [:X1\Y1,X2:]\/[:X1,X2\Y2:];
now
per cases by A3,XBOOLE_0:def 3;
suppose x in [:X1\Y1,X2:];
hence thesis by XBOOLE_0:def 3;
end;
suppose x in [:X1,X2\Y2:];
then consider x1,x2 be object such that
A4: x1 in X1 and
A5: x2 in X2\Y2 and
A6: x=[x1,x2] by ZFMISC_1:def 2;
(x1 in X1 & not x1 in Y1) or
(x1 in X1 & x1 in Y1) by A4;
then (x1 in (X1\Y1) & x2 in X2) or (x1 in (X1/\Y1)&
x2 in X2\Y2) by A5,XBOOLE_0:def 4,def 5;
then x in [:X1\Y1,X2:] or x in [:X1/\Y1,X2\Y2:]
by A6,ZFMISC_1:def 2;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
A7: [:X1\Y1,X2:]\/[:X1/\Y1,X2\Y2:] c= [:X1\Y1,X2:]\/[:X1,X2\Y2:]
proof
let x be object;
assume
A8: x in [:X1\Y1,X2:]\/[:X1/\Y1,X2\Y2:];
now
per cases by A8,XBOOLE_0:def 3;
suppose x in [:X1\Y1,X2:];
hence thesis by XBOOLE_0:def 3;
end;
suppose x in [:X1/\Y1,X2\Y2:];
then consider x1,x2 be object such that
A9: x1 in X1/\Y1 and
A10: x2 in X2\Y2 and
A11: x=[x1,x2] by ZFMISC_1:def 2;
x1 in X1 & x2 in X2\Y2 & x=[x1,x2]
by A9,A10,A11,XBOOLE_0:def 4;
then x in [:X1,X2\Y2:] by ZFMISC_1:def 2;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
[:X1\Y1,X2:] misses [:X1/\Y1,X2\Y2:]
proof
now
let x be object;
assume x in [:X1\Y1,X2:] /\ [:X1/\Y1,X2\Y2:];
then
A12: x in [:X1\Y1,X2:] & x in [:X1/\Y1,X2\Y2:] by XBOOLE_0:def 4;
then consider a1,a2 be object such that
A13: a1 in X1\Y1 & a2 in X2 & x=[a1,a2] by ZFMISC_1:def 2;
consider a3,a4 be object such that
A14: a3 in X1/\Y1 & a4 in X2\Y2 & x=[a3,a4] by ZFMISC_1:def 2,A12;
a1=a3 & a2=a4 by XTUPLE_0:1,A13,A14;
then a1 in X1 & not a1 in Y1 & a1 in Y1 by A13,A14,XBOOLE_0:def 4,
XBOOLE_0:def 5;
hence contradiction;
end;
then [:X1\Y1,X2:] /\ [:X1/\Y1,X2\Y2:] is empty;
hence thesis;
end;
hence thesis by A2,A7,ZFMISC_1:103;
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 be set;
cluster -> cap-finite-partition-closed diff-c=-finite-partition-closed
with_countable_Cover with_empty_element for SigmaField of X;
coherence
proof
let SF be SigmaField of X;
set U={X};
A1: U is Subset-Family of X by ZFMISC_1:68;
A2: union U=X;
X is Element of SF by PROB_1:5;
then U is Subset of SF by SUBSET_1:33;
hence thesis by A1,SETFAM_1:45,def 8,A2,SRINGS_1:def 4,PROB_1:4;
end;
end;
begin :: Ordinary Examples of Semirings of Sets
theorem
for F being SigmaField of X holds F is semiring_of_sets of X;
registration
let X be set;
cluster bool X -> cap-finite-partition-closed diff-c=-finite-partition-closed
with_countable_Cover with_empty_element for Subset-Family of X;
coherence;
end;
theorem
bool X is semiring_of_sets of X;
Lemme4:
for X be set, a,b,c be object st [a,b] in [:X,bool X:] & c in X &
[a,b]=[c,{c}] holds a=c & b={c}
proof
let X be set, a,b,c be object;
assume [a,b] in [:X,bool X:];
assume c in X;
assume
A1: [a,b]=[c,{c}];
[a,b]`1=a & [a,b]`2=b & [c,{c}]`1=c & [c,{c}]`2={c};
hence thesis by A1;
end;
FinConv:
for D be set, SD be Subset-Family of D holds SD={y where y is Subset of D :
y is finite} iff SD=Fin D
proof
let D be set, SD be Subset-Family of D;
thus SD={y where y is Subset of D : y is finite} implies SD=Fin D
proof
assume
A1: SD={y where y is Subset of D : y is finite};
thus SD c= Fin D
proof
let x be object;
assume x in SD;
then ex y be Subset of D st x=y & y is finite by A1;
hence thesis by FINSUB_1:def 5;
end;
let x be object;
assume
B1: x in Fin D;
reconsider x as set by TARSKI:1;
x c= D & x is finite by B1,FINSUB_1:def 5;
hence thesis by A1;
end;
for D be set, SD be Subset-Family of D st SD=Fin D holds
SD={y where y is Subset of D : y is finite}
proof
let D be set;
let SD be Subset-Family of D;
assume
A4: SD=Fin D;
then
A5: SD c= {y where y is Subset of D : y is finite};
{y where y is Subset of D : y is finite} c= SD
proof
let x be object;
assume x in {y where y is Subset of D : y is finite};
then consider y be Subset of D such that
A6: x=y & y is finite;
thus thesis by A4,A6,FINSUB_1:def 5;
end;
hence thesis by A5;
end;
hence thesis;
end;
registration
let X;
cluster Fin X -> cap-finite-partition-closed
diff-c=-finite-partition-closed with_empty_element for Subset-Family of X;
coherence
proof
Fin X is cap-closed
proof
let x,y be set;
assume x in Fin X & y in Fin X;
then
A2: x is finite & y is finite & x c= X & y c= X by FINSUB_1:def 5;
x/\y c= x by XBOOLE_1:17;
then x/\y is finite & x/\y c= X by A2;
hence thesis by FINSUB_1:def 5;
end;
hence thesis by FINSUB_1:7,SETFAM_1:def 8;
end;
end;
registration
let D be denumerable set;
cluster Fin D -> with_countable_Cover for Subset-Family of D;
coherence
proof
let SD be Subset-Family of D;
assume SD=Fin D;
then
A1: SD={y where y is Subset of D : y is finite} by FinConv;
defpred P[object] means $1 in SD & ex x be set st x in D & $1={x};
consider XX being set such that
A2: for y being object holds
y in XX iff y in bool D & P[y] from XBOOLE_0:sch 1;
for x being object holds x in XX implies x in SD by A2;
then
A3: XX is Subset of SD by TARSKI:def 3;
A4: for x be object holds x in union XX iff x in D
proof
let x be object;
thus x in union XX implies x in D
proof
assume
A5: x in union XX;
consider U be set such that
A6: x in U & U in XX by A5,TARSKI:def 4;
consider y0 be set such that
A7: y0 in D & U={y0} by A2,A6;
thus x in D by A6,A7,TARSKI:def 1;
end;
thus thesis
proof
assume
A8: x in D;
then
A9: {x} is Subset of D by SUBSET_1:41;
A10: {x} in SD by A1,A9;
set y={x};
x in y & y in XX by A2,A8,A10,TARSKI:def 1;
hence x in union XX by TARSKI:def 4;
end;
end;
A11: union XX = D by A4,TARSKI:2;
XX is countable
proof
D,XX are_equipotent
proof
defpred P[object] means ex x be set st x in D & $1=[x,{x}];
consider Z being set such that
A12: for z being object holds
z in Z iff z in [:D,bool D:] & P[z] from XBOOLE_0:sch 1;
(for c be object st c in D ex xx be object st xx in XX & [c,xx] in Z)&
(for xx be object st xx in XX ex c be object st c in D & [c,xx] in Z)&
(for w1,w2,w3,w4 be object st [w1,w2] in Z &
[w3,w4] in Z holds w1=w3 iff w2=w4)
proof
A13: for c be object st c in D ex xx be object st xx in XX & [c,xx] in Z
proof
let c be object;
assume
A14: c in D;
set xx0={c};
take xx0;
[c,xx0] in [:D,bool D:] & xx0 in XX & [c,xx0] in Z
proof
A15: {c} is Subset of D by A14,SUBSET_1:33;
A16: xx0 in SD by A1,A15;
A17: {c} c= D by A14,ZFMISC_1:31;
[c,{c}] in [:D,bool D:] by A14,A17,ZFMISC_1:def 2;
hence thesis by A2,A12,A14,A16;
end;
hence thesis;
end;
A19: for xx be object st xx in XX ex c be object st c in D & [c,xx] in Z
proof
let xx be object;
assume
A20: xx in XX;
consider c0 be set such that
A21: c0 in D & xx={c0} by A2,A20;
take c0;
[c0,xx] in [:D,bool D:] & [c0,xx] in Z
proof
[c0,{c0}] in [:D,bool D:]
proof
{c0} is Subset of D by A21,SUBSET_1:41;
hence thesis by A21,ZFMISC_1:def 2;
end;
hence thesis by A12,A21;
end;
hence thesis by A21;
end;
(for w1,w2,w3,w4 be object st [w1,w2] in Z &
[w3,w4] in Z holds w1=w3 iff w2=w4)
proof
let w1,w2,w3,w4 be object;
assume
A23: [w1,w2] in Z;
assume
A24: [w3,w4] in Z;
thus w1=w3 implies w2=w4
proof
assume
A25: w1=w3;
A26: [w1,w2] in [:D,bool D:] &
ex x0 be set st x0 in D & [w1,w2]=[x0,{x0}] by A12,A23;
consider x0 be set such that
A27: x0 in D & [w1,w2]=[x0,{x0}] by A12,A23;
A28: w1=x0 & w2={x0} by A26,A27,Lemme4;
A29: [w1,w4] in [:D,bool D:] &
ex y0 be set st y0 in D & [w1,w4]=[y0,{y0}] by A12,A24,A25;
consider y0 be set such that
A30: y0 in D & [w1,w4]=[y0,{y0}] by A12,A24,A25;
A31: w1=y0 & w4={y0} by A29,A30,Lemme4;
thus thesis by A28,A31;
end;
thus w2=w4 implies w1=w3
proof
assume
A32: w2=w4;
A33: [w1,w2] in [:D,bool D:] &
ex x0 be set st x0 in D & [w1,w2]=[x0,{x0}] by A12,A23;
consider x0 be set such that
A34: x0 in D & [w1,w2]=[x0,{x0}] by A12,A23;
A35: w1=x0 & w2={x0} by A33,A34,Lemme4;
A36: [w3,w2] in [:D,bool D:] &
ex y0 be set st y0 in D & [w3,w2]=[y0,{y0}] by A12,A24,A32;
consider y0 be set such that
A37: y0 in D & [w3,w2]=[y0,{y0}] by A12,A24,A32;
w3=y0 & w2={y0} by A36,A37,Lemme4;
hence thesis by A35,ZFMISC_1:3;
end;
end;
hence thesis by A13,A19;
end;
hence thesis;
end;
hence thesis by YELLOW_8:4;
end;
hence thesis by A3,A11,Lem6a,SRINGS_1:def 4;
end;
end;
theorem
Fin X is semiring_of_sets of X by FINSUB_1:13;
Lemme9:
for X1,X2 be non empty set,S1 be non empty Subset-Family of X1,
S2 be non empty Subset-Family of X2 holds {[:a,b:] where a is Element
of S1, b is Element of S2:a in S1\{{}} & b in S2\{{}}}= {s where s is
Subset of [:X1,X2:] : ex a,b be set st a in (S1\{{}}) & b in (S2\{{}}) &
s=[:a,b:]}
proof
let X1,X2 be non empty set;
let S1 be non empty Subset-Family of X1;
let S2 be non empty Subset-Family of X2;
thus {[:a,b:] where a is Element of S1, b is Element of S2:a in S1\{{}} &
b in S2\{{}}} c= {s where s is Subset of [:X1,X2:] : ex a,b be set st
a in S1\{{}} & b in S2\{{}} & s=[:a,b:]}
proof
let x be object;
assume x in {[:a,b:] where a is Element of S1, b is Element of
S2:a in S1\{{}} & b in S2\{{}}};
then consider a be Element of S1, b be Element of S2 such that
A1: x=[:a,b:] & a in S1\{{}} & b in S2\{{}};
thus thesis by A1;
end;
let x be object;
assume x in {s where s is Subset of [:X1,X2:] : ex a,b be set st
a in S1\{{}} & b in S2\{{}} & s=[:a,b:]};
then consider s0 be Subset of [:X1,X2:] such that
A2: x=s0 & ex a0,b0 be set st
a0 in S1\{{}} & b0 in S2\{{}} & s0=[:a0,b0:];
consider a0,b0 be set such that
A3: a0 in S1\{{}} & b0 in S2\{{}} & s0=[:a0,b0:] by A2;
a0 in S1 & b0 in S2 & s0=[:a0,b0:] by TARSKI:def 3,A3,XBOOLE_1:36;
hence thesis by A2,A3;
end;
Lem7:
for x,S1,S2 be set holds
x in {[:a,b:] where a is Element of (S1\{{}}),
b is Element of (S2\{{}}):a in S1\{{}} &
b in S2\{{}}} iff x in
{[:a,b:] where a is Element of S1, b is Element of S2:a in S1\{{}} &
b in S2\{{}}}
proof
let x, S1,S2 be set;
x in {[:a,b:] where a is Element of (S1\{{}}),
b is Element of (S2\{{}}):a in S1\{{}} &
b in S2\{{}}} iff ex a0 be Element of S1\{{}}, b0 be Element of S2\{{}}
st x=[:a0,b0:] & a0 in S1\{{}} & b0 in S2\{{}};
then x in {[:a,b:] where a is Element of (S1\{{}}),
b is Element of (S2\{{}}):a in S1\{{}} &
b in S2\{{}}} iff ex a0 be Element of S1, b0 be Element of S2
st x=[:a0,b0:] & a0 in S1\{{}} & b0 in S2\{{}};
hence thesis;
end;
Lem8:
for X1,X2 be non empty set, S1 be non empty Subset-Family of X1,S2 be
non empty Subset-Family of X2 holds {[:a,b:] where a is Element of
S1\{{}}, b is Element of S2\{{}}: a in S1\{{}} & b in S2\{{}}} =
{[:a,b:] where a is Element of S1, b is Element of S2:a in S1\{{}} &
b in S2\{{}}}
proof
let X1,X2 be non empty set;
let S1 be non empty Subset-Family of X1;
let S2 be non empty Subset-Family of X2;
for x0 be object holds
x0 in {[:a,b:] where a is Element of S1\{{}},
b is Element of S2\{{}}:a in S1\{{}} &
b in S2\{{}}} iff
x0 in {[:a,b:] where a is Element of S1,
b is Element of S2:a in S1\{{}} &
b in S2\{{}}} by Lem7;
hence thesis by TARSKI:2;
end;
Lem9:
for X be set, S be Subset-Family of X, A be Subset of S holds
A is Subset-Family of X
proof
let X be set;
let S be Subset-Family of X;
let A be Subset of S;
S c= bool X;
then A c= bool X;
hence thesis;
end;
theorem
for X1,X2 be set, S1 be semiring_of_sets of X1,S2 be semiring_of_sets of X2
holds {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st x1 in S1 &
x2 in S2 & s=[:x1,x2:]} is semiring_of_sets of [:X1,X2:]
proof
let X1,X2 be set;
let S1 be semiring_of_sets of X1;
let S2 be semiring_of_sets of X2;
defpred Q[object,object] means
ex A,B being set st A = $2`1 & B = $2`2 & $1 = [:A,B:];
set Y={s where s is Subset of [:X1,X2:]: ex
x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]};
A1: Y is with_empty_element
proof
A2: {} in S1 & {} in S2 by SETFAM_1:def 8;
[:{},{}:] c= [:X1,X2:];
then {} in Y by A2;
hence thesis;
end; then
A3: Y is non empty;
reconsider Y as Subset-Family of [:X1,X2:] by Lem3;
A4: Y is cap-finite-partition-closed
proof
let D1,D2 be Element of Y;
D1 in Y by A3;
then consider s1 be Subset of [:X1,X2:] such that
A5: D1=s1 & ex x11,x12 be set st x11 in S1 & x12 in S2 & s1=[:x11,x12:];
consider x11,x12 be set such that
A6: x11 in S1 & x12 in S2 & D1=[:x11,x12:] by A5;
D2 in Y by A3;
then consider s2 be Subset of [:X1,X2:] such that
A9: D2=s2 &
ex x21,x22 be set st x21 in S1 & x22 in S2 &s2=[:x21,x22:];
consider x21,x22 be set such that
A10: x21 in S1 & x22 in S2 &D2=[:x21,x22:] by A9;
assume D1/\D2 is non empty;
then [:x11/\x21,x12/\x22:]<>{} by ZFMISC_1:100,A6,A10;
then
A13: x11/\x21 is non empty & x12/\x22 is non empty;
then consider y1 be finite Subset of S1 such that
A14: y1 is a_partition of x11/\x21 by A6,A10,SRINGS_1:def 1;
consider y2 be finite Subset of S2 such that
A15: y2 is a_partition of x12/\x22 by A6,A10,A13,SRINGS_1:def 1;
set YY= the set of all [:a,b:] where a is Element of y1,
b is Element of y2;
A16: y1 is non empty by A13,A14;
A17: y2 is non empty by A13,A15;
A18: YY c= Y
proof
let x be object;
assume x in YY;
then consider a0 be Element of y1, b0 be Element of y2 such that
A19: x=[:a0,b0:];
reconsider x as set by TARSKI:1;
A20: a0 in S1
proof
a0 in y1 by A16;
hence thesis;
end;
A21: b0 in S2
proof
b0 in y2 by A17;
hence thesis;
end;
x is Subset of [:X1,X2:]
proof
x c= [:X1,X2:]
proof
let y be object;
assume y in x;
then consider ya0,yb0 be object such that
A22: ya0 in a0 & yb0 in b0 & y=[ya0,yb0] by A19,ZFMISC_1:def 2;
thus thesis by A20,A21,A22,ZFMISC_1:def 2;
end;
hence thesis;
end;
hence thesis by A19,A20,A21;
end;
set YY= the set of all [:a,b:] where a is Element of y1,
b is Element of y2;
YY is a_partition of [:x11/\x21,x12/\x22:] by A13,A14,A15,PUA2MSS1:8;
then
A24: YY is a_partition of D1/\D2 by A6,A10,ZFMISC_1:100;
YY is finite
proof
A25: for x be object st x in YY holds
ex y be object st y in [:y1,y2:] & Q[x,y]
proof
let x be object;
assume x in YY;
then consider x1 be Element of y1, x2 be Element of y2 such that
A26: x=[:x1,x2:];
set y=[x1,x2];
reconsider Y1 = y`1, Y2 = y`2 as set;
A27: x = [:Y1,Y2:] by A26;
y in [:y1,y2:] by ZFMISC_1:def 2,A13,A14,A15;
hence thesis by A27;
end;
consider f be Function such that
A28: dom f=YY & rng f c= [:y1,y2:] and
A29: for x being object st x in YY holds Q[x,f.x]
from FUNCT_1:sch 6(A25);
f is one-to-one
proof
let a,b be object;
assume that
A30: a in dom f and
A31: b in dom f and
A32: f.a=f.b;
Q[a,f.a] & Q[b,f.a] by A29,A32,A28,A30,A31;
hence thesis;
end;
then card YY c= card [:y1,y2:] by A28,CARD_1:10;
hence thesis;
end;
hence thesis by A18,A24;
end;
Y is diff-finite-partition-closed
proof
let D3,D4 be Element of Y;
D3 in Y by A3;
then consider s1 be Subset of [:X1,X2:] such that
A34: D3=s1 &
ex x11,x12 be set st x11 in S1 & x12 in S2 & s1=[:x11,x12:];
consider x11,x12 be set such that
A35: x11 in S1 and
A36: x12 in S2 and
A37: D3=[:x11,x12:] by A34;
D4 in Y by A3;
then consider s2 be Subset of [:X1,X2:] such that
A40: D4=s2 & ex x21,x22 be set st x21 in S1 & x22 in S2 & s2=[:x21,x22:];
consider x21,x22 be set such that
A41: x21 in S1 and
A42: x22 in S2 and
A43: D4=[:x21,x22:] by A40;
assume D3\D4 is non empty;
A46: (x11\x21 is non empty & x12 <>{}) implies
ex Z1 be finite Subset of Y st Z1 is a_partition of [:x11\x21,x12:]
proof
assume
A47: x11\x21 is non empty & x12<>{};
then consider z1 be finite Subset of S1 such that
A48: z1 is a_partition of x11\x21 by A35,A41,SRINGS_1:def 2;
A49: z1 is non empty by A48,A47;
set Z1=the set of all [:u1,x12:] where u1 is Element of z1;
A50: Z1 is Subset of Y
proof
for x be object st x in Z1 holds x in Y
proof
let x be object;
assume x in Z1;
then consider a0 be Element of z1 such that
A51: x=[:a0,x12:];
A52: a0 in S1
proof
a0 in z1 by SUBSET_1:def 1,A47,A48;
hence thesis;
end;
reconsider x as set by TARSKI:1;
x is Subset of [:X1,X2:]
proof
for y be object st y in x holds y in [:X1,X2:]
proof
let y be object;
assume y in x;
then consider ya0,yx12 be object such that
A53: ya0 in a0 & yx12 in x12 & y=[ya0,yx12] by A51,ZFMISC_1:def 2;
thus thesis by A36,A52,A53,ZFMISC_1:def 2;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by A51,A52,A36;
end;
hence thesis by TARSKI:def 3;
end;
A56: Z1 is finite
proof
defpred P[object,object] means
ex A being set st A = $2 & $1 = [:A,x12:];
A57: for x be object st x in Z1 ex y be object st y in z1 & P[x,y]
proof
let x be object;
assume x in Z1;
then consider x1 be Element of z1 such that
A58: x=[:x1,x12:];
take x1;
thus thesis by A49,A58;
end;
consider f be Function such that
A59: dom f=Z1 & rng f c= z1 and
A60: for x being object st x in Z1 holds
P[x,f.x] from FUNCT_1:sch 6(A57);
f is one-to-one
proof
let a,b be object;
assume that
A61: a in dom f and
A62: b in dom f and
A63: f.a=f.b;
P[a,f.a] & P[b,f.b] by A59,A60,A61,A62;
hence thesis by A63;
end;
then card Z1 c= card z1 by A59,CARD_1:10;
hence thesis;
end;
Z1 is a_partition of [:x11\x21,x12:]
proof
set Z2=the set of all [:p,q:] where p is Element of z1,
q is Element of {x12};
A65: Z1=Z2
proof
A66: Z1 c= Z2
proof
let x be object;
assume x in Z1;
then consider x00 be Element of z1 such that
A67: x=[:x00,x12:];
x12 is Element of {x12} by TARSKI:def 1;
hence thesis by A67;
end;
Z2 c= Z1
proof
let x be object;
assume x in Z2;
then consider x01 be Element of z1,x02 be Element of {x12}
such that
A68: x=[:x01,x02:];
x=[:x01,x12:] by A68,TARSKI:def 1;
hence thesis;
end;
hence thesis by A66;
end;
{x12} is a_partition of x12 by A47,EQREL_1:39;
hence thesis by A65,PUA2MSS1:8,A47,A48;
end;
hence thesis by A50,A56;
end;
A71: (x11/\x21 <>{} & x12\x22 <>{}) implies
ex Z2 be finite Subset of Y st Z2 is a_partition of [:x11/\x21,x12\x22:]
proof
assume
A72: x11/\x21<>{} & x12\x22<>{};
then consider z1 be finite Subset of S1 such that
A73: z1 is a_partition of x11/\x21 by A35,A41,SRINGS_1:def 1;
consider z2 be finite Subset of S2 such that
A74: z2 is a_partition of x12\x22 by A72,A36,A42,SRINGS_1:def 2;
A75: z2 is non empty by A72,A74;
set Z2=the set of all [:u1,u2:] where u1 is Element of z1,
u2 is Element of z2;
A76: Z2 is Subset of Y
proof
for x be object st x in Z2 holds x in Y
proof
let x be object;
assume x in Z2;
then consider a0 be Element of z1, b0 be Element of z2 such that
A77: x=[:a0,b0:];
reconsider x as set by TARSKI:1;
A78: a0 in S1
proof
a0 in z1 by SUBSET_1:def 1,A72,A73;
hence thesis;
end;
A79: b0 in S2
proof
b0 in z2 by A75;
hence thesis;
end;
x is Subset of [:X1,X2:]
proof
for y be object st y in x holds y in [:X1,X2:]
proof
let y be object;
assume y in x;
then consider ya0,yb0 be object such that
A80: ya0 in a0 & yb0 in b0 & y=[ya0,yb0] by A77,ZFMISC_1:def 2;
thus thesis by A78,A79,A80,ZFMISC_1:def 2;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by A77,A78,A79;
end;
hence thesis by TARSKI:def 3;
end;
A83: Z2 is finite
proof
A84: for x be object st x in Z2 holds
ex y be object st y in [:z1,z2:] & Q[x,y]
proof
let x be object;
assume x in Z2;
then consider x1 be Element of z1, x2 be Element of z2 such that
A85: x=[:x1,x2:];
set y=[x1,x2];
reconsider Y1 = y`1, Y2 = y`2 as set;
A86: x=[:Y1,Y2:] by A85;
y in [:z1,z2:] by A74,A73,A72,ZFMISC_1:def 2;
hence thesis by A86;
end;
consider f be Function such that
A87: dom f=Z2 & rng f c= [:z1,z2:] and
A88: for x being object st x in Z2 holds
Q[x,f.x] from FUNCT_1:sch 6(A84);
f is one-to-one
proof
let a,b be object;
assume that
A89: a in dom f and
A90: b in dom f and
A91: f.a=f.b;
reconsider Y1 = (f.a)`1, Y2 = (f.a)`2 as set by TARSKI:1;
Q[a,f.a] & Q[b,f.b] by A87,A88,A89,A90;
hence thesis by A91;
end;
then card Z2 c= card [:z1,z2:] by A87,CARD_1:10;
hence thesis;
end;
Z2 is a_partition of [:x11/\x21,x12\x22:] by PUA2MSS1:8,A73,A74,A72;
hence thesis by A76,A83;
end;
A94: ([:x11\x21,x12:]<>{} & [:x11/\x21,x12\x22:]={}) implies
ex ZZ be set st ZZ is a_partition of [:x11,x12:]\[:x21,x22:] &
ZZ is finite Subset of Y
proof
assume
A95: ([:x11\x21,x12:]<>{} & [:x11/\x21,x12\x22:]={});
then consider ZZ be finite Subset of Y such that
A96: ZZ is a_partition of [:x11\x21,x12:] by A46;
[:x11,x12:]\[:x21,x22:]=
[:x11\x21,x12:]\/[:x11/\x21,x12\x22:] by Lem4;
hence thesis by A95,A96;
end;
A97: ([:x11\x21,x12:]={}) & ([:x11/\x21,x12\x22:]<>{}) implies
ex ZZ be set st ZZ is a_partition of [:x11,x12:]\[:x21,x22:] &
ZZ is finite Subset of Y
proof
assume
A98: ([:x11\x21,x12:]={}) & ([:x11/\x21,x12\x22:]<>{});
then consider ZZ be finite Subset of Y such that
A99: ZZ is a_partition of [:x11/\x21,x12\x22:] by A71;
[:x11,x12:]\[:x21,x22:]=
[:x11\x21,x12:]\/[:x11/\x21,x12\x22:] by Lem4;
hence thesis by A98,A99;
end;
A100: ([:x11\x21,x12:]={}) &
([:x11/\x21,x12\x22:]={}) implies ex ZZ be set
st ZZ is a_partition of
[:x11,x12:]\[:x21,x22:] & ZZ is finite Subset of Y
proof
assume
A101: ([:x11\x21,x12:]={}) & ([:x11/\x21,x12\x22:]={});
take {};
[:x11,x12:]\[:x21,x22:]=
[:x11\x21,x12:]\/[:x11/\x21,x12\x22:] by Lem4;
hence thesis by A101,EQREL_1:45,SUBSET_1:1;
end;
[:x11\x21,x12:]<>{} & [:x11/\x21,x12\x22:]<>{}implies
ex ZZ be set st ZZ is a_partition of [:x11,x12:]\[:x21,x22:] &
ZZ is finite Subset of Y
proof
assume
A104: ([:x11\x21,x12:]<>{}) & ([:x11/\x21,x12\x22:]<>{});
then consider p1 be finite Subset of Y such that
A105: p1 is a_partition of [:x11\x21,x12:] by A46;
consider p2 be finite Subset of Y such that
A106: p2 is a_partition of [:x11/\x21,x12\x22:] by A71,A104;
[:x11,x12:]\[:x21,x22:]=[:x11\x21,x12:]\/[:x11/\x21,x12\x22:] &
[:x11\x21,x12:] misses [:x11/\x21,x12\x22:] by Lem4;
then
A107: p1\/p2 is a_partition of [:x11,x12:]\[:x21,x22:]
by A105,A106,DILWORTH:3;
thus thesis by A107;
end;
hence thesis by A37,A43,A94,A97,A100;
end;
hence thesis by A1,A4;
end;
theorem
for X1,X2 be non empty set, S1 be with_countable_Cover Subset-Family of X1,
S2 be with_countable_Cover Subset-Family of X2, S be Subset-Family of
[:X1,X2:] st S= {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st
x1 in S1 & x2 in S2 & s=[:x1,x2:]} holds S is with_countable_Cover
proof
let X1,X2 be non empty set;
let S1 be with_countable_Cover Subset-Family of X1;
let S2 be with_countable_Cover Subset-Family of X2;
let S be Subset-Family of [:X1,X2:];
assume
A1: S= {s where s is Subset of [:X1,X2:]: ex
x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]};
ex U be countable Subset of S st union U = [:X1,X2:] & U is Subset of S
proof
consider U1 be countable Subset of S1 such that
A2: U1 is Cover of X1 by SRINGS_1:def 4;
A3: union U1 = X1 by A2,Lem6a;
consider U2 be countable Subset of S2 such that
A4: U2 is Cover of X2 by SRINGS_1:def 4;
A5: union U2=X2 by A4,Lem6a;
set U={u where u is Subset of [:X1,X2:] :ex u1,u2 be set st
u1 in U1\{{}} & u2 in U2\{{}} & u=[:u1,u2:]};
A6: U1 is non empty by A2,ZFMISC_1:2,Lem6a;
A7: U1\{{}} is non empty
proof
assume U1\{{}} is empty;
then union U1 c= union {{}} by ZFMISC_1:77,XBOOLE_1:37;
hence thesis by A2,Lem6a;
end;
A8: U2 is non empty by A4,Lem6a,ZFMISC_1:2;
A9: U2\{{}} is non empty
proof
assume U2\{{}} is empty;
then union U2 c= union {{}} by ZFMISC_1:77,XBOOLE_1:37;
hence contradiction by A4,Lem6a;
end;
set V={[:a,b:] where a is Element of U1,
b is Element of U2 :a in U1\{{}} & b in U2\{{}}};
A10: U=V
proof
U1 is Subset-Family of X1 & U2 is Subset-Family of X2 by Lem9;
hence thesis by A6,A8,Lemme9;
end;
U is Subset of S
proof
for x be object st x in U holds x in S
proof
let x be object;
assume x in U;
then consider u0 be Subset of [:X1,X2:] such that
A11: x=u0 & ex u1,u2 be set st
u1 in U1\{{}} & u2 in U2\{{}} & u0=[:u1,u2:];
reconsider x as Subset of [:X1,X2:] by A11;
thus thesis by A1,A11;
end;
hence thesis by TARSKI:def 3;
end;
then reconsider U as Subset of S;
A12: U is countable
proof
U1\{{}} is countable & U2\{{}} is countable by CARD_3:95;
then
A13: [:U1\{{}},U2\{{}}:] is countable by CARD_4:7;
set W=[:U1\{{}},U2\{{}}:];
V, W are_equipotent
proof
set Z={[[:u1,u2:],[u1,u2]] where u1 is Element of U1,
u2 is Element of U2: u1 in U1\{{}} & u2 in U2\{{}}};
A14: (for v be object st v in V ex w be object st w in W & [v,w] in Z)&
(for w be object st w in W ex v be object st v in V & [v,w] in Z)&
for v1,v2,w1,w2 be object st [v1,w1] in Z & [v2,w2] in Z holds
v1=v2 iff w1=w2
proof
A15: for v be object st v in V ex w be object st w in W & [v,w] in Z
proof
let v be object;
assume v in V;
then consider u1 be Element of U1 such that
A16: ex u2 be Element of U2
st v=[:u1,u2:] & u1 in U1\{{}} & u2 in U2\{{}};
consider u2 be Element of U2 such that
A17: v=[:u1,u2:] & u1 in U1\{{}} & u2 in U2\{{}} by A16;
set w=[u1,u2];
take w;
thus thesis by A17,ZFMISC_1:def 2;
end;
A18: for w be object st w in W ex v be object st v in V & [v,w] in Z
proof
let w be object;
assume w in W;
then ex u1,u2 be object st u1 in U1\{{}} &
u2 in U2\{{}} & w=[u1,u2] by ZFMISC_1:def 2;
then consider u1,u2 be set such that
A19: w=[u1,u2] & u1 in U1\{{}} & u2 in U2\{{}};
set v=[:u1,u2:];
take v;
u1 is Element of U1 & u2 is Element of U2
by A19,XBOOLE_1:36,TARSKI:def 3;
hence thesis by A19;
end;
for v1,v2,w1,w2 be object st [v1,w1] in Z & [v2,w2] in Z holds
v1=v2 iff w1=w2
proof
let v1,v2,w1,w2 be object;
assume [v1,w1] in Z;
then consider a1 be Element of U1, a2 be Element of U2 such that
A21: [v1,w1]=[[:a1,a2:],[a1,a2]] &
a1 in U1\{{}} & a2 in U2\{{}};
A22: v1=[:a1,a2:] & w1=[a1,a2] by A21,XTUPLE_0:1;
assume [v2,w2] in Z;
then consider b1 be Element of U1, b2 be Element of U2 such that
A23: [v2,w2]=[[:b1,b2:],[b1,b2]]&b1 in U1\{{}} & b2 in U2\{{}};
A24: v2=[:b1,b2:] & w2=[b1,b2] by A23,XTUPLE_0:1;
thus v1=v2 implies w1=w2
proof
assume
A25: v1=v2;
not a1 in {{}} & not a2 in {{}} by A21,XBOOLE_0:def 5;
then a1 <> {} & a2 <>{} by TARSKI:def 1;
then a1=b1 & a2=b2 by A22,A24,A25,ZFMISC_1:110;
hence thesis by A21,A23,XTUPLE_0:1;
end;
assume
A26: w1=w2;
w1=[a1,a2] & w2=[b1,b2] by A21,A23,XTUPLE_0:1;
then a1=b1 & a2=b2 by A26,XTUPLE_0:1;
hence thesis by A21,A23,XTUPLE_0:1;
end;
hence thesis by A15,A18;
end;
ex Z be set st
(for v be object st v in V ex w be object st w in W & [v,w] in Z)&
(for w be object st w in W ex v be object st v in V & [v,w] in Z)&
(for x,y,z,u be object st [x,y] in Z & [z,u] in Z holds
x=z iff y=u)
proof
take Z;
thus thesis by A14;
end;
hence thesis;
end;
hence thesis by A10,A13,YELLOW_8:4;
end;
union U=[:X1,X2:]
proof
set V2= {[:a,b:] where a is Element of U1\{{}},
b is Element of U2\{{}} : a in U1\{{}} & b in U2\{{}}};
A26: U=V2
proof
U1 is Subset-Family of X1 & U2 is Subset-Family of X2 by Lem9;
hence thesis by A6,A8,A10,Lem8;
end;
union (U1\{{}})=union U1 & union(U2\{{}})=union U2 by PARTIT1:2;
hence thesis by A3,A5,A7,A9,A26,LATTICE5:2;
end;
hence thesis by A12;
end;
hence thesis by Lem6a,SRINGS_1:def 4;
end;
THS0:
{{}}\/{s where s is Subset of REAL:ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)} =
{s where s is Subset of REAL:ex a,b be Real st a<=b &
for x be real number holds x in s iff (a<x & x<=b)}
proof
set S1={{}}\/{s where s is Subset of REAL:ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)};
set S2={s where s is Subset of REAL:ex a,b be Real st a<=b &
for x be real number holds x in s iff (a<x & x<=b)};
A1: S1 c= S2
proof
let x be object;
assume x in S1; then
A2: x in {{}} or x in {s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)} by XBOOLE_0:def 3;
A3: x={} implies x in S2
proof
set a=0;
set b=0;
set s0=].a,b.];
for x be real number holds x in s0 iff (a<x & x<=b);
hence thesis;
end;
x in {s where s is Subset of REAL:ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)} implies x in S2
proof
assume x in {s where s is Subset of REAL:ex a,b be Real st a<b &
for t be real number holds t in s iff (a<t & t<=b)};
then consider s0 be Subset of REAL such that
A4: s0=x & ex a,b be Real st a<b &
for t be real number holds t in s0 iff (a<t & t<=b);
thus thesis by A4;
end;
hence thesis by A2,A3,TARSKI:def 1;
end;
S2 c= S1
proof
let x be object;
assume x in S2;
then consider s0 be Subset of REAL such that
A5: x=s0 and
A6: ex a,b be Real st a<=b &
for t be real number holds t in s0 iff (a<t & t<=b);
consider a,b be Real such that
A7: a<=b and
A8: for t be real number holds t in s0 iff (a<t & t<=b) by A6;
A9: a=b implies x in {{}}
proof
assume a=b;
then s0 c= {} by A8;
then x={} by A5;
hence thesis by TARSKI:def 1;
end;
a<b implies x in {s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)} by A5,A8;
hence thesis by XBOOLE_0:def 3,XXREAL_0:1,A7,A9;
end;
hence thesis by A1;
end;
set II = {].a,b.] where a,b is Real:a<=b};
II c= bool REAL
proof
let x be object;
assume x in II;
then ex a0,b0 be Real st x = ].a0,b0.] & a0<=b0;
hence thesis;
end;
then reconsider II as Subset-Family of REAL;
THS2:
{s where s is Subset of REAL:ex a,b be Real st a<=b &
for x be real number holds x in s iff (a<x & x<=b)} = II
proof
set S1={s where s is Subset of REAL:ex a,b be Real st a<=b &
for x be real number holds x in s iff (a<x & x<=b)};
A1: S1 c= II
proof
let y be object;
assume y in S1;
then consider s0 be Subset of REAL such that
A2: y=s0 & ex a,b be Real st a<=b &
for x be real number holds x in s0 iff (a<x & x<=b);
consider a0,b0 be Real such that
A3: a0<=b0 & for x be real number holds x in s0 iff (a0<x & x<=b0) by A2;
A4: s0 c= ].a0,b0.]
proof
let x be object;
assume
A5: x in s0;
then reconsider x as real number;
a0<x & x<=b0 by A3,A5;
hence thesis;
end;
].a0,b0.] c= s0
proof
let x be object;
assume
A6: x in ].a0,b0.];
then reconsider x as real number;
a0<x & x<=b0 by A6,XXREAL_1:2;
hence thesis by A3;
end;
then s0 = ].a0,b0.] by A4;
hence thesis by A2,A3;
end;
II c= S1
proof
let y be object;
assume y in II;
then consider a0,b0 be Real such that
A7: y = ].a0,b0.] & a0<=b0;
reconsider y as set by TARSKI:1;
for x be real number holds x in y iff (a0<x & x<=b0) by A7,XXREAL_1:2;
hence thesis by A7;
end;
hence thesis by A1;
end;
THS1:
for S be Subset-Family of REAL st
S={{}}\/{s where s is Subset of REAL:ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}
holds S is cap-closed & S is diff-finite-partition-closed
with_empty_element Subset-Family of REAL
proof
let S be Subset-Family of REAL such that
A1: S={{}}\/{s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)};
A2: S is with_empty_element
proof
{} in {{}} by TARSKI:def 1;
then {} in S by A1,XBOOLE_0:def 3;
hence thesis;
end;
A3: S is cap-closed
proof
let e1,e2 be set;
assume
A4: e1 in S;
assume
A5: e2 in S;
A6: e1 in {{}} or e1 in {s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}
by A1,A4,XBOOLE_0:def 3;
A7: e2 in {{}} or e2 in {s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}
by A1,A5,XBOOLE_0:def 3;
A8: e1={} implies e1/\e2 in S
proof
assume e1={};
then e1/\e2 in {{}} by TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 3;
end;
A9: e2={} implies e1/\e2 in S
proof
assume e2={};
then e1/\e2 in {{}} by TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 3;
end;
(e1 in {s where s is Subset of REAL: ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}) &
(e2 in {s where s is Subset of REAL: ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}) implies e1/\e2 in S
proof
assume
A10: e1 in {s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)};
assume
A11: e2 in {s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)};
consider E1 be Subset of REAL such that
A12: e1=E1 & ex a1,b1 be Real st a1<b1 &
for x be real number holds x in E1 iff (a1<x & x<=b1) by A10;
consider E2 be Subset of REAL such that
A13: e2=E2 & ex a2,b2 be Real st a2<b2 &
for x be real number holds x in E2 iff (a2<x & x<=b2) by A11;
consider a1,b1 be Real such that
A14: a1<b1 & for x be real number holds x in E1 iff (a1<x & x<=b1) by A12;
consider a2,b2 be Real such that
A15: a2<b2 & for x be real number holds x in E2 iff (a2<x & x<=b2) by A13;
e1/\e2 in {{}}\/{s where s is Subset of REAL:ex a,b be Real
st a<b & for x be real number holds x in s iff (a<x & x<=b)}
proof
A16: b1<=a2 implies e1/\e2 in {{}}
proof
assume
A17: b1<=a2;
e1/\e2 c= {}
proof
let x be object;
assume
A18: x in e1/\e2; then
A19: x in e1 & x in e2 by XBOOLE_0:def 4;
reconsider x as real number by A13,A18;
a1<x & x <= b1 & a2<x & x<=b2 by A12,A13,A14,A15,A19;
hence thesis by A17,XXREAL_0:2;
end;
then e1/\e2={};
hence thesis by TARSKI:def 1;
end;
A20: a2<b1 & a1<b2 implies
e1/\e2 in {s where s is Subset of REAL:ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)} or e1/\e2 in {{}}
proof
set P={s where s is Subset of REAL:ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)};
assume a2<b1 & a1<b2;
A21: a2<a1 & b2<b1 & a1<b2 implies e1/\e2 in P
proof
assume
A22: a2<a1 & b2<b1;
assume
A23: a1<b2;
A24: for x be real number holds x in e1/\e2 iff (a1<x & x<=b2)
proof
A25: for x be real number st x in e1/\e2 holds (a1<x & x<=b2)
proof
let x be real number;
assume x in e1/\e2;
then x in e1 & x in e2 by XBOOLE_0:def 4;
hence thesis by A12,A13,A14,A15;
end;
for x be real number st (a1<x & x<=b2) holds x in e1/\e2
proof
let x be real number;
assume
A26: a1<x & x<=b2; then
A27: x<=b1 by A22,XXREAL_0:2;
a1<x & a2<a1 implies a2<x by XXREAL_0:2; then
x in e1 & x in e2 by A12,A13,A14,A15,A22,A26,A27;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by A25;
end;
e1/\e2=E1/\E2 by A12,A13;
hence thesis by A23,A24;
end;
A28: a2<a1 & b2<b1 & not a1<b2 implies e1/\e2 in {{}}
proof
assume
A29: a2<a1 & b2<b1 & not a1<b2;
e1/\e2 c= {}
proof
let x be object;
assume
A30: x in e1/\e2; then
A31: x in e1 & x in e2 by XBOOLE_0:def 4;
reconsider x as real number by A12,A30;
a1<x & x <= b1 & a2<x & x<=b2 by A12,A13,A14,A15,A31;
hence thesis by A29,XXREAL_0:2;
end;
then e1/\e2={};
hence thesis by TARSKI:def 1;
end;
A32: a2<a1 & b1<=b2 implies e1/\e2 in P
proof
assume
A33: a2<a1 & b1<=b2;
A34: for x be real number holds x in e1/\e2 iff (a1<x & x<=b1)
proof
A35: for x be real number st x in e1/\e2 holds (a1<x & x<=b1)
proof
let x be real number;
assume x in e1/\e2;
then x in e1 & x in e2 by XBOOLE_0:def 4;
hence thesis by A12,A14;
end;
for x be real number st (a1<x & x<=b1) holds x in e1/\e2
proof
let x be real number;
assume a1<x & x<=b1;
then a1<x & x<=b1 & a2<x & x<=b2 by A33,XXREAL_0:2;
then x in e1 & x in e2 by A12,A13,A14,A15;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by A35;
end;
e1/\e2=E1/\E2 by A12,A13;
hence thesis by A14,A34;
end;
A37: a1<=a2 & b2<b1 implies e1/\e2 in P
proof
assume
A38: a1<=a2 & b2<b1;
A39: for x be real number holds x in e1/\e2 iff (a2<x & x<=b2)
proof
A40: for x be real number st x in e1/\e2 holds (a2<x & x<=b2)
proof
let x be real number;
assume x in e1/\e2;
then x in e1 & x in e2 by XBOOLE_0:def 4;
hence thesis by A13,A15;
end;
for x be real number st (a2<x & x<=b2) holds x in e1/\e2
proof
let x be real number;
assume
A41: a2<x & x<=b2;
A42: a2<x & a1<=a2 implies a1<x by XXREAL_0:2;
x<=b2 & b2<b1 implies x<=b1 by XXREAL_0:2;
then x in e1 & x in e2 by A12,A13,A14,A15,A38,A41,A42;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by A40;
end;
e1/\e2=E1/\E2 by A12,A13;
hence thesis by A15,A39;
end;
A43: a1<=a2 & b1<=b2 & not a2<b1 implies e1/\e2 in {{}}
proof
assume
A44: a1<=a2 & b1<=b2 & not a2<b1;
e1/\e2 c= {}
proof
let x be object;
assume
A45: x in e1/\e2;
then
A46: x in e1 & x in e2 by XBOOLE_0:def 4;
reconsider x as real number by A12,A45;
a2<x & x<=b1 by A12,A13,A14,A15,A46;
hence thesis by A44,XXREAL_0:2;
end;
then e1/\e2={};
hence thesis by TARSKI:def 1;
end;
a1<=a2 & b1<=b2 & a2<b1 implies e1/\e2 in P
proof
assume
A47: a1<=a2 & b1<=b2 & a2<b1;
A48: for x be real number holds x in e1/\e2 iff (a2<x & x<=b1)
proof
A49: for x be real number st x in e1/\e2 holds (a2<x & x<=b1)
proof
let x be real number;
assume x in e1/\e2;
then x in e1 & x in e2 by XBOOLE_0:def 4;
hence thesis by A12,A13,A14,A15;
end;
for x be real number st (a2<x & x<=b1) holds x in e1/\e2
proof
let x be real number;
assume
A50: a2<x & x<=b1;
then
A51: x<=b2 by A47,XXREAL_0:2;
a2<x & a1<=a2 implies a1<x by XXREAL_0:2;
then x in e1 & x in e2 by A12,A13,A14,A15,A47,A50,A51;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by A49;
end;
e1/\e2=E1/\E2 by A12,A13;
hence thesis by A47,A48;
end;
hence thesis by A21,A28,A32,A37,A43;
end;
a2<b1 & b2<=a1 implies e1/\e2 in {{}}
proof
assume
A52: a2<b1 & b2<=a1;
e1/\e2 c= {}
proof
let x be object;
assume
A53: x in e1/\e2; then
A54: x in e1 & x in e2 by XBOOLE_0:def 4;
reconsider x as real number by A12,A53;
a1<x & x <= b1 & a2<x & x<=b2 by A12,A13,A14,A15,A54;
hence thesis by A52,XXREAL_0:2;
end;
then e1/\e2={};
hence thesis by TARSKI:def 1;
end;
hence thesis by A16,A20,XBOOLE_0:def 3;
end;
hence thesis by A1;
end;
hence thesis by A6,A7,A8,A9,TARSKI:def 1;
end;
S is diff-finite-partition-closed
proof
(for S3,S4 be Element of S st S3\S4 is non empty
ex z be finite Subset of S st
z is a_partition of S3\S4)
proof
let S3,S4 be Element of S;
assume
A55: S3\S4 is non empty;
A57: not S3 in {{}} by A55,TARSKI:def 1;
A58: S4 in {{}} or S4 in {s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}
by A1,XBOOLE_0:def 3;
A59: S4={} implies ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume
A60: S4={};
A61: {S3} c= S
proof
let x be object;
assume x in {S3};
then x is Element of S by TARSKI:def 1;
hence thesis by A2,SUBSET_1:def 1;
end;
{S3} is a_partition of S3 by A55,EQREL_1:39;
hence thesis by A60,A61;
end;
S4 in {s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)} implies
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume
A62: S4 in {s where s is Subset of REAL:
ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)};
S3 in {s where s is Subset of REAL: ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}
by A1,A57,XBOOLE_0:def 3;
then consider E1 be Subset of REAL such that
A63: S3=E1 & ex a1,b1 be Real st a1<b1 &
for x be real number holds x in E1 iff (a1<x & x<=b1);
consider E2 be Subset of REAL such that
A64: S4=E2 & ex a2,b2 be Real st a2<b2 &
for x be real number holds x in E2 iff (a2<x & x<=b2) by A62;
consider a1,b1 be Real such that
A65: a1<b1 &
for x be real number holds x in E1 iff (a1<x & x<=b1) by A63;
consider a2,b2 be Real such that
A66: a2<b2 &
for x be real number holds x in E2 iff (a2<x & x<=b2) by A64;
A67: for x be real number holds x in S3\S4 iff
((a1<x & x<=b1) & not (a2<x & x<=b2))
proof
A68: for x be real number st x in S3\S4 holds
((a1<x & x<=b1) & not (a2<x & x<=b2) )
proof
let x be real number;
assume x in S3\S4;
then x in S3 & not x in S4 by XBOOLE_0:def 5;
hence thesis by A63,A64,A65,A66;
end;
for x be real number st
((a1<x & x<=b1) & not (a2<x & x<=b2)) holds x in S3\S4
proof
let x be real number;
assume (a1<x & x<=b1) & not (a2<x & x<=b2);
then x in S3 & not x in S4 by A63,A64,A65,A66;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by A68;
end;
A69: a1<b1 & a2<b2 &b1<= a2 & b1<=b2 implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A70: a1<b1 & a2<b2 &b1<= a2 & b1<=b2;
A71: S3\S4=S3
proof
S3 c= S3\S4
proof
let x be object;
assume
A72: x in S3;
then reconsider x as real number by A63;
a1<x & x<=b1 by A63,A65,A72;
then ((a1<x & x<=b1) & not (a2<x & x<=b2)) by A70,XXREAL_0:2;
hence thesis by A67;
end;
hence thesis;
end;
A72a: {S3} c= S
proof
let x be object;
assume x in {S3};
then x is Element of S by TARSKI:def 1;
hence thesis by A2,SUBSET_1:def 1;
end;
{S3} is a_partition of S3 by A55,EQREL_1:39;
hence thesis by A71,A72a;
end;
A74: a1<b1 & a2<b2 & a2<b1 & a1<=a2 & b1<=b2 implies
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume
A75: a1<b1 & a2<b2 & a2<b1 & a1<=a2 & b1<=b2;
A76: a1<b1 & a2<b2 & a2<b1 & a1=a2 & b1<=b2 implies
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume
A77: a1<b1 & a2<b2 & a2<b1 & a1=a2 & b1<=b2;
S3\S4 c= {}
proof
let y be object;
assume
A78: y in S3\S4;
then reconsider y as real number by A63;
(a1<y & y<=b1 ) & (y<=a2 or b2<y) by A67,A78;
hence thesis by A77,XXREAL_0:2;
end;
hence thesis by A55;
end;
a1<b1 & a2<b2 & a2<b1 & a1<a2 & b1<=b2 implies
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume
A79: a1<b1 & a2<b2 & a2<b1 & a1<a2 & b1<=b2;
set P={x where x is real number:a1<x & x<=a2};
A80: S3\S4=P
proof
A81: S3\S4 c= {x where x is real number:a1<x & x<=a2}
proof
let y be object;
assume
A82: y in S3\S4;
then reconsider y as real number by A63;
(a1<y & y<=b1) & (y<=a2 or b2<y) by A67,A82;
hence thesis by A79,XXREAL_0:2;
end;
{x where x is real number:a1<x & x<=a2} c= S3\S4
proof
let y be object;
assume y in {x where x is real number:a1<x & x<=a2};
then consider y0 be real number such that
A83: y=y0 & a1<y0 & y0<=a2;
(a1<y0 & y0<=b1 ) & (y0<=a2 or b2<y0) by A79,A83,XXREAL_0:2;
hence thesis by A67,A83;
end;
hence thesis by A81;
end;
A83a: {P} c= S
proof
let x be object;
assume x in {P}; then
A84: x=P by TARSKI:def 1;
P in {s where s is Subset of REAL:ex a,b be Real
st a<b & for x be real number holds x in s iff (a<x & x<=b)}
proof
A86: P c= REAL
proof
let x be object;
assume x in P;
then consider x0 be real number such that
A87: x=x0 & a1<x0 & x0<=a2;
thus thesis by A87,XREAL_0:def 1;
end;
for x be real number holds x in P iff (a1<x & x<=a2)
proof
for x be real number st x in P holds (a1<x & x<=a2)
proof
let x be real number;
assume x in P;
then consider x0 be real number such that
A89: x=x0 & a1<x0 & x0<=a2;
thus thesis by A89;
end;
hence thesis;
end;
hence thesis by A79,A86;
end;
hence thesis by A1,A84,XBOOLE_0:def 3;
end;
{P} is a_partition of P by A80,A55,EQREL_1:39;
hence thesis by A80,A83a;
end;
hence thesis by A75,A76,XXREAL_0:1;
end;
A90: a1<b1 & a2<b2 & a2<b1 & a1<=a2 & b2<b1 & a1<b2 implies
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume
A91: a1<b1 & a2<b2 & a2<b1 & a1<=a2 & b2<b1 & a1<b2;
A92: a1<b1 & a2<b2 & a2<b1 & a1<a2 & b2<b1 & a1<b2 implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A93: a1<b1 & a2<b2 & a2<b1 & a1<a2 & b2<b1 & a1<b2;
set P1={x where x is Real:a1<x & x<=a2};
A94: P1 in S
proof
P1 in {s where s is Subset of REAL:ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}
proof
P1 c= REAL
proof
let x be object;
assume x in P1;
then consider x0 be Real such that
A96: x=x0 & a1<x0 & x0<=a2;
thus thesis by A96,XREAL_0:def 1;
end; then
A95: P1 is Subset of REAL;
for x be real number holds x in P1 iff (a1<x & x<=a2)
proof
for x be real number st x in P1 holds (a1<x & x<=a2)
proof
let x be real number;
assume x in P1;
then consider x0 be Real such that
A97: x=x0 & (a1<x0 & x0<=a2);
thus thesis by A97;
end;
hence thesis;
end;
hence thesis by A93,A95;
end;
hence thesis by A1,XBOOLE_0:def 3;
end;
set P2={x where x is Real:b2<x & x<=b1};
A98: P2 in S
proof
P2 in {s where s is Subset of REAL:ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}
proof
A99: P2 is Subset of REAL
proof
P2 c= REAL
proof
let x be object;
assume x in P2;
then consider x0 be Real such that
A100: x=x0 & b2<x0 & x0<=b1;
thus thesis by A100,XREAL_0:def 1;
end;
hence thesis;
end;
for x be real number holds x in P2 iff (b2<x & x<=b1)
proof
for x be real number st x in P2 holds (b2<x & x<=b1)
proof
let x be real number;
assume x in P2;
then consider x0 be Real such that
A101: x=x0 & (b2<x0 & x0<=b1);
thus thesis by A101;
end;
hence thesis;
end;
hence thesis by A93,A99;
end;
hence thesis by A1,XBOOLE_0:def 3;
end;
A101a: {P1,P2}c=S by A94,A98,TARSKI:def 2;
A102: {P1,P2} is Subset-Family of S3\S4
proof
{P1,P2} c= bool (S3\S4)
proof
let x be object;
assume
A103: x in {P1,P2};
A104: P1 in bool (S3\S4)
proof
P1 c= S3\S4
proof
let x be object;
assume x in P1;
then consider x0 be Real such that
A105: x=x0 & a1<x0 & x0<=a2;
reconsider x as real number by A105,TARSKI:1;
a1<x & x<=a2 & x<=b1 by A93,A105,XXREAL_0:2;
hence thesis by A67;
end;
hence thesis;
end;
P2 in bool (S3\S4)
proof
P2 c= S3\S4
proof
let x be object;
assume x in P2;
then consider x0 be Real such that
A106: x=x0 & b2<x0 & x0<=b1;
reconsider x as real number by A106,TARSKI:1;
a1<x & b2<x & x<=b1 by A93,A106,XXREAL_0:2;
hence thesis by A67;
end;
hence thesis;
end;
hence thesis by A103,A104,TARSKI:def 2;
end;
hence thesis;
end;
A107: union {P1,P2}=S3\S4
proof
A108: union{P1,P2}=P1\/P2 by ZFMISC_1:75;
A109: P1\/P2 c= S3\S4
proof
union {P1,P2} c= union (bool (S3\S4)) by A102,ZFMISC_1:77;
hence thesis by A108,ZFMISC_1:81;
end;
S3\S4 c= P1\/P2
proof
let y be object;
assume
A110: y in S3\S4;
then reconsider y as real number by A63;
(a1<y & y<=a2) or
(b2<y & y<=b1) by A67,A110;
then y in P1 or y in P2;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by ZFMISC_1:75,A109;
end;
for A be Subset of S3\S4 st A in {P1,P2} holds A<>{} &
for B be Subset of S3\S4 st B in {P1,P2} holds A=B or A misses B
proof
let A be Subset of S3\S4;
assume
A111: A in {P1,P2};
A112: P1 <> {}
proof
a2 in P1 by A93;
hence thesis;
end;
A113: P2<>{}
proof
b1 in P2 by A93;
hence thesis;
end;
for B be Subset of S3\S4 st B in {P1,P2} holds
A=B or A misses B
proof
let B be Subset of S3\S4;
assume B in {P1,P2};
then
A114: (A=P1 & B=P1) or (A=P1 & B=P2) or (A=P2 & B=P1) or
(A=P2 & B=P2) by A111,TARSKI:def 2;
P1 misses P2
proof
P1/\P2 c= {}
proof
let x be object;
assume x in P1/\P2; then
A115: x in P1 & x in P2 by XBOOLE_0:def 4;
then consider x0 be Real such that
A116: x=x0 & a1<x0 & x0<=a2;
consider y0 be Real such that
A117: x=y0 & b2<y0 & y0<=b1 by A115;
thus thesis by A93,A116,A117,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis by A114;
end;
hence thesis by A111,A112,A113;
end;
then {P1,P2} is a_partition of S3\S4 by A102,A107,EQREL_1:def 4;
hence thesis by A101a;
end;
a1<b1 & a2<b2 & a2<b1 & a1=a2 & b2<b1 & a1<b2 implies
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume
A118: a1<b1 & a2<b2 & a2<b1 & a1=a2 & b2<b1 & a1<b2;
set P={x where x is real number:b2<x & x<=b1};
A119: S3\S4=P
proof
A120: S3\S4 c= {x where x is real number:b2<x & x<=b1}
proof
let y be object;
assume
A121: y in S3\S4;
then reconsider y as real number by A63;
(a1<y & y<=b1) & not (a2<y & y<=b2) by A67,A121;
hence thesis by A118;
end;
{x where x is real number:b2<x & x<=b1} c= S3\S4
proof
let y be object;
assume y in {x where x is real number:b2<x & x<=b1};
then consider y0 be real number such that
A122: y=y0 & b2<y0 & y0<=b1;
(a1<y0 & y0<=b1 ) & (y0<=a2 or b2<y0) by A118,A122,XXREAL_0:2;
hence thesis by A67,A122;
end;
hence thesis by A120;
end;
A123: {P} c= S
proof
let x be object;
assume x in {P}; then
A124: x=P by TARSKI:def 1;
P in {s where s is Subset of REAL:ex a,b be Real st
a<b & for x be real number holds x in s iff (a<x & x<=b)}
proof
A125: P c= REAL
proof
let x be object;
assume x in P;
then consider x0 be real number such that
A126: x=x0 & b2<x0 & x0<=b1;
thus thesis by A126,XREAL_0:def 1;
end;
for x be real number holds x in P iff (b2<x & x<=b1)
proof
for x be real number st x in P holds (b2<x & x<=b1)
proof
let x be real number;
assume x in P;
then consider x0 be real number such that
A126a: x=x0 & b2<x0 & x0<=b1;
thus thesis by A126a;
end;
hence thesis;
end;
hence thesis by A118,A125;
end;
hence thesis by A1,A124,XBOOLE_0:def 3;
end;
{P} is a_partition of P by A55,A119,EQREL_1:39;
hence thesis by A123,A119;
end;
hence thesis by A91,A92,XXREAL_0:1;
end;
A127: a1<b1 & a2<b2 & b1<=b2 & a2<b1 & a2<a1 implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A128: a1<b1 & a2<b2 & b1<=b2 & a2<b1 & a2<a1;
S3\S4 c= {}
proof
let y be object;
assume
A129: y in S3\S4;
then reconsider y as real number by A63;
A130: (a1<y & y<=b1 ) & (y<=a2 or b2<y) by A67,A129;
thus thesis by A128,A130,XXREAL_0:2;
end;
hence thesis by A55;
end;
A131: a1<b1 & a2<b2 & b2<b1 & b2<=a1 & a2<b1 & a2<a1 implies
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume
A132: a1<b1 & a2<b2 & b2<b1 & b2<=a1 & a2<b1 & a2<a1;
S3 c= S3\S4
proof
let x be object;
assume
A133: x in S3;
then reconsider x as real number by A63;
A134: a1<x & x<=b1 by A63,A65,A133;
b2<x by A132,A134,XXREAL_0:2;
hence thesis by A67,A134;
end;
then
A135: S3=S3\S4;
A135a: {S3} c= S
proof
let x be object;
assume x in {S3};
then x is Element of S by TARSKI:def 1;
hence thesis by A2,SUBSET_1:def 1;
end;
{S3} is a_partition of S3 by A55,EQREL_1:39;
hence thesis by A135a,A135;
end;
a1<b1 & a2<b2 & (b2<b1 & a1<b2) & a2<b1 & a2<a1 implies
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume
A137: a1<b1 & a2<b2 & (b2<b1 & a1<b2) & a2<b1 & a2<a1;
set P={x where x is real number:b2<x & x<=b1};
A138: S3\S4=P
proof
A139: S3\S4 c= {x where x is real number:b2<x & x<=b1}
proof
let y be object;
assume
A140: y in S3\S4;
then reconsider y as real number by A63;
(a1<y & y<=b1&y<=a2) or (a1<y & y<=b1&b2<y) by A67,A140;
hence thesis by A137,XXREAL_0:2;
end;
{x where x is real number:b2<x & x<=b1} c= S3\S4
proof
let y be object;
assume y in {x where x is real number:b2<x & x<=b1};
then consider y0 be real number such that
A141: y=y0 & b2<y0 & y0<=b1;
(a1<y0 & y0<=b1 ) & (y0<=a2 or b2<y0) by A137,A141,XXREAL_0:2;
hence thesis by A67,A141;
end;
hence thesis by A139;
end;
A142: {P} c= S
proof
let x be object;
assume x in {P}; then
A143: x=P by TARSKI:def 1;
P in {s where s is Subset of REAL: ex a,b be Real st a<b &
for x be real number holds x in s iff (a<x & x<=b)}
proof
A144: P is Subset of REAL
proof
P c= REAL
proof
let x be object;
assume x in P;
then consider x0 be real number such that
A145: x=x0 & b2<x0 & x0<=b1;
thus thesis by A145,XREAL_0:def 1;
end;
hence thesis;
end;
for x be real number holds x in P iff (b2<x & x<=b1)
proof
for x be real number st x in P holds (b2<x & x<=b1)
proof
let x be real number;
assume x in P;
then consider x0 be real number such that
A146: x=x0 & b2<x0 & x0<=b1;
thus thesis by A146;
end;
hence thesis;
end;
hence thesis by A137,A144;
end;
hence thesis by A1,A143,XBOOLE_0:def 3;
end;
{P} is a_partition of P by A55,A138,EQREL_1:39;
hence thesis by A142,A138;
end;
hence thesis by A65,A66,A69,A74,A90,A127,A131,XXREAL_0:2;
end;
hence thesis by A58,A59,TARSKI:def 1;
end;
hence thesis by SRINGS_1:def 2;
end;
hence thesis by A2,A3;
end;
LemmA1:
II is with_countable_Cover
proof
defpred F[object,object] means
$1 is Element of NAT & $2 in II &
ex x be real number st x=$1 & $2=].-x,x.];
A2: for x be object st x in NAT holds ex y be object st y in II & F[x,y]
proof
let x be object;
assume
A3: x in NAT;
then reconsider x as real number;
set y = ].-x,x.];
y in II & F[x,y] by A3;
hence thesis;
end;
consider f be Function such that
A4: dom f=NAT & rng f c= II and
A5: for x be object st x in NAT holds
F[x,f.x] from FUNCT_1:sch 6(A2);
A6: rng f is Subset-Family of REAL by A4,XBOOLE_1:1;
A7: rng f is countable
proof
reconsider f as SetSequence of REAL by A4,A6,RELSET_1:4,FUNCT_2:def 1;
rng f is countable by TOPGEN_4:58;
hence thesis;
end;
rng f is Cover of REAL
proof
Union f=REAL
proof
thus Union f c= REAL
proof
let x be object;
assume x in Union f;
then consider t be object such that
A9: t in dom f & x in f.t by CARD_5:2;
consider x0 be real number such that
A10: x0=t & f.t=].-x0,x0.] by A4,A5,A9;
thus thesis by A9,A10;
end;
let x be object;
assume x in REAL;
then reconsider x as Real;
consider n be Element of NAT such that
A11: |.x.| <=n by MESFUNC1:8;
A12: n+1 is Element of NAT by ORDINAL1:def 12;
x in f.(n+1)
proof
consider z be real number such that
A13: z=(n+1) & f.(n+1)=].-z,z.] by A5,A12;
A14: -|.x.| <=x & x<=|.x.| & |.x.| <=n by A11,ABSVALUE:4;
A15: x <= n implies x+0 <= n+1 by XREAL_1:7;
-(n+1) < x
proof
per cases;
suppose 0<=x;
hence thesis;
end;
suppose x<0;
then - x <= n by A11,ABSVALUE:def 1; then
A16: - n <= --x by XREAL_1:24; then
A17: -n-1 <= x-1 by XREAL_1:13;
x-1<=x-0 by XREAL_1:13; then
A18: -(n+1) <= x by A17,XXREAL_0:2;
-(n+1) < x
proof
not -(n+1)=x
proof
assume x=-(n+1);
then -n+n<=-(n+1)+n by A16,XREAL_1:7;
hence thesis;
end;
hence thesis by A18,XXREAL_0:1;
end;
hence thesis;
end;
end;
hence thesis by A13,A14,A15,XXREAL_0:2;
end;
then x in f.(n+1) & f.(n+1) in rng f by A4,A12,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
hence thesis by A6,SETFAM_1:45;
end;
hence thesis by A4,A7,SRINGS_1:def 4;
end;
theorem
for S be Subset-Family of REAL
st S = {].a,b.] where a,b is Real: a<=b}
holds S is cap-closed &
S is diff-finite-partition-closed with_empty_element &
S is with_countable_Cover by THS0,THS1,THS2,LemmA1;
LemmB:
for S be Subset-Family of REAL
st S={s where s is Subset of REAL:s is left_open_interval}
holds S is with_countable_Cover
proof
let S be Subset-Family of REAL;
assume
A1: S = {s where s is Subset of REAL:s is left_open_interval};
defpred F[object,object] means
$1 is Element of NAT & $2 in S &
ex x be real number st x=$1 & $2=].-infty,x.];
A2: for x be object st x in NAT holds
ex y be object st y in S & F[x,y]
proof
let x be object;
assume
A3: x in NAT;
then reconsider x as real number;
set y= ].-infty,x.];
A4: y is Subset of REAL & y is left_open_interval by MEASURE5:def 5;
F[x,y] by A1,A3,A4;
hence thesis;
end;
consider f be Function such that
A5: dom f=NAT & rng f c= S and
A6: for x be object st x in NAT holds
F[x,f.x] from FUNCT_1:sch 6(A2);
A7: rng f is Subset-Family of REAL by A5,XBOOLE_1:1;
A8: rng f is countable
proof
reconsider f as SetSequence of REAL by A5,A7,RELSET_1:4,FUNCT_2:def 1;
rng f is countable by TOPGEN_4:58;
hence thesis;
end;
rng f is Cover of REAL
proof
union rng f=REAL
proof
A9: union rng f c= REAL
proof
let x be object;
assume x in union rng f;
then x in Union f;
then consider t be object such that
A10: t in dom f & x in f.t by CARD_5:2;
consider x0 be real number such that
A11: x0=t & f.t=].-infty,x0.] by A5,A6,A10;
thus thesis by A10,A11;
end;
REAL c= union rng f
proof
let x be object;
assume x in REAL;
then reconsider x as Real;
consider n be Element of NAT such that
A12: x<=n by MESFUNC1:8;
x in f.n
proof
ex z be real number st
z=n & f.n=].-infty,z.] by A6;
hence thesis by A12,XXREAL_1:234;
end;
then x in f.n & f.n in rng f by A5,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
hence thesis by A9;
end;
hence thesis by A7,SETFAM_1:45;
end;
hence thesis by A5,A8,SRINGS_1:def 4;
end;
theorem
for S be Subset-Family of REAL
st S = {s where s is Subset of REAL:s is left_open_interval}
holds S is cap-closed &
S is diff-finite-partition-closed with_empty_element &
S is with_countable_Cover
proof
let S be Subset-Family of REAL;
assume
A1: S={s where s is Subset of REAL:s is left_open_interval};
A2: S is cap-closed
proof
for S1,S2 being set st S1 in S & S2 in S holds S1/\S2 in S
proof
let S1,S2 be set;
assume
A3: S1 in S;
assume
A4: S2 in S;
consider s1 be Subset of REAL such that
A5: S1=s1 & s1 is left_open_interval by A1,A3;
consider s2 be Subset of REAL such that
A6: S2=s2 & s2 is left_open_interval by A1,A4;
set S3=s1/\s2;
reconsider S3 as Subset of REAL;
consider a1 being R_eal,b1 being Real such that
A7: s1=].a1,b1.] by MEASURE5:def 5,A5;
consider a2 being R_eal,b2 being Real such that
A8: s2=].a2,b2.] by MEASURE5:def 5,A6;
A9: S3=].max(a1,a2),min(b1,b2).] by A7,A8,XXREAL_1:141;
set m1=max(a1,a2);
m1 in ExtREAL by XXREAL_0:def 1;
then S3 is left_open_interval by A9,MEASURE5:def 5;
hence thesis by A1,A5,A6;
end;
hence thesis by FINSUB_1:def 2;
end;
A10: S is with_empty_element
proof
].0,0.] is left_open_interval
proof
0 in REAL by NUMBERS:19;
hence thesis by NUMBERS:31,MEASURE5:def 5;
end; then
{} in S by A1;
hence thesis;
end;
then
A12: S is non empty;
S is diff-finite-partition-closed
proof
for S3,S4 be Element of S st S3\S4 is non empty
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
let S3,S4 be Element of S;
assume
A13: S3\S4 is non empty;
A14: S3 in S & S4 in S by A12;
consider s3 be Subset of REAL such that
A15: S3=s3 & s3 is left_open_interval by A1,A14;
consider s4 be Subset of REAL such that
A16: S4=s4 & s4 is left_open_interval by A1,A14;
consider a1 be R_eal,b1 be Real such that
A17: s3=].a1,b1.] by A15,MEASURE5:def 5;
consider a2 be R_eal,b2 be Real such that
A18: s4=].a2,b2.] by A16,MEASURE5:def 5;
A20: s4 is empty implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A21: s4 is empty;
set z={S3};
A22: z c= S by A14,TARSKI:def 1;
{S3} is a_partition of S3 by A13,EQREL_1:39;
hence thesis by A22,A16,A21;
end;
A23: (s4 is non empty & s3 misses s4) implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A24: s4 is non empty & s3 misses s4;
A25: S3\S4=S3
proof
S3 c= S3\S4
proof
let x be object;
assume
A27: x in S3;
not x in S4 by A27,A15,A16,A24,XBOOLE_0:def 4;
hence thesis by A27,XBOOLE_0:def 5;
end;
hence thesis;
end;
set z={S3};
A28: z c= S by A14,TARSKI:def 1;
z is a_partition of S3 by A13,EQREL_1:39;
hence thesis by A28,A25;
end;
s4 is non empty & s3 meets s4 implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A29: s4 is non empty & s3 meets s4;
then
A30: ].a1,b1.] \ ].a2,b2.] = ].a1,a2.] \/ ].b2,b1.]
by A17,A18,XXREAL_1:199;
A31: b1<=b2 implies ].a1,a2.] /\ ].b2,b1.] c= {}
proof
assume
A32: b1<=b2;
].b2,b1.]={}
proof
assume ].b2,b1.]<>{};
then consider x be object such that
A33: x in ].b2,b1.] by XBOOLE_0:def 1;
reconsider x as real number by A33;
b2<x & x<=b1 by A33,XXREAL_1:2;
hence thesis by A32,XXREAL_0:2;
end;
hence thesis;
end;
A33a: b2<b1 implies ].a1,a2.] /\ ].b2,b1.] c= {}
proof
assume b2<b1;
].a1,a2.] /\ ].b2,b1.] c= {}
proof
let x be object;
assume
A34: x in ].a1,a2.] /\ ].b2,b1.];
then
A35: x in ].a1,a2.] & x in ].b2,b1.] by XBOOLE_0:def 4;
reconsider x as real number by A34;
per cases;
suppose
A36: a2<=b2;
b2<x & x<=a2 by A35,XXREAL_1:2;
hence thesis by A36,XXREAL_0:2;
end;
suppose
A37: b2<a2;
s4 c= {}
proof
let x be object;
assume
A38: x in s4;
then reconsider x as real number;
a2<x & x<=b2 by A18,A38,XXREAL_1:2;
hence thesis by A37,XXREAL_0:2;
end;
hence thesis by A29;
end;
end;
hence thesis;
end;
A40: a2 in REAL or a2 in {-infty,+infty} by XBOOLE_0:def 3;
A41: a2=+infty implies
ex z be finite Subset of S st
z is a_partition of S3\S4 by A18,A29,XXREAL_1:216;
A42: a2= -infty implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A43: a2=-infty;
A44: S3\S4={}\/].b2,b1.] by A15,A16,A17,A18,A30,A43,XXREAL_1:212;
set z={].b2,b1.]};
A45: z c= S
proof
let x be object;
assume
A47: x in z; then
A48: x=].b2,b1.] by TARSKI:def 1;
reconsider x as Subset of REAL by A47,TARSKI:def 1;
b2 in REAL by XREAL_0:def 1;
then x is left_open_interval by A48,NUMBERS:31,MEASURE5:def 5;
hence thesis by A1;
end;
z is a_partition of S3\S4 by A44,A13,EQREL_1:39;
hence thesis by A45;
end;
A49: a2 in REAL & not(not(a1<a2) & not(b2<b1)) &
not(a1<a2 & b2<b1) implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A50: a2 in REAL;
assume
A51: not(not(a1<a2) & not(b2<b1)) & not(a1<a2 & b2<b1);
A52: a1<a2 & b1<=b2 implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A53: a1<a2 & b1<=b2;
].b2,b1.] c= {}
proof
let x be object;
assume
A54: x in ].b2,b1.];
then reconsider x as real number;
b2<x & x<=b1 by A54,XXREAL_1:2;
hence thesis by A53,XXREAL_0:2;
end; then
A55: ].b2,b1.]={};
set z={].a1,a2.]};
A56: {].a1,a2.]} c= S
proof
let x be object;
assume
A57: x in {].a1,a2.]};
].a1,a2.] in S
proof
set AA=].a1,a2.];
reconsider AA as Subset of REAL by A50,XXREAL_1:227;
AA is left_open_interval by A50,MEASURE5:def 5;
hence thesis by A1;
end;
hence thesis by A57,TARSKI:def 1;
end;
].a1,a2.]<>{}
proof
a2 in ].a1,a2.] by A53;
hence thesis;
end;
then z is a_partition of ].a1,a2.] by EQREL_1:39;
hence thesis by A15,A16,A17,A18,A30,A55,A56;
end;
b2<b1 & a2<=a1 implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A58: b2<b1 & a2<=a1;
].a1,a2.] c= {}
proof
let x be object;
assume
A59: x in ].a1,a2.];
then reconsider x as real number by A50;
a1<x & x<=a2 by A59,XXREAL_1:2;
hence thesis by A58,XXREAL_0:2;
end; then
A60: ].a1,a2.]={};
set z={].b2,b1.]};
A61: {].b2,b1.]} c= S
proof
let x be object;
assume
A62: x in {].b2,b1.]};
].b2,b1.] in S
proof
set AA=].b2,b1.];
reconsider AA as Subset of REAL;
b2 in REAL by XREAL_0:def 1;
then AA is left_open_interval by NUMBERS:31,MEASURE5:def 5;
hence thesis by A1;
end;
hence thesis by A62,TARSKI:def 1;
end;
].b2,b1.]<>{} by A58,XXREAL_1:2;
then z is a_partition of ].b2,b1.] by EQREL_1:39;
hence thesis by A15,A16,A17,A18,A30,A60,A61;
end;
hence thesis by A51,A52;
end;
A63: a2 in REAL & not(a1<a2) & not(b2<b1) implies
ex z be finite Subset of S st
z is a_partition of S3\S4
proof
assume a2 in REAL;
assume
A64: not(a1<a2) & not(b2<b1);
S3\S4 c= {}
proof
let x be object;
assume
A65: x in S3\S4; then
A66: x in ].a1,b1.] & not x in ].a2,b2.]
by A15,A16,A17,A18,XBOOLE_0:def 5;
reconsider x as real number by A15,A65;
a1<x & x<=b1 & (x<=a2 or b2<x) by A66,XXREAL_1:2;
hence thesis by A64,XXREAL_0:2;
end;
hence thesis by A13;
end;
a2 in REAL & a1<a2 & b2<b1 implies
ex z be finite Subset of S st z is a_partition of S3\S4
proof
assume
A67: a2 in REAL;
assume
a1<a2 & b2<b1;
then
A69: ].a1,a2.] <>{} & ].b2,b1.]<>{} by XXREAL_1:2;
set z={].a1,a2.], ].b2,b1.]};
A70: {].a1,a2.], ].b2,b1.]} c= S
proof
let x be object;
assume
A71: x in {].a1,a2.], ].b2,b1.]};
A72: ].a1,a2.] in S
proof
set AA=].a1,a2.];
reconsider AA as Subset of REAL by A67,XXREAL_1:227;
AA is left_open_interval by A67,MEASURE5:def 5;
hence thesis by A1;
end;
].b2,b1.] in S
proof
set BB=].b2,b1.];
reconsider BB as Subset of REAL;
b2 in REAL by XREAL_0:def 1;
then BB is left_open_interval by NUMBERS:31,MEASURE5:def 5;
hence thesis by A1;
end;
hence thesis by A71,A72,TARSKI:def 2;
end;
z is a_partition of ].a1,b1.]\].a2,b2.]
proof
A73: z is Subset-Family of ].a1,b1.]\].a2,b2.]
proof
z c= bool (].a1,b1.]\].a2,b2.])
proof
let x be object;
assume x in z;
then
A74: x=].a1,a2.] or x=].b2,b1.] by TARSKI:def 2;
reconsider x as set by TARSKI:1;
x c= ].a1,b1.]\].a2,b2.]
proof
let y be object;
assume y in x;
then y in ].a1,a2.] \/ ].b2,b1.] by A74,XBOOLE_0:def 3;
hence thesis by A17,A18,A29,XXREAL_1:199;
end;
hence thesis;
end;
hence thesis;
end;
A75: union z = ].a1,b1.]\].a2,b2.] by A30,ZFMISC_1:75;
for A be Subset of ].a1,b1.]\].a2,b2.] st A in z holds A<>{} &
for B be Subset of ].a1,b1.]\].a2,b2.] st B in z holds A=B or
A misses B
proof
let A be Subset of ].a1,b1.]\].a2,b2.];
assume
A76: A in z;
for B be Subset of ].a1,b1.]\].a2,b2.] st B in z holds A=B or
A misses B
proof
let B be Subset of ].a1,b1.]\].a2,b2.];
assume B in z;
then (A=].a1,a2.] & B=].a1,a2.]) or
(A=].a1,a2.] & B=].b2,b1.]) or
(A=].b2,b1.] & B=].a1,a2.]) or
(A=].b2,b1.] & B=].b2,b1.]) by A76,TARSKI:def 2;
hence thesis by A31,A33a;
end;
hence thesis by A69,A76;
end;
hence thesis by A73,A75,EQREL_1:def 4;
end;
hence thesis by A15,A16,A17,A18,A70;
end;
hence thesis by A40,A41,A42,A49,A63,TARSKI:def 2;
end;
hence thesis by A20,A23;
end;
hence thesis by SRINGS_1:def 2;
end;
hence thesis by A1,A2,A10,LemmB;
end;
begin :: Numerical Example
definition
func sring4_8 -> Subset-Family of {1,2,3,4} equals
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}};
coherence
proof
set SF={{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}};
SF c= bool {1,2,3,4}
proof
let x be object;
assume x in SF;
then
S1: x={1,2,3,4} or x={1,2,3} or x={2,3,4} or x={1} or
x={2} or x={3} or x={4} or x={} by ENUMSET1:def 6;
reconsider x as set by TARSKI:1;
S3: {1,2,3} c= {1,2,3,4}
proof
let x be object;
assume x in {1,2,3};
then x=1 or x=2 or x=3 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 2;
end;
S4: {2,3,4} c= {1,2,3,4}
proof
let x be object;
assume x in {2,3,4};
then x=2 or x=3 or x=4 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 2;
end;
S5: {1} c= {1,2,3,4}
proof
let x be object;
assume x in {1};
then x=1 by TARSKI:def 1;
hence thesis by ENUMSET1:def 2;
end;
S6: {2} c= {1,2,3,4}
proof
let x be object;
assume x in {2};
then x=2 by TARSKI:def 1;
hence thesis by ENUMSET1:def 2;
end;
S7: {3} c= {1,2,3,4}
proof
let x be object;
assume x in {3};
then x=3 by TARSKI:def 1;
hence thesis by ENUMSET1:def 2;
end;
S8: {4} c= {1,2,3,4}
proof
let x be object;
assume x in {4};
then x=4 by TARSKI:def 1;
hence thesis by ENUMSET1:def 2;
end;
x c= {1,2,3,4} by S1,S3,S4,S5,S6,S7,S8;
hence thesis;
end;
hence thesis;
end;
end;
set S = sring4_8;
registration
cluster sring4_8 -> with_empty_element;
coherence
proof
{} in S by ENUMSET1:def 6;
hence thesis;
end;
end;
LL2:{1,2,3,4}/\{1,2,3} = {1,2,3}
proof
now
let x be object;
x in {1,2,3,4}/\{1,2,3} iff x in {1,2,3,4} &
x in {1,2,3} by XBOOLE_0:def 4;
then x in {1,2,3,4}/\{1,2,3} iff
x=1 or x=2 or x=3 by ENUMSET1:def 1,ENUMSET1:def 2;
hence x in {1,2,3,4}/\{1,2,3} iff
x in {1,2,3} by ENUMSET1:def 1;
end;
hence thesis by TARSKI:2;
end;
LL3:{1,2,3,4}/\{2,3,4} = {2,3,4}
proof
now
let x be object;
x in {1,2,3,4}/\{2,3,4} iff x in {1,2,3,4} &
x in {2,3,4} by XBOOLE_0:def 4;
then x in {1,2,3,4}/\{2,3,4} iff
x=4 or x=2 or x=3 by ENUMSET1:def 1,ENUMSET1:def 2;
hence x in {1,2,3,4}/\{2,3,4} iff
x in {2,3,4} by ENUMSET1:def 1;
end;
hence thesis by TARSKI:2;
end;
LL4:{1,2,3,4}/\{1} = {1}
proof
now
let x be object;
x in {1,2,3,4}/\{1} iff x in {1,2,3,4} &
x in {1} by XBOOLE_0:def 4;
then x in {1,2,3,4}/\{1} iff
x=1 by TARSKI:def 1,ENUMSET1:def 2;
hence x in {1,2,3,4}/\{1} iff
x in {1} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL5:{1,2,3,4}/\{2} = {2}
proof
now
let x be object;
x in {1,2,3,4}/\{2} iff x in {1,2,3,4} &
x in {2} by XBOOLE_0:def 4;
then x in {1,2,3,4}/\{2} iff
x=2 by TARSKI:def 1,ENUMSET1:def 2;
hence x in {1,2,3,4}/\{2} iff
x in {2} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL6:{1,2,3,4}/\{3} = {3}
proof
now
let x be object;
x in {1,2,3,4}/\{3} iff x in {1,2,3,4} &
x in {3} by XBOOLE_0:def 4;
then x in {1,2,3,4}/\{3} iff
x=3 by TARSKI:def 1,ENUMSET1:def 2;
hence x in {1,2,3,4}/\{3} iff
x in {3} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL7:{1,2,3,4}/\{4} = {4}
proof
now
let x be object;
x in {1,2,3,4}/\{4} iff x in {1,2,3,4} &
x in {4} by XBOOLE_0:def 4;
then x in {1,2,3,4}/\{4} iff
x=4 by TARSKI:def 1,ENUMSET1:def 2;
hence x in {1,2,3,4}/\{4} iff
x in {4} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL10:{1,2,3}/\{2,3,4}={2,3}
proof
now
let x be object;
x in {1,2,3}/\{2,3,4} iff x in {1,2,3} & x in {2,3,4} by XBOOLE_0:def 4;
then x in {1,2,3}/\{2,3,4} iff (x=1 or x=2 or x=3) &
(x=2 or x=3 or x=4) by ENUMSET1:def 1;
hence x in {1,2,3}/\{2,3,4} iff x in {2,3} by TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
LL11:{1,2,3}/\{1} = {1}
proof
now
let x be object;
x in {1,2,3}/\{1} iff x in {1,2,3} &
x in {1} by XBOOLE_0:def 4;
then x in {1,2,3}/\{1} iff
x=1 by TARSKI:def 1,ENUMSET1:def 1;
hence x in {1,2,3}/\{1} iff
x in {1} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL12:{1,2,3}/\{2} = {2}
proof
now
let x be object;
x in {1,2,3}/\{2} iff x in {1,2,3} &
x in {2} by XBOOLE_0:def 4;
then x in {1,2,3}/\{2} iff
x=2 by TARSKI:def 1,ENUMSET1:def 1;
hence x in {1,2,3}/\{2} iff
x in {2} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL13:{1,2,3}/\{3} = {3}
proof
now
let x be object;
x in {1,2,3}/\{3} iff x in {1,2,3} &
x in {3} by XBOOLE_0:def 4;
then x in {1,2,3}/\{3} iff
x=3 by TARSKI:def 1,ENUMSET1:def 1;
hence x in {1,2,3}/\{3} iff x in {3} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL14:{1,2,3}/\{4} = {}
proof
now
let x be object;
x in {1,2,3}/\{4} iff x in {1,2,3} &
x in {4} by XBOOLE_0:def 4;
then x in {1,2,3}/\{4} iff (x=1 or x=2 or x=3) & x=4
by TARSKI:def 1,ENUMSET1:def 1;
hence x in {1,2,3}/\{4} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
LL11a:{2,3,4}/\{1} = {}
proof
now
let x be object;
x in {2,3,4}/\{1} iff x in {2,3,4} &
x in {1} by XBOOLE_0:def 4;
then x in {2,3,4}/\{1} iff (x=2 or x=3 or x=4) & x=1
by TARSKI:def 1,ENUMSET1:def 1;
hence x in {2,3,4}/\{1} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
LL12a:{2,3,4}/\{2} = {2}
proof
now
let x be object;
x in {2,3,4}/\{2} iff x in {2,3,4} &
x in {2} by XBOOLE_0:def 4;
then x in {2,3,4}/\{2} iff
x=2 by TARSKI:def 1,ENUMSET1:def 1;
hence x in {2,3,4}/\{2} iff
x in {2} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL13a:{2,3,4}/\{3} = {3}
proof
now
let x be object;
x in {2,3,4}/\{3} iff x in {2,3,4} &
x in {3} by XBOOLE_0:def 4;
then x in {2,3,4}/\{3} iff
x=3 by TARSKI:def 1,ENUMSET1:def 1;
hence x in {2,3,4}/\{3} iff x in {3} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL14a:{2,3,4}/\{4} = {4}
proof
now
let x be object;
x in {2,3,4}/\{4} iff x in {2,3,4} &
x in {4} by XBOOLE_0:def 4;
then x in {2,3,4}/\{4} iff
x=4 by TARSKI:def 1,ENUMSET1:def 1;
hence x in {2,3,4}/\{4} iff
x in {4} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
LL17:{1}/\{2}={}
proof
now
let x be object;
x in {1}/\{2} iff x in {1} & x in {2} by XBOOLE_0:def 4;
then x in {1}/\{2} iff x=1 & x=2 by TARSKI:def 1;
hence x in {1}/\{2} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
LL18:{1}/\{3}={}
proof
now
let x be object;
x in {1}/\{3} iff x in {1} & x in {3} by XBOOLE_0:def 4;
then x in {1}/\{3} iff x=1 & x=3 by TARSKI:def 1;
hence x in {1}/\{3} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
LL19:{1}/\{4}={}
proof
now
let x be object;
x in {1}/\{4} iff x in {1} & x in {4} by XBOOLE_0:def 4;
then x in {1}/\{4} iff x=1 & x=4 by TARSKI:def 1;
hence x in {1}/\{4} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
LL21:{2}/\{3}={}
proof
now
let x be object;
x in {2}/\{3} iff x in {2} & x in {3} by XBOOLE_0:def 4;
then x in {2}/\{3} iff x=2 & x=3 by TARSKI:def 1;
hence x in {2}/\{3} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
LL22:{2}/\{4}={}
proof
now
let x be object;
x in {2}/\{4} iff x in {2} & x in {4} by XBOOLE_0:def 4;
then x in {2}/\{4} iff x=2 & x=4 by TARSKI:def 1;
hence x in {2}/\{4} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
LL24:{3}/\{4}={}
proof
now
let x be object;
x in {3}/\{4} iff x in {3} & x in {4} by XBOOLE_0:def 4;
then x in {3}/\{4} iff x=3 & x=4 by TARSKI:def 1;
hence x in {3}/\{4} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
Thm1:
INTERSECTION(S,S)=
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}}
proof
T1: INTERSECTION(S,S) c= {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},
{},{2,3}}
proof
let s be object;
assume s in INTERSECTION(S,S);
then consider x,y be set such that
H2: x in S and
H3: y in S and
H4: s=x/\y by SETFAM_1:def 5;
(x= {1,2,3,4} or x={1,2,3} or x={2,3,4} or x={1} or x={2} or
x={3} or x={4} or x={})& (y={1,2,3,4} or y={1,2,3} or y={2,3,4} or
y={1} or y={2} or y={3} or y={4} or y={}) by H2,H3,ENUMSET1:def 6;
hence thesis by LL2,LL3,LL4,LL5,LL6,LL7,LL10,
LL11,LL12,LL13,LL14,LL17,LL18,LL19,LL21,LL22,LL24,
LL11a,LL12a,LL13a,LL14a,H4,ENUMSET1:def 7;
end;
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} c= INTERSECTION(S,S)
proof
let x be object;
assume
B0: x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}};
{1,2,3,4} in S & {1,2,3} in S & {2,3,4} in S & {1} in S &
{2} in S & {3} in S & {4} in S & {} in S by ENUMSET1:def 6;
then {1,2,3,4}/\{1,2,3,4} in INTERSECTION(S,S) &
{1,2,3}/\{1,2,3} in INTERSECTION(S,S) &
{2,3,4}/\{2,3,4} in INTERSECTION(S,S) &
{1}/\{1} in INTERSECTION(S,S) & {2}/\{2} in INTERSECTION(S,S) &
{3}/\{3} in INTERSECTION(S,S) & {4}/\{4} in INTERSECTION(S,S) &
{}/\{} in INTERSECTION(S,S) & {1,2,3}/\{2,3,4} in INTERSECTION(S,S)
by SETFAM_1:def 5;
hence thesis by LL10,B0,ENUMSET1:def 7;
end;
hence thesis by T1;
end;
LemAA:
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}}=
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}}\/{{2,3}}
proof
thus {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} c=
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}}\/{{2,3}}
proof
let x be object;
assume x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}};
then x={1,2,3,4} or x={1,2,3} or x={2,3,4} or x={1} or x= {2} or
x={3} or x={4} or x={} or x={2,3} by ENUMSET1:def 7;
then x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} or x in {{2,3}}
by ENUMSET1:def 6,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}}\/{{2,3}};
then x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} or x in {{2,3}}
by XBOOLE_0:def 3;
then x={1,2,3,4} or x={1,2,3} or x={2,3,4} or
x={1} or x={2} or x={3} or x={4} or x={} or x ={2,3}
by ENUMSET1:def 6,TARSKI:def 1;
hence thesis by ENUMSET1:def 7;
end;
LemmeA:
for x be non empty set st x in sring4_8 holds
{x} is Subset of sring4_8 &
{x} is a_partition of x
proof
let x be non empty set;
assume x in S;
then {x} c= S by TARSKI:def 1;
hence thesis by EQREL_1:39;
end;
Thm98:
for x be set st x in sring4_8 ex P be finite Subset of sring4_8 st
P is a_partition of x
proof
let x be set;
assume
A0: x in S;
per cases;
suppose
C0: x is empty;
{} is Subset of S &
{} is a_partition of {} by SUBSET_1:1,EQREL_1:45;
hence thesis by C0;
end;
suppose x is non empty;
then {x} is Subset of S & {x} is a_partition of x by A0,LemmeA;
hence thesis;
end;
end;
Thm99:
{{2},{3}} is Subset of sring4_8 & {{2},{3}} is a_partition of {2,3}
proof
H1a: {{2},{3}} c= S
proof
let x be object;
assume x in {{2},{3}};
then x ={2} or x={3} by TARSKI:def 2;
hence thesis by ENUMSET1:def 6;
end;
H2: {{2},{3}} is Subset-Family of {2,3}
proof
{{2},{3}} c= bool {2,3}
proof
let x be object;
assume x in {{2},{3}}; then
AAA: x={2} or x={3} by TARSKI:def 2;
{2} c= {2,3} & {3} c= {2,3} by ZFMISC_1:7;
hence thesis by AAA;
end;
hence thesis;
end;
H3: union {{2},{3}}={2,3} by ZFMISC_1:26;
for x be Subset of {2,3} st x in {{2},{3}} holds x<>{} &
for y be Subset of {2,3} st y in {{2},{3}} holds x=y or x misses y
proof
let x be Subset of {2,3};
assume
AA0: x in {{2},{3}};
hence x<>{};
for y be Subset of {2,3} st y in {{2},{3}} holds x=y or x misses y
proof
let y be Subset of {2,3};
assume y in {{2},{3}};
then (y={2} or y={3}) & (x={2} or x={3}) by AA0,TARSKI:def 2;
hence thesis by LL21;
end;
hence thesis;
end;
hence thesis by H1a,H2,H3,EQREL_1:def 4;
end;
LemC:
for x be set st x in INTERSECTION(S,S) ex P be finite Subset of S st
P is a_partition of x
proof
let x be set;
assume x in INTERSECTION(S,S);
then
H2: x in S or x in {{2,3}} by LemAA,Thm1,XBOOLE_0:def 3;
x={2,3} implies ex P be finite Subset of S st P is a_partition of x
by Thm99;
hence thesis by H2,TARSKI:def 1,Thm98;
end;
LemA:
not {1,2,3}/\{2,3,4} in S
proof
A1: {2,3} <> {1,2,3,4}
proof
assume {2,3}={1,2,3,4};
then 1 in {2,3} by ENUMSET1:def 2;
hence thesis by TARSKI:def 2;
end;
A2: {2,3} <> {1,2,3}
proof
assume {2,3}={1,2,3};
then 1 in {2,3} by ENUMSET1:def 1;
hence thesis by TARSKI:def 2;
end;
A3: {2,3} <> {2,3,4}
proof
assume {2,3}={2,3,4};
then 4 in {2,3} by ENUMSET1:def 1;
hence thesis by TARSKI:def 2;
end;
A4: {2,3} <> {1} by ZFMISC_1:5;
A5: {2,3} <> {2} by ZFMISC_1:5;
A6: {2,3} <> {3} by ZFMISC_1:5;
{2,3} <> {4} by ZFMISC_1:5;
hence thesis by LL10,A1,A2,A3,A4,A5,A6,ENUMSET1:def 6;
end;
registration
cluster sring4_8 -> cap-finite-partition-closed non cap-closed;
coherence
proof
sring4_8 is cap-finite-partition-closed
proof
let S1,S2 be Element of sring4_8;
assume
S1/\S2 is non empty;
S1/\S2 in INTERSECTION(sring4_8,sring4_8) by SETFAM_1:def 5;
then consider P be finite Subset of sring4_8 such that
A5: P is a_partition of S1/\S2 by LemC;
take P;
thus thesis by A5;
end;
hence sring4_8 is cap-finite-partition-closed;
assume
H2: S is cap-closed;
{1,2,3} in S & {2,3,4} in S by ENUMSET1:def 6;
hence thesis by LemA,H2,FINSUB_1:def 2;
end;
end;
GG2: {1,2,3,4}\{1,2,3}={4}
proof
thus {1,2,3,4}\{1,2,3} c= {4}
proof
let x be object;
assume x in {1,2,3,4}\{1,2,3};
then x in {1,2,3,4} & not x in {1,2,3} by XBOOLE_0:def 5;
then (x=1 or x=2 or x=3 or x=4) &
not (x=1 or x=2 or x=3) by ENUMSET1:def 1,ENUMSET1:def 2;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {4};
then x=4 by TARSKI:def 1;
then x in {1,2,3,4} & not x in {1,2,3} by ENUMSET1:def 1,ENUMSET1:def 2;
hence thesis by XBOOLE_0:def 5;
end;
GG3:{1,2,3,4}\{2,3,4}={1}
proof
thus {1,2,3,4}\{2,3,4} c= {1}
proof
let x be object;
assume x in {1,2,3,4}\{2,3,4};
then x in {1,2,3,4} & not x in {2,3,4} by XBOOLE_0:def 5;
then (x=1 or x=2 or x=3 or x=4) &
not (x=2 or x=3 or x=4) by ENUMSET1:def 1,ENUMSET1:def 2;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {1};
then x=1 by TARSKI:def 1;
then x in {1,2,3,4} & not x in {2,3,4} by ENUMSET1:def 1,ENUMSET1:def 2;
hence thesis by XBOOLE_0:def 5;
end;
GG4:{1,2,3,4}\{1}={2,3,4}
proof
thus {1,2,3,4}\{1} c= {2,3,4}
proof
let x be object;
assume x in {1,2,3,4}\{1};
then x in {1,2,3,4} & not x in {1} by XBOOLE_0:def 5;
then (x=1 or x=2 or x=3 or x=4) &
not (x=1) by ENUMSET1:def 2,TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
let x be object;
assume x in {2,3,4};
then x=2 or x=3 or x=4 by ENUMSET1:def 1;
then x in {1,2,3,4} & not x in {1} by TARSKI:def 1,ENUMSET1:def 2;
hence thesis by XBOOLE_0:def 5;
end;
GG5:{1,2,3,4}\{2}={1,3,4}
proof
thus {1,2,3,4}\{2} c= {1,3,4}
proof
let x be object;
assume x in {1,2,3,4}\{2};
then x in {1,2,3,4} & not x in {2} by XBOOLE_0:def 5;
then (x=1 or x=2 or x=3 or x=4) &
not (x=2) by ENUMSET1:def 2,TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
let x be object;
assume x in {1,3,4};
then x=1 or x=3 or x=4 by ENUMSET1:def 1;
then x in {1,2,3,4} & not x in {2} by TARSKI:def 1,ENUMSET1:def 2;
hence thesis by XBOOLE_0:def 5;
end;
GG6:{1,2,3,4}\{3}={1,2,4}
proof
thus {1,2,3,4}\{3} c= {1,2,4}
proof
let x be object;
assume x in {1,2,3,4}\{3};
then x in {1,2,3,4} & not x in {3} by XBOOLE_0:def 5;
then (x=1 or x=2 or x=3 or x=4) &
not x=3 by ENUMSET1:def 2,TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
let x be object;
assume x in {1,2,4};
then x=1 or x=2 or x=4 by ENUMSET1:def 1;
then x in {1,2,3,4} & not x in {3} by TARSKI:def 1,ENUMSET1:def 2;
hence thesis by XBOOLE_0:def 5;
end;
GG7:{1,2,3,4}\{4}={1,2,3}
proof
thus {1,2,3,4}\{4} c= {1,2,3}
proof
let x be object;
assume x in {1,2,3,4}\{4};
then x in {1,2,3,4} & not x in {4} by XBOOLE_0:def 5;
then (x=1 or x=2 or x=3 or x=4) &
not x=4 by ENUMSET1:def 2,TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
let x be object;
assume x in {1,2,3};
then x=1 or x=2 or x=3 by ENUMSET1:def 1;
then x in {1,2,3,4} & not x in {4} by TARSKI:def 1,ENUMSET1:def 2;
hence thesis by XBOOLE_0:def 5;
end;
GG11:{1,2,3}\{2,3,4}={1}
proof
thus {1,2,3}\{2,3,4} c= {1}
proof
let x be object;
assume x in {1,2,3}\{2,3,4};
then x in {1,2,3} & not x in {2,3,4} by XBOOLE_0:def 5;
then (x=1 or x=2 or x=3) &
not (x=2 or x=3 or x=4) by ENUMSET1:def 1;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {1};
then x=1 by TARSKI:def 1;
then x in {1,2,3} & not x in {2,3,4} by ENUMSET1:def 1;
hence thesis by XBOOLE_0:def 5;
end;
GG12:{1,2,3}\{1}={2,3}
proof
now
let x be object;
x in {1,2,3}\{1} iff x in {1,2,3} & not x in {1} by XBOOLE_0:def 5;
then x in {1,2,3}\{1} iff (x=1 or x=2 or x=3) & not x=1
by ENUMSET1:def 1,TARSKI:def 1;
hence x in {1,2,3}\{1} iff x in {2,3} by TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
GG13:{1,2,3}\{2}={1,3}
proof
now
let x be object;
x in {1,2,3}\{2} iff x in {1,2,3} & not x in {2} by XBOOLE_0:def 5;
then x in {1,2,3}\{2} iff (x=1 or x=2 or x=3) & not x=2
by ENUMSET1:def 1,TARSKI:def 1;
hence x in {1,2,3}\{2} iff x in {1,3} by TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
GG14:{1,2,3}\{3}={1,2}
proof
now
let x be object;
x in {1,2,3}\{3} iff x in {1,2,3} & not x in {3} by XBOOLE_0:def 5;
then x in {1,2,3}\{3} iff (x=1 or x=2 or x=3) & not x=3
by ENUMSET1:def 1,TARSKI:def 1;
hence x in {1,2,3}\{3} iff x in {1,2} by TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
GG15:{1,2,3}\{4}={1,2,3}
proof
now
let x be object;
x in {1,2,3}\{4} iff x in {1,2,3} & not x in {4} by XBOOLE_0:def 5;
then x in {1,2,3}\{4} iff (x=1 or x=2 or x=3) & not x=4
by ENUMSET1:def 1,TARSKI:def 1;
hence x in {1,2,3}\{4} iff x in {1,2,3} by ENUMSET1:def 1;
end;
hence thesis by TARSKI:2;
end;
GG18:{2,3,4}\{1,2,3}={4}
proof
now
let x be object;
x in {2,3,4}\{1,2,3} iff x in {2,3,4} & not x in {1,2,3} by XBOOLE_0:def 5;
then x in {2,3,4}\{1,2,3} iff (x=2 or x=3 or x=4) & not (x=1 or x=2 or x=3)
by ENUMSET1:def 1;
hence x in {2,3,4}\{1,2,3} iff x in {4} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
GG20:{2,3,4}\{1}={2,3,4}
proof
now
let x be object;
x in {2,3,4}\{1} iff x in {2,3,4} & not x in {1} by XBOOLE_0:def 5;
then x in {2,3,4}\{1} iff (x=2 or x=3 or x=4) & not x=1
by ENUMSET1:def 1,TARSKI:def 1;
hence x in {2,3,4}\{1} iff x in {2,3,4} by ENUMSET1:def 1;
end;
hence thesis by TARSKI:2;
end;
GG21:{2,3,4}\{2}={3,4}
proof
now
let x be object;
x in {2,3,4}\{2} iff x in {2,3,4} & not x in {2} by XBOOLE_0:def 5;
then x in {2,3,4}\{2} iff (x=2 or x=3 or x=4) & not x=2
by ENUMSET1:def 1,TARSKI:def 1;
hence x in {2,3,4}\{2} iff x in {3,4} by TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
GG22:{2,3,4}\{3}={2,4}
proof
now
let x be object;
x in {2,3,4}\{3} iff x in {2,3,4} & not x in {3} by XBOOLE_0:def 5;
then x in {2,3,4}\{3} iff (x=2 or x=3 or x=4) & not x=3
by ENUMSET1:def 1,TARSKI:def 1;
hence x in {2,3,4}\{3} iff x in {2,4} by TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
GG23:{2,3,4}\{4}={2,3}
proof
now
let x be object;
x in {2,3,4}\{4} iff x in {2,3,4} & not x in {4} by XBOOLE_0:def 5;
then x in {2,3,4}\{4} iff (x=2 or x=3 or x=4) & not x=4
by ENUMSET1:def 1,TARSKI:def 1;
hence x in {2,3,4}\{4} iff x in {2,3} by TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
GG27:{1}\{2,3,4}={1}
proof
now
let x be object;
x in {1}\{2,3,4} iff x in {1} & not x in {2,3,4} by XBOOLE_0:def 5;
then x in {1}\{2,3,4} iff x=1 & not (x=2 or x=3 or x=4)
by TARSKI:def 1,ENUMSET1:def 1;
hence x in {1}\{2,3,4} iff x in {1} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
GG33:{2}\{1,2,3,4}={}
proof
now
let x be object;
x in {2}\{1,2,3,4} iff x in {2} & not x in {1,2,3,4} by XBOOLE_0:def 5;
then x in {2}\{1,2,3,4} iff x=2 & not (x=1 or x=2 or x=3 or x=4)
by TARSKI:def 1,ENUMSET1:def 2;
hence x in {2}\{1,2,3,4} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
GG34:{2}\{1,2,3}={}
proof
now
let x be object;
x in {2}\{1,2,3} iff x in {2} & not x in {1,2,3} by XBOOLE_0:def 5;
then x in {2}\{1,2,3} iff x=2 & not (x=1 or x=2 or x=3)
by TARSKI:def 1,ENUMSET1:def 1;
hence x in {2}\{1,2,3} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
GG35:{2}\{2,3,4}={}
proof
now
let x be object;
x in {2}\{2,3,4} iff x in {2} & not x in {2,3,4} by XBOOLE_0:def 5;
then x in {2}\{2,3,4} iff x=2 & not (x=2 or x=3 or x=4)
by TARSKI:def 1,ENUMSET1:def 1;
hence x in {2}\{2,3,4} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
GG41:{3}\{1,2,3,4}={}
proof
now
let x be object;
x in {3}\{1,2,3,4} iff x in {3} & not x in {1,2,3,4} by XBOOLE_0:def 5;
then x in {3}\{1,2,3,4} iff x=3 & not (x=1 or x=2 or x=3 or x=4)
by TARSKI:def 1,ENUMSET1:def 2;
hence x in {3}\{1,2,3,4} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
GG42:{3}\{1,2,3}={}
proof
now
let x be object;
x in {3}\{1,2,3} iff x in {3} & not x in {1,2,3} by XBOOLE_0:def 5;
then x in {3}\{1,2,3} iff x=3 & not (x=1 or x=2 or x=3)
by TARSKI:def 1,ENUMSET1:def 1;
hence x in {3}\{1,2,3} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
GG43:{3}\{2,3,4}={}
proof
now
let x be object;
x in {3}\{2,3,4} iff x in {3} & not x in {2,3,4} by XBOOLE_0:def 5;
then x in {3}\{2,3,4} iff x=3 & not (x=2 or x=3 or x=4)
by TARSKI:def 1,ENUMSET1:def 1;
hence x in {3}\{2,3,4} iff contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
GG50:{4}\{1,2,3}={4}
proof
now
let x be object;
x in {4}\{1,2,3} iff x in {4} & not x in {1,2,3} by XBOOLE_0:def 5;
then x in {4}\{1,2,3} iff x=4 & not (x=1 or x=2 or x=3)
by TARSKI:def 1,ENUMSET1:def 1;
hence x in {4}\{1,2,3} iff x in {4} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
Thm50:
DIFFERENCE(sring4_8,sring4_8) =
sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}
proof
thus DIFFERENCE(S,S) c=
S \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}
proof
let s be object;
assume s in DIFFERENCE(S,S);
then consider x,y be set such that
A1: x in S & y in S and
A2: s=x\y by SETFAM_1:def 6;
(x= {1,2,3,4} or x={1,2,3} or x={2,3,4} or x={1} or x={2} or
x={3} or x={4} or x={})& (y={1,2,3,4} or
y={1,2,3} or y={2,3,4} or y={1} or y={2} or
y={3} or y={4} or y={}) by A1,ENUMSET1:def 6; then
s={1,2,3,4} or s={1,2,3} or s={2,3,4} or s={1} or s={2} or s={3} or
s={4} or
s={} or s={1,3,4} or s={1,2,4} or s={2,3} or s={1,3} or s={1,2} or
s={3,4} or s={2,4} or s={2,3} or s={}
by GG2,GG3,GG4,GG5,GG6,GG7,XBOOLE_1:37,
GG11,GG12,GG13,GG14,GG15,GG18,GG20,
GG21,GG22,GG23,GG27,ZFMISC_1:14,
GG33,GG34,GG35,GG41,GG42,GG43,GG50,A2;
then s in S or s in {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}
by ENUMSET1:def 6,def 5;
hence thesis by XBOOLE_0:def 3;
end;
let s be object;
assume s in S \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}};
then s in S or
s in {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} by XBOOLE_0:def 3;
then
VU: s={1,2,3,4}\{} or s={1,2,3}\{} or s={2,3,4}\{} or s={1}\{} or
s={2}\{} or s={3}\{} or
s={4}\{} or s={}\{} or
s={1}\{1} or s={1,2,3,4}\{2} or s={1,2,3,4}\{3} or s={1,2,3}\{1} or
s={1,2,3}\{2} or s={1,2,3}\{3} or s={2,3,4}\{2} or
s={1,2,3}\{2,3,4} or s={2,3,4}\{3} or s={1,2,3}\{1}
by GG5,GG6,GG12,GG13,GG14,
GG21,GG22,ENUMSET1:def 6,ENUMSET1:def 5;
{1,2,3,4} in S & {1,2,3} in S & {2,3,4} in S & {1} in S &
{2} in S & {3} in S & {4} in S & {} in S by ENUMSET1:def 6;
hence thesis by VU,SETFAM_1:def 6;
end;
ThmV1:
{{1},{3}} is Subset of sring4_8 & {{1},{3}} is a_partition of {1,3}
proof
H1a: {{1},{3}} c= S
proof
let x be object;
assume x in {{1},{3}};
then x ={1} or x={3} by TARSKI:def 2;
hence thesis by ENUMSET1:def 6;
end;
H2: {{1},{3}} is Subset-Family of {1,3}
proof
{{1},{3}} c= bool {1,3}
proof
let x be object;
assume x in {{1},{3}}; then
AAA: x={1} or x={3} by TARSKI:def 2;
{1} c= {1,3} & {3} c= {1,3} by ZFMISC_1:7;
hence thesis by AAA;
end;
hence thesis;
end;
H3: union {{1},{3}}={1,3} by ZFMISC_1:26;
for x be Subset of {1,3} st x in {{1},{3}} holds x<>{} &
for y be Subset of {1,3} st y in {{1},{3}} holds x=y or x misses y
proof
let x be Subset of {1,3};
assume
AA0: x in {{1},{3}};
hence x<>{};
for y be Subset of {1,3} st y in {{1},{3}} holds x=y or x misses y
proof
let y be Subset of {1,3};
assume y in {{1},{3}};
then (y={1} or y={3}) & (x={1} or x={3}) by AA0,TARSKI:def 2;
hence thesis by LL18;
end;
hence thesis;
end;
hence thesis by H1a,H2,H3,EQREL_1:def 4;
end;
ThmV2:
{{1},{2}} is Subset of sring4_8 & {{1},{2}} is a_partition of {1,2}
proof
H1a: {{1},{2}} c= S
proof
let x be object;
assume x in {{1},{2}};
then x ={1} or x={2} by TARSKI:def 2;
hence thesis by ENUMSET1:def 6;
end;
H2: {{1},{2}} is Subset-Family of {1,2}
proof
{{1},{2}} c= bool {1,2}
proof
let x be object;
assume x in {{1},{2}};
then
AAA: x={1} or x={2} by TARSKI:def 2;
{1} c= {1,2} & {2} c= {1,2} by ZFMISC_1:7;
hence thesis by AAA;
end;
hence thesis;
end;
H3: union {{1},{2}}={1,2} by ZFMISC_1:26;
for x be Subset of {1,2} st x in {{1},{2}} holds x<>{} &
for y be Subset of {1,2} st y in {{1},{2}} holds x=y or x misses y
proof
let x be Subset of {1,2};
assume
AA0: x in {{1},{2}};
hence x<>{};
for y be Subset of {1,2} st y in {{1},{2}} holds x=y or x misses y
proof
let y be Subset of {1,2};
assume y in {{1},{2}};
then (y={1} or y={2}) & (x={1} or x={2}) by AA0,TARSKI:def 2;
hence thesis by LL17;
end;
hence thesis;
end;
hence thesis by H1a,H2,H3,EQREL_1:def 4;
end;
ThmV3:
{{2},{4}} is Subset of sring4_8 & {{2},{4}} is a_partition of {2,4}
proof
H1a: {{2},{4}} c= S
proof
let x be object;
assume x in {{2},{4}};
then x ={2} or x={4} by TARSKI:def 2;
hence thesis by ENUMSET1:def 6;
end;
H2: {{2},{4}} is Subset-Family of {2,4}
proof
{{2},{4}} c= bool {2,4}
proof
let x be object;
assume x in {{2},{4}}; then
AAA: x={2} or x={4} by TARSKI:def 2;
{2} c= {2,4} & {4} c= {2,4} by ZFMISC_1:7;
hence thesis by AAA;
end;
hence thesis;
end;
H3: union {{2},{4}}={2,4} by ZFMISC_1:26;
for x be Subset of {2,4} st x in {{2},{4}} holds x<>{} &
for y be Subset of {2,4} st y in {{2},{4}} holds x=y or x misses y
proof
let x be Subset of {2,4};
assume
AA0: x in {{2},{4}};
hence x<>{};
for y be Subset of {2,4} st y in {{2},{4}} holds x=y or x misses y
proof
let y be Subset of {2,4};
assume y in {{2},{4}};
then (y={2} or y={4}) & (x={2} or x={4}) by AA0,TARSKI:def 2;
hence thesis by LL22;
end;
hence thesis;
end;
hence thesis by H1a,H2,H3,EQREL_1:def 4;
end;
ThmV4:
{{3},{4}} is Subset of sring4_8 & {{3},{4}} is a_partition of {3,4}
proof
H1a: {{3},{4}} c= S
proof
let x be object;
assume x in {{3},{4}};
then x ={3} or x={4} by TARSKI:def 2;
hence thesis by ENUMSET1:def 6;
end;
H2: {{3},{4}} is Subset-Family of {3,4}
proof
{{3},{4}} c= bool {3,4}
proof
let x be object;
assume x in {{3},{4}};
then
AAA: x={3} or x={4} by TARSKI:def 2;
{3} c= {3,4} & {4} c= {3,4} by ZFMISC_1:7;
hence thesis by AAA;
end;
hence thesis;
end;
H3: union {{3},{4}}={3,4} by ZFMISC_1:26;
for x be Subset of {3,4} st x in {{3},{4}} holds x<>{} &
for y be Subset of {3,4} st y in {{3},{4}} holds x=y or x misses y
proof
let x be Subset of {3,4};
assume
AA0: x in {{3},{4}};
hence x<>{};
for y be Subset of {3,4} st y in {{3},{4}} holds x=y or x misses y
proof
let y be Subset of {3,4};
assume y in {{3},{4}};
then (y={3} or y={4}) & (x={3} or x={4}) by AA0,TARSKI:def 2;
hence thesis by LL24;
end;
hence thesis;
end;
hence thesis by H1a,H2,H3,EQREL_1:def 4;
end;
ThmV5:
{{1},{3},{4}} is Subset of sring4_8 &
{{1},{3},{4}} is a_partition of {1,3,4}
proof
H1a: {{1},{3},{4}} c= S
proof
let x be object;
assume x in {{1},{3},{4}};
then x={1} or x={3} or x={4} by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 6;
end;
H2: {{1},{3},{4}} is Subset-Family of {1,3,4}
proof
{{1},{3},{4}} c= bool {1,3,4}
proof
let x be object;
assume x in {{1},{3},{4}};
then
AAA: x={1} or x={3} or x={4} by ENUMSET1:def 1;
{1} c= {1,3,4} & {3} c= {1,3,4} & {4} c= {1,3,4}
proof
thus {1} c= {1,3,4}
proof
let x be object;
assume x in {1};
then x=1 by TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
thus {3} c= {1,3,4}
proof
let x be object;
assume x in {3};
then x=3 by TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
let x be object;
assume x in {4};
then x = 4 by TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
hence thesis by AAA;
end;
hence thesis;
end;
H3: union {{1},{3},{4}}={1,3,4}
proof
T1: union {{1}} = {1} & union {{3},{4}}={3,4}
by ZFMISC_1:26;
T1A: union {{1},{3},{4}}=union ({{1}}\/{{3},{4}}) by ENUMSET1:2;
{1}\/{3,4}={1,3,4} by ENUMSET1:2;
hence thesis by T1,T1A,ZFMISC_1:78;
end;
for x be Subset of {1,3,4} st x in {{1},{3},{4}} holds x<>{} &
for y be Subset of {1,3,4} st y in {{1},{3},{4}} holds x=y or x misses y
proof
let x be Subset of {1,3,4};
assume
AA0: x in {{1},{3},{4}};
hence x<>{};
for y be Subset of {1,3,4} st y in {{1},{3},{4}} holds x=y or x misses y
proof
let y be Subset of {1,3,4};
assume y in {{1},{3},{4}};
then (y={1} or y={3} or y={4}) & (x={1} or x={3} or x={4})
by AA0,ENUMSET1:def 1;
hence thesis by LL18,LL19,LL24;
end;
hence thesis;
end;
hence thesis by H1a,H2,H3,EQREL_1:def 4;
end;
ThmV6:
{{1},{2},{4}} is Subset of sring4_8 &
{{1},{2},{4}} is a_partition of {1,2,4}
proof
H1a: {{1},{2},{4}} c= S
proof
let x be object;
assume x in {{1},{2},{4}};
then x={1} or x={2} or x={4} by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 6;
end;
H2: {{1},{2},{4}} is Subset-Family of {1,2,4}
proof
{{1},{2},{4}} c= bool {1,2,4}
proof
let x be object;
assume x in {{1},{2},{4}}; then
AAA: x={1} or x={2} or x={4} by ENUMSET1:def 1;
{1} c= {1,2,4} & {2} c= {1,2,4} & {4} c= {1,2,4}
proof
thus {1} c= {1,2,4}
proof
let x be object;
assume x in {1};
then x=1 by TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
thus {2} c={1,2,4}
proof
let x be object;
assume x in {2};
then x=2 by TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
let x be object;
assume x in {4};
then x = 4 by TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
hence thesis by AAA;
end;
hence thesis;
end;
H3: union {{1},{2},{4}}={1,2,4}
proof
T1: union {{1}} = {1} & union {{2},{4}}={2,4} by ZFMISC_1:26;
T1A: {{1},{2},{4}}={{1}}\/{{2},{4}} by ENUMSET1:2;
{1}\/{2,4}={1,2,4} by ENUMSET1:2;
hence thesis by T1,T1A,ZFMISC_1:78;
end;
for x be Subset of {1,2,4} st x in {{1},{2},{4}} holds x<>{} &
for y be Subset of {1,2,4} st y in {{1},{2},{4}} holds x=y or x misses y
proof
let x be Subset of {1,2,4};
assume
AA0: x in {{1},{2},{4}};
hence x<>{};
for y be Subset of {1,2,4} st y in {{1},{2},{4}} holds x=y or x misses y
proof
let y be Subset of {1,2,4};
assume y in {{1},{2},{4}};
then (y={1} or y={2} or y={4}) & (x={1} or x={2} or x={4})
by AA0,ENUMSET1:def 1;
hence thesis by LL17,LL19,LL22;
end;
hence thesis;
end;
hence thesis by H1a,H2,H3,EQREL_1:def 4;
end;
LemD:
for x be set st x in DIFFERENCE(S,S) ex P be finite Subset of S st
P is a_partition of x
proof
let x be set;
assume x in DIFFERENCE(S,S); then
x in S or x in {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}
by Thm50,XBOOLE_0:def 3;
then per cases by ENUMSET1:def 5;
suppose x in S;
hence thesis by Thm98;
end;
suppose x={2,3};
hence thesis by Thm99;
end;
suppose x={1,3};
hence thesis by ThmV1;
end;
suppose x={1,2};
hence thesis by ThmV2;
end;
suppose x={3,4};
hence thesis by ThmV4;
end;
suppose x={2,4};
hence thesis by ThmV3;
end;
suppose x={1,3,4};
hence thesis by ThmV5;
end;
suppose x={1,2,4};
hence thesis by ThmV6;
end;
end;
registration
cluster sring4_8 -> diff-finite-partition-closed;
coherence
proof
for y,z be Element of sring4_8 st y\z is non empty holds
ex P be finite Subset of sring4_8 st P is a_partition of y\z
proof
let y,z be Element of sring4_8;
assume y\z is non empty;
y\z in DIFFERENCE(sring4_8,sring4_8) by SETFAM_1:def 6;
hence thesis by LemD;
end;
hence thesis by SRINGS_1:def 2;
end;
end;