srings_2.miz
begin
reserve X for
set;
reserve S for
Subset-Family of X;
theorem ::
SRINGS_2:1
for X1,X2 be
set, S1 be
Subset-Family of X1, S2 be
Subset-Family of X2 holds {
[:a, b:] where a be
Element of S1, b be
Element of S2 : a
in S1 & b
in S2 }
= { s where s be
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 be
Element of S1, b be
Element of S2 : a
in S1 & b
in S2 }
c= { s where s be
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 be
Element of S1, b be
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 be
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 ::
SRINGS_2:2
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 be
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 be
Element of S1, x2 be
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 be
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 be
Element of S1, x2 be
Element of S2
proof
let x be
object;
assume x
in { s where s be
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 be
Element of S1, x2 be
Element of S2 holds x
in { s where s be
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 be
Element of S1, x2 be
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 ::
SRINGS_2:3
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 be
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 be
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 be
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 be
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,
XBOOLE_0: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,
SETFAM_1:def 8,
A2,
SRINGS_1:def 4,
PROB_1: 4;
end;
end
begin
theorem ::
SRINGS_2:4
for F be
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;
coherence ;
end
theorem ::
SRINGS_2:5
(
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 be
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 be
Subset of D : y is
finite } implies SD
= (
Fin D)
proof
assume
A1: SD
= { y where y be
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 be
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 be
Subset of D : y is
finite };
{ y where y be
Subset of D : y is
finite }
c= SD
proof
let x be
object;
assume x
in { y where y be
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;
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;
coherence
proof
let SD be
Subset-Family of D;
assume SD
= (
Fin D);
then
A1: SD
= { y where y be
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 be
set such that
A2: for y be
object holds y
in XX iff y
in (
bool D) &
P[y] from
XBOOLE_0:sch 1;
for x be
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 be
set such that
A12: for z be
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 holds ex xx be
object st xx
in XX &
[c, xx]
in Z) & (for xx be
object st xx
in XX holds 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 holds 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 holds 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 ::
SRINGS_2:6
(
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 be
Element of S1, b be
Element of S2 : a
in (S1
\
{
{} }) & b
in (S2
\
{
{} }) }
= { s where s be
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 be
Element of S1, b be
Element of S2 : a
in (S1
\
{
{} }) & b
in (S2
\
{
{} }) }
c= { s where s be
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 be
Element of S1, b be
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 be
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 be
Element of (S1
\
{
{} }), b be
Element of (S2
\
{
{} }) : a
in (S1
\
{
{} }) & b
in (S2
\
{
{} }) } iff x
in {
[:a, b:] where a be
Element of S1, b be
Element of S2 : a
in (S1
\
{
{} }) & b
in (S2
\
{
{} }) }
proof
let x,S1,S2 be
set;
x
in {
[:a, b:] where a be
Element of (S1
\
{
{} }), b be
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 be
Element of (S1
\
{
{} }), b be
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 be
Element of (S1
\
{
{} }), b be
Element of (S2
\
{
{} }) : a
in (S1
\
{
{} }) & b
in (S2
\
{
{} }) }
= {
[:a, b:] where a be
Element of S1, b be
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 be
Element of (S1
\
{
{} }), b be
Element of (S2
\
{
{} }) : a
in (S1
\
{
{} }) & b
in (S2
\
{
{} }) } iff x0
in {
[:a, b:] where a be
Element of S1, b be
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 ::
SRINGS_2:7
for X1,X2 be
set, S1 be
semiring_of_sets of X1, S2 be
semiring_of_sets of X2 holds { s where s be
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 be
set st A
= ($2
`1 ) & B
= ($2
`2 ) & $1
=
[:A, B:];
set Y = { s where s be
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 be
Element of y1, b be
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 be
Element of y1, b be
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 be
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 be
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 be
set st A
= $2 & $1
=
[:A, x12:];
A57: for x be
object st x
in Z1 holds 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 be
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 be
Element of z1, q be
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 be
Element of z1, u2 be
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 be
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 ::
SRINGS_2:8
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 be
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 be
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 be
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 be
Element of U1, b be
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 be
Element of U1, u2 be
Element of U2 : u1
in (U1
\
{
{} }) & u2
in (U2
\
{
{} }) };
A14: (for v be
object st v
in V holds ex w be
object st w
in W &
[v, w]
in Z) & (for w be
object st w
in W holds 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 holds 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 holds 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 holds ex w be
object st w
in W &
[v, w]
in Z) & (for w be
object st w
in W holds 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 be
Element of (U1
\
{
{} }), b be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 holds 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 be
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 be
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 be
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 be
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 be
real
number : a1
< x & x
<= a2 };
A80: (S3
\ S4)
= P
proof
A81: (S3
\ S4)
c= { x where x be
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 be
real
number : a1
< x & x
<= a2 }
c= (S3
\ S4)
proof
let y be
object;
assume y
in { x where x be
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 be
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 be
Real : a1
< x & x
<= a2 };
A94: P1
in S
proof
P1
in { s where s be
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 be
Real : b2
< x & x
<= b1 };
A98: P2
in S
proof
P2
in { s where s be
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 be
real
number : b2
< x & x
<= b1 };
A119: (S3
\ S4)
= P
proof
A120: (S3
\ S4)
c= { x where x be
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 be
real
number : b2
< x & x
<= b1 }
c= (S3
\ S4)
proof
let y be
object;
assume y
in { x where x be
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 be
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 be
real
number : b2
< x & x
<= b1 };
A138: (S3
\ S4)
= P
proof
A139: (S3
\ S4)
c= { x where x be
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 be
real
number : b2
< x & x
<= b1 }
c= (S3
\ S4)
proof
let y be
object;
assume y
in { x where x be
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 be
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 ::
SRINGS_2:9
for S be
Subset-Family of
REAL st S
= {
].a, b.] where a,b be
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 be
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 be
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 ::
SRINGS_2:10
for S be
Subset-Family of
REAL st S
= { s where s be
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 be
Subset of
REAL : s is
left_open_interval };
A2: S is
cap-closed
proof
for S1,S2 be
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 be
R_eal, b1 be
Real such that
A7: s1
=
].a1, b1.] by
MEASURE5:def 5,
A5;
consider a2 be
R_eal, b2 be
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 holds 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
definition
::
SRINGS_2:def1
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 holds 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)) holds 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,
ENUMSET1: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)) holds 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;
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