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