:: Semiring of Sets: Examples
:: by Roland Coghetto
::
:: Received March 31, 2014
:: Copyright (c) 2014 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_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
proof
Fin X c= bool X by FINSUB_1:13;
then Fin X is Subset-Family of X;
hence thesis;
end;
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**{} &
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{};
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{}
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{} 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{} & ].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;
**