let X be set ; 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 diff-c=-finite-partition-closed Subset-Family of A
let S be 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 diff-c=-finite-partition-closed Subset-Family of A
let A be Element of S; { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is diff-c=-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 H1:
not
A is
empty
;
{ x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is diff-c=-finite-partition-closed Subset-Family of AAA:
{ x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } c= bool A
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
not
{ x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is
empty
;
{ x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is diff-c=-finite-partition-closed Subset-Family of Athen 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
y c= x holds
ex
P being
finite Subset of
B st
P is
a_partition of
x \ y
proof
let x,
y be
Element of
B;
( y c= x implies ex P being finite Subset of B st P is a_partition of x \ y )
assume
y c= x
;
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,
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;
set P1 =
{ p where p is Element of P : ( p is Subset of x & p misses y ) } ;
T1:
{ p where p is Element of P : ( p is Subset of x & p misses y ) } is
finite Subset of
B
{ p where p is Element of P : ( p is Subset of x & p misses y ) } is
a_partition of
x \ y
proof
Y1:
{ p where p is Element of P : ( p is Subset of x & p misses y ) } c= bool (x \ y)
Y2:
union { p where p is Element of P : ( p is Subset of x & p misses y ) } = x \ y
proof
thus
union { p where p is Element of P : ( p is Subset of x & p misses y ) } c= x \ y
XBOOLE_0:def 10 x \ y c= union { p where p is Element of P : ( p is Subset of x & p misses y ) }
let a be
object ;
TARSKI:def 3 ( not a in x \ y or a in union { p where p is Element of P : ( p is Subset of x & p misses y ) } )
assume AS0:
a in x \ y
;
a in union { p where p is Element of P : ( p is Subset of x & p misses 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 being
set such that U2:
a in b
and U3:
b in P
by TARSKI:def 4;
consider u being
set such that U4:
u in x1 '/\' y1
and U5:
b c= u
by U3, 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 U4, SETFAM_1:def 5;
UU1:
b is
Subset of
x
b misses y
proof
assume
not
b misses y
;
contradiction
then consider z being
object such that WA1:
z in b /\ y
by XBOOLE_0:def 1;
consider v being
set such that K1:
v in x1 '/\' y1
and K2:
b c= v
by U3, D2, SETFAM_1:def 2;
consider xx1,
yy1 being
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
(
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
contradiction
by A1, C1, W3, EQREL_1:def 4, LEM, AS2A, XBOOLE_0:def 7;
verum
end;
then
b in { p where p is Element of P : ( p is Subset of x & p misses y ) }
by UU1, U3;
hence
a in union { p where p is Element of P : ( p is Subset of x & p misses y ) }
by U2, TARSKI:def 4;
verum
end;
for
a being
Subset of
(x \ y) st
a in { p where p is Element of P : ( p is Subset of x & p misses y ) } holds
(
a <> {} & ( for
b being
Subset of
(x \ y) holds
( not
b in { p where p is Element of P : ( p is Subset of x & p misses y ) } or
a = b or
a misses b ) ) )
hence
{ p where p is Element of P : ( p is Subset of x & p misses y ) } is
a_partition of
x \ y
by Y1, Y2, EQREL_1:def 4;
verum
end;
hence
ex
P being
finite Subset of
B st
P is
a_partition of
x \ y
by T1;
verum
end; hence
{ x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is
diff-c=-finite-partition-closed Subset-Family of
A
by AA, Defdiff2;
verum end; end;