let X be set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X
for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A
let S be cap-finite-partition-closed Subset-Family of X; :: thesis: for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A
let A be Element of S; :: thesis: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A
set B = { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } ;

per cases ( A is empty or not A is empty ) ;

suppose H0: A is empty ; :: thesis: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A

T1: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } c= {}

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } or t in {} )
assume t in { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } ; :: thesis: t in {}
then consider t0 being Element of S such that
t = t0 and
ZE2: t0 in union ((PARTITIONS A) /\ (Fin S)) ;
consider u0 being 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 t in {} by ZE3, TARSKI:def 1; :: thesis: verum

end;

{} is Subset-Family of {} by XBOOLE_1:2;
then reconsider B = { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } as Subset-Family of {} by T1;
for a, b being Element of B st not a /\ b is empty holds
ex P being finite Subset of B st P is a_partition of a /\ b

proof

let a, b be Element of B; :: thesis: ( not a /\ b is empty implies ex P being finite Subset of B st P is a_partition of a /\ b )
assume VA: not a /\ b is empty ; :: thesis: ex P being finite Subset of B st P is a_partition of a /\ b
( a = {} & b = {} ) by T1, SUBSET_1:def 1;
hence ex P being finite Subset of B st P is a_partition of a /\ b by VA; :: thesis: verum

end;

hence { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A by H0, Defcap; :: thesis: verum

end;

suppose H1: not A is empty ; :: thesis: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A

AA: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } c= bool A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } or x in bool A )
assume x in { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } ; :: thesis: x in bool A
then consider x0 being Element of S such that
B1: x = x0 and
B2: x0 in union ((PARTITIONS A) /\ (Fin S)) ;
consider x1 being 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; :: thesis: verum

end;

per cases ( { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is empty or not { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is empty ) ;

suppose U0: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is empty ; :: thesis: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A

then reconsider B = { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } as Subset-Family of A by XBOOLE_1:2;
B is cap-finite-partition-closed by U0;
hence { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A ; :: thesis: verum

end;

suppose not { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is empty ; :: thesis: { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A

then reconsider B = { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } as non empty set ;
for x, y being Element of B st not x /\ y is empty holds
ex P being finite Subset of B st P is a_partition of x /\ y

proof

let x, y be Element of B; :: thesis: ( not x /\ y is empty implies ex P being finite Subset of B st P is a_partition of x /\ y )
assume V1: not x /\ y is empty ; :: thesis: ex P being finite Subset of B st P is a_partition of x /\ y
x in B ;
then consider x0 being Element of S such that
A1: x = x0 and
A2: x0 in union ((PARTITIONS A) /\ (Fin S)) ;
consider x1 being 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 being Element of S such that
A3: y = y0 and
A4: y0 in union ((PARTITIONS A) /\ (Fin S)) ;
consider y1 being 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 = A as non empty set by H1;
reconsider x1 = x1 as a_partition of A by C4a, PARTIT1:def 3;
reconsider y1 = y1 as a_partition of A by C4a, PARTIT1:def 3;
consider P being a_partition of A such that
D1: P is finite Subset of S and
D2: P '<' x1 '/\' y1 by C5, ThmJ1;
consider P1 being 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 ; :: according to TARSKI:def 3 :: thesis: ( not d in P1 or d in B )
assume UP: d in P1 ; :: thesis: d in B
UJ: ( x0 in x1 & x1 is a_partition of A ) by C1;
KK2: x /\ y c= A by A1, UJ, XBOOLE_1:108;
set PP = { p where p is Element of P : p misses x /\ y } \/ P1;
GH2: { p where p is Element of P : p misses x /\ y } \/ P1 is finite Subset of S

proof

GHAA: { p where p is Element of P : p misses x /\ y } \/ P1 c= P \/ P1

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { p where p is Element of P : p misses x /\ y } \/ P1 or z in P \/ P1 )
assume z in { p where p is Element of P : p misses x /\ y } \/ P1 ; :: thesis: z in P \/ P1
then UU: ( z in { p where p is Element of P : p misses x /\ y } or z in P1 ) by XBOOLE_0:def 3;
{ p where p is Element of P : p misses x /\ y } c= P

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { p where p is Element of P : p misses x /\ y } or a in P )
assume a in { p where p is Element of P : p misses x /\ y } ; :: thesis: a in P
then consider p being Element of P such that
UU2: a = p and
p misses x /\ y ;
thus a in P by UU2; :: thesis: verum

end;

hence z in P \/ P1 by UU, XBOOLE_0:def 3; :: thesis: verum

end;

{ p where p is Element of P : p misses x /\ y } \/ P1 c= S

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { p where p is Element of P : p misses x /\ y } \/ P1 or a in S )
assume a in { p where p is Element of P : p misses x /\ y } \/ P1 ; :: thesis: a in S
then GHAA: ( a in { p where p is Element of P : p misses x /\ y } or a in P1 ) by XBOOLE_0:def 3;
{ p where p is Element of P : p misses x /\ y } c= S

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { p where p is Element of P : p misses x /\ y } or b in S )
assume b in { p where p is Element of P : p misses x /\ y } ; :: thesis: b in S
then consider p being Element of P such that
GHC: b = p and
p misses x /\ y ;
b in P by GHC;
hence b in S by D1; :: thesis: verum

end;

hence a in S by GHAA; :: thesis: verum

end;

hence { p where p is Element of P : p misses x /\ y } \/ P1 is finite Subset of S by GHAA, D1; :: thesis: verum

end;

{ p where p is Element of P : p misses x /\ y } \/ P1 is a_partition of A

proof

FD1: { p where p is Element of P : p misses x /\ y } \/ P1 c= bool A

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { p where p is Element of P : p misses x /\ y } \/ P1 or z in bool A )
assume z in { p where p is Element of P : p misses x /\ y } \/ P1 ; :: thesis: z in bool A
then O1: ( z in { p where p is Element of P : p misses x /\ y } or z in P1 ) by XBOOLE_0:def 3;
O2: { p where p is Element of P : p misses x /\ y } c= bool A

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { p where p is Element of P : p misses x /\ y } or t in bool A )
assume t in { p where p is Element of P : p misses x /\ y } ; :: thesis: t in bool A
then consider t0 being Element of P such that
O3: ( t = t0 & t0 misses x /\ y ) ;
thus t in bool A by O3; :: thesis: verum

end;

P1 c= bool A

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in P1 or t in bool A )
assume X1: t in P1 ; :: thesis: t in bool A
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 bool (x /\ y) c= bool A by ZFMISC_1:67; :: thesis: verum

end;

then P1 c= bool A by F1, XBOOLE_1:1;
hence t in bool A by X1; :: thesis: verum

end;

hence z in bool A by O1, O2; :: thesis: verum

end;

FD2: union ( { p where p is Element of P : p misses x /\ y } \/ P1) = A

proof

thus union ( { p where p is Element of P : p misses x /\ y } \/ P1) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= union ( { p where p is Element of P : p misses x /\ y } \/ P1)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union ( { p where p is Element of P : p misses x /\ y } \/ P1) or a in A )
assume S0: a in union ( { p where p is Element of P : p misses x /\ y } \/ P1) ; :: thesis: a in A
S1: union ( { p where p is Element of P : p misses x /\ y } \/ P1) = (union { p where p is Element of P : p misses x /\ y } ) \/ (union P1) by ZFMISC_1:78;
S5: union P1 c= A by KK2, F1, EQREL_1:def 4;
union { p where p is Element of P : p misses x /\ y } c= A

proof

S5a: { p where p is Element of P : p misses x /\ y } c= P

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { p where p is Element of P : p misses x /\ y } or a in P )
assume a in { p where p is Element of P : p misses x /\ y } ; :: thesis: a in P
then consider b being Element of P such that
S6: a = b and
b misses x /\ y ;
thus a in P by S6; :: thesis: verum

end;

union P = A by EQREL_1:def 4;
hence union { p where p is Element of P : p misses x /\ y } c= A by S5a, ZFMISC_1:77; :: thesis: verum

end;

then (union { p where p is Element of P : p misses x /\ y } ) \/ (union P1) c= A by S5, XBOOLE_1:8;
hence a in A by S0, S1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in union ( { p where p is Element of P : p misses x /\ y } \/ P1) )
assume PO0: a in A ; :: thesis: a in union ( { p where p is Element of P : p misses x /\ y } \/ P1)

per cases ( a in x /\ y or not a in x /\ y ) ;

suppose PO1: a in x /\ y ; :: thesis: a in union ( { p where p is Element of P : p misses x /\ y } \/ P1)

a in union P1 by PO1, F1, EQREL_1:def 4;
then a in (union P1) \/ (union { p where p is Element of P : p misses x /\ y } ) by XBOOLE_1:7, TARSKI:def 3;
hence a in union ( { p where p is Element of P : p misses x /\ y } \/ P1) by ZFMISC_1:78; :: thesis: verum

end;

suppose I0: not a in x /\ y ; :: thesis: a in union ( { p where p is Element of P : p misses x /\ y } \/ P1)

union P = A by EQREL_1:def 4;
then consider b being set such that
I1: a in b and
I2: b in P by PO0, TARSKI:def 4;
consider u being set such that
W1: u in x1 '/\' y1 and
W2: b c= u by I2, D2, SETFAM_1:def 2;
consider xx1, yy1 being 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 ; :: thesis: contradiction
then consider i being 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 contradiction by I0, I1, W2, W4; :: thesis: verum

end;

b misses x /\ y

proof

assume not b misses x /\ y ; :: thesis: contradiction
then consider b0 being 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 contradiction by W5W, W2, W4, XBOOLE_0:def 4; :: thesis: verum

end;

then b in { p where p is Element of P : p misses x /\ y } by I2;
then a in union { p where p is Element of P : p misses x /\ y } by I1, TARSKI:def 4;
then a in (union { p where p is Element of P : p misses x /\ y } ) \/ (union P1) by XBOOLE_1:7, TARSKI:def 3;
hence a in union ( { p where p is Element of P : p misses x /\ y } \/ P1) by ZFMISC_1:78; :: thesis: verum

end;

end;

end;

for a being Subset of A st a in { p where p is Element of P : p misses x /\ y } \/ P1 holds
( a <> {} & ( for b being Subset of A holds
( not b in { p where p is Element of P : p misses x /\ y } \/ P1 or a = b or a misses b ) ) )

proof

let a be Subset of A; :: thesis: ( a in { p where p is Element of P : p misses x /\ y } \/ P1 implies ( a <> {} & ( for b being Subset of A holds
( not b in { p where p is Element of P : p misses x /\ y } \/ P1 or a = b or a misses b ) ) ) )
assume a in { p where p is Element of P : p misses x /\ y } \/ P1 ; :: thesis: ( a <> {} & ( for b being Subset of A holds
( not b in { p where p is Element of P : p misses x /\ y } \/ P1 or a = b or a misses b ) ) )
then DF1: ( a in { p where p is Element of P : p misses x /\ y } or a in P1 ) by XBOOLE_0:def 3;
DF1A: { p where p is Element of P : p misses x /\ y } c= P

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { p where p is Element of P : p misses x /\ y } or a in P )
assume a in { p where p is Element of P : p misses x /\ y } ; :: thesis: a in P
then consider p being Element of P such that
UU2: a = p and
p misses x /\ y ;
thus a in P by UU2; :: thesis: verum

end;

for b being Subset of A holds
( not b in { p where p is Element of P : p misses x /\ y } \/ P1 or a = b or a misses b )

proof

let b be Subset of A; :: thesis: ( not b in { p where p is Element of P : p misses x /\ y } \/ P1 or a = b or a misses b )
assume b in { p where p is Element of P : p misses x /\ y } \/ P1 ; :: thesis: ( a = b or a misses b )
then DF5: ( b in { p where p is Element of P : p misses x /\ y } or b in P1 ) by XBOOLE_0:def 3;
DF7A: ( a in { p where p is Element of P : p misses x /\ y } & b in P1 implies a misses b )

proof

assume that
QW1: a in { p where p is Element of P : p misses x /\ y } and
QW2: b in P1 ; :: thesis: a misses b
consider a0 being Element of P such that
QW3: ( a = a0 & a0 misses x /\ y ) by QW1;
thus a misses b by QW3, QW2, F1, XBOOLE_1:63; :: thesis: verum

end;

( b in { p where p is Element of P : p misses x /\ y } & a in P1 implies a misses b )

proof

assume that
QW1: b in { p where p is Element of P : p misses x /\ y } and
QW2: a in P1 ; :: thesis: a misses b
consider b0 being Element of P such that
QW3: ( b = b0 & b0 misses x /\ y ) by QW1;
thus a misses b by QW3, QW2, F1, XBOOLE_1:63; :: thesis: verum

end;

hence ( a = b or a misses b ) by DF1, DF5, DF1A, DF7A, F1, EQREL_1:def 4; :: thesis: verum

end;

hence ( a <> {} & ( for b being Subset of A holds
( not b in { p where p is Element of P : p misses x /\ y } \/ P1 or a = b or a misses b ) ) ) by F1, DF1A, DF1; :: thesis: verum

end;

hence { p where p is Element of P : p misses x /\ y } \/ P1 is a_partition of A by FD1, FD2, EQREL_1:def 4; :: thesis: verum

end;

then ( d in { p where p is Element of P : p misses x /\ y } \/ P1 & { p where p is Element of P : p misses x /\ y } \/ P1 in PARTITIONS A & { p where p is Element of P : p misses x /\ y } \/ P1 in Fin S ) by UP, XBOOLE_0:def 3, GH2, PARTIT1:def 3, FINSUB_1:def 5;
then ( d in { p where p is Element of P : p misses x /\ y } \/ P1 & { p where p is Element of P : p misses x /\ y } \/ P1 in (PARTITIONS A) /\ (Fin S) ) by XBOOLE_0:def 4;
then d in union ((PARTITIONS A) /\ (Fin S)) by TARSKI:def 4;
hence d in B by UP; :: thesis: verum

end;

hence P1 is finite Subset of B ; :: thesis: verum

end;

hence ex P being finite Subset of B st P is a_partition of x /\ y by F1; :: thesis: verum

end;

hence { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A by AA, Defcap; :: thesis: verum

end;

end;

end;

end;