let X be set ; :: thesis:
let S be diff-finite-partition-closed Subset-Family of X; :: thesis:
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 ; :: thesis:
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 } ; :: thesis:
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 S₁[ 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 } & S₁[x,y] )

proof

let x be object ; :: thesis:
assume A: x in a ; :: thesis:
reconsider x = x as set by TARSKI:1;
consider P being finite Subset of S such that
B: P is a_partition of x \ (Union SFB) by A, A8, Thm1;
( P in { s where s is finite Subset of S : verum } & S₁[x,P] ) by A, B;
hence ex y being object st
( y in { s where s is finite Subset of S : verum } & S₁[x,y] ) ; :: thesis:

end;

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
S₁[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 being set st x in rng f holds
x is finite

proof

let x be set ; :: thesis:
assume x in rng f ; :: thesis:
then x in { s where s is finite Subset of S : verum } by F1;
then consider s being finite Subset of S such that
V: x = s ;
thus x is finite by V; :: thesis:

end;

hence Union f is finite by F1, FINSET_1:8, FINSET_1:7; :: thesis:

end;

Union f c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Union f ; :: thesis:
then consider y being set such that
H: ( x in y & y in rng f ) by TARSKI:def 4;
y in { s where s is finite Subset of S : verum } by H, F1;
then consider s being finite Subset of S such that
I: y = s ;
thus x in S by H, I; :: thesis:

end;

hence Union f is finite Subset of S by W1; :: thesis:

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 ; :: according to TARSKI:def 3 :: thesis:
assume x in Union f ; :: thesis:
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: S₁[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; :: thesis:

end;

Z2: union (Union f) = (Union SFA) \ (Union SFB)

proof

ZE: union (Union f) c= (Union SFA) \ (Union SFB)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A: x in union (Union f) ; :: thesis:
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 x in (Union SFA) \ (Union SFB) by ZFMISC_1:81; :: thesis:

end;

(Union SFA) \ (Union SFB) c= union (Union f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume U1: x in (Union SFA) \ (Union SFB) ; :: thesis:
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;
S₁[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; :: thesis:

end;

hence union (Union f) = (Union SFA) \ (Union SFB) by ZE; :: thesis:

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)); :: thesis:
assume L0: m in Union f ; :: thesis:
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: S₁[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)); :: thesis:
assume CL0: n in Union f ; :: thesis:
( 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: S₁[n1,f . n1] by F2, CL4;

per cases ;

suppose m1 = n1 ; :: thesis:

hence ( n = m or n misses m ) by L2, L5, CL2, CL5, CL6, EQREL_1:def 4; :: thesis:

end;

suppose KKA: not m1 = n1 ; :: thesis:

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; :: thesis:

end;

hence ( n = m or n misses m ) ; :: thesis:

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; :: thesis:

end;

hence Union f is a_partition of (Union SFA) \ (Union SFB) by Z1, Z2, EQREL_1:def 4; :: thesis:

end;

V2: Union f is mutually-disjoint

proof

for n, m being set st n in Union f & m in Union f & n <> m holds
n misses m by V1a, EQREL_1:def 4;
hence Union f is mutually-disjoint by TAXONOM2:def 5; :: thesis:

end;

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; :: thesis:

end;

hence { (union x) where x is finite Subset of S : x is mutually-disjoint } is diff-closed ; :: thesis: