let X be set ; for S being diff-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is diff-closed
let S be diff-finite-partition-closed Subset-Family of X; { (union x) where x is finite Subset of S : x is mutually-disjoint } is diff-closed
set Y = { (union x) where x is finite Subset of S : x is mutually-disjoint } ;
for A, B being set st A in { (union x) where x is finite Subset of S : x is mutually-disjoint } & B in { (union x) where x is finite Subset of S : x is mutually-disjoint } holds
A \ B in { (union x) where x is finite Subset of S : x is mutually-disjoint }
proof
let A,
B be
set ;
( A in { (union x) where x is finite Subset of S : x is mutually-disjoint } & B in { (union x) where x is finite Subset of S : x is mutually-disjoint } implies A \ B in { (union x) where x is finite Subset of S : x is mutually-disjoint } )
assume that A1:
A in { (union x) where x is finite Subset of S : x is mutually-disjoint }
and A2:
B in { (union x) where x is finite Subset of S : x is mutually-disjoint }
;
A \ B in { (union x) where x is finite Subset of S : x is mutually-disjoint }
consider a being
finite Subset of
S such that A3:
A = union a
and A4:
a is
mutually-disjoint
by A1;
consider b being
finite Subset of
S such that A5:
B = union b
and
b is
mutually-disjoint
by A2;
consider SFA being
FinSequence such that A7:
a = rng SFA
by FINSEQ_1:52;
consider SFB being
FinSequence such that A8:
b = rng SFB
by FINSEQ_1:52;
defpred S1[
object ,
object ]
means ex
A being
set st
(
A = $1 & $1
in a & $2 is
a_partition of
A \ (Union SFB) );
set XOUT =
{ s where s is finite Subset of S : verum } ;
A12:
for
x being
object st
x in a holds
ex
y being
object st
(
y in { s where s is finite Subset of S : verum } &
S1[
x,
y] )
consider f being
Function such that F1:
(
dom f = a &
rng f c= { s where s is finite Subset of S : verum } )
and F2:
for
x being
object st
x in a holds
S1[
x,
f . x]
from FUNCT_1:sch 6(A12);
V1:
Union f is
finite Subset of
S
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 ;
TARSKI:def 3 ( not x in Union f or x in bool ((Union SFA) \ (Union SFB)) )
assume
x in Union f
;
x in bool ((Union SFA) \ (Union SFB))
then consider y being
set such that R1:
x in y
and R2:
y in rng f
by TARSKI:def 4;
consider x0 being
object such that R3:
x0 in dom f
and R4:
y = f . x0
by R2, FUNCT_1:def 3;
reconsider x0 =
x0 as
set by TARSKI:1;
R5:
S1[
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
x in bool ((Union SFA) \ (Union SFB))
by R1, R4;
verum
end;
Z2:
union (Union f) = (Union SFA) \ (Union SFB)
proof
ZE:
union (Union f) c= (Union SFA) \ (Union SFB)
(Union SFA) \ (Union SFB) c= union (Union f)
proof
let x be
object ;
TARSKI:def 3 ( not x in (Union SFA) \ (Union SFB) or x in union (Union f) )
assume U1:
x in (Union SFA) \ (Union SFB)
;
x in union (Union f)
consider y being
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;
S1[
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
x in union (Union f)
by U6;
verum
end;
hence
union (Union f) = (Union SFA) \ (Union SFB)
by ZE;
verum
end;
for
m being
Subset of
((Union SFA) \ (Union SFB)) st
m in Union f holds
(
m <> {} & ( for
n being
Subset of
((Union SFA) \ (Union SFB)) holds
( not
n in Union f or
n = m or
n misses m ) ) )
proof
let m be
Subset of
((Union SFA) \ (Union SFB));
( m in Union f implies ( m <> {} & ( for n being Subset of ((Union SFA) \ (Union SFB)) holds
( not n in Union f or n = m or n misses m ) ) ) )
assume L0:
m in Union f
;
( m <> {} & ( for n being Subset of ((Union SFA) \ (Union SFB)) holds
( not n in Union f or n = m or n misses m ) ) )
consider m0 being
set such that L2:
m in m0
and L3:
m0 in rng f
by L0, TARSKI:def 4;
consider m1 being
object such that L4:
m1 in a
and L5:
m0 = f . m1
by L3, F1, FUNCT_1:def 3;
reconsider m1 =
m1 as
set by TARSKI:1;
L6:
S1[
m1,
f . m1]
by F2, L4;
for
n being
Subset of
((Union SFA) \ (Union SFB)) holds
( not
n in Union f or
n = m or
n misses m )
proof
let n be
Subset of
((Union SFA) \ (Union SFB));
( not n in Union f or n = m or n misses m )
assume CL0:
n in Union f
;
( n = m or n misses m )
(
n = m or
n misses m )
proof
consider n0 being
set such that CL2:
n in n0
and CL3:
n0 in rng f
by CL0, TARSKI:def 4;
consider n1 being
object such that CL4:
n1 in a
and CL5:
n0 = f . n1
by CL3, F1, FUNCT_1:def 3;
reconsider n1 =
n1 as
set by TARSKI:1;
CL6:
S1[
n1,
f . n1]
by F2, CL4;
per cases
( m1 = n1 or not m1 = n1 )
;
suppose KKA:
not
m1 = n1
;
( n = m or n misses m )
m1 \ (Union SFB) misses n1 \ (Union SFB)
by KKA, A4, L4, CL4, TAXONOM2:def 5, XBOOLE_1:64;
hence
(
n = m or
n misses m )
by L6, CL6, L2, L5, CL2, CL5, XBOOLE_1:64;
verum end; end;
end;
hence
(
n = m or
n misses m )
;
verum
end;
hence
(
m <> {} & ( for
n being
Subset of
((Union SFA) \ (Union SFB)) holds
( not
n in Union f or
n = m or
n misses m ) ) )
by L2, L5, L6;
verum
end;
hence
Union f is
a_partition of
(Union SFA) \ (Union SFB)
by Z1, Z2, EQREL_1:def 4;
verum
end;
V2:
Union f is
mutually-disjoint
A \ B = union (Union f)
by V1a, A3, A5, A7, A8, EQREL_1:def 4;
hence
A \ B in { (union x) where x is finite Subset of S : x is mutually-disjoint }
by V1, V2;
verum
end;
hence
{ (union x) where x is finite Subset of S : x is mutually-disjoint } is diff-closed
; verum