let X be set ; for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B being set st A in S & B in DisUnion S holds
B \ A in DisUnion S
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; for A, B being set st A in S & B in DisUnion S holds
B \ A in DisUnion S
let A, B be set ; ( A in S & B in DisUnion S implies B \ A in DisUnion S )
assume A2:
( A in S & B in DisUnion S )
; B \ A in DisUnion S
reconsider A1 = A as Subset of X by A2;
consider B1 being Subset of X such that
A5:
( B = B1 & ex F being disjoint_valued FinSequence of S st B1 = Union F )
by A2;
consider g1 being disjoint_valued FinSequence of S such that
A6:
B1 = Union g1
by A5;
reconsider R1 = DisUnion S as non empty set ;
defpred S1[ Nat, object ] means $2 = (g1 . $1) \ A1;
A7:
for k being Nat st k in Seg (len g1) holds
ex x being Element of R1 st S1[k,x]
consider g2 being FinSequence of R1 such that
A8:
( dom g2 = Seg (len g1) & ( for k being Nat st k in Seg (len g1) holds
S1[k,g2 . k] ) )
from FINSEQ_1:sch 5(A7);
A11:
for n, m being Nat st n in dom g2 & m in dom g2 & n <> m holds
g2 . n misses g2 . m
set R = DisUnion S;
defpred S2[ Nat] means union (rng (g2 | $1)) in DisUnion S;
( union (rng (g2 | 0)) in S & S c= DisUnion S )
by lemma100, SETFAM_1:def 8, ZFMISC_1:2;
then A12:
S2[ 0 ]
;
A13:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A14:
S2[
k]
;
S2[k + 1]
per cases
( k + 1 <= len g2 or k + 1 > len g2 )
;
suppose A15:
k + 1
<= len g2
;
S2[k + 1]then A20:
(
k <= len g2 &
k <= k + 1 )
by NAT_1:13;
then
(
len (g2 | (k + 1)) = k + 1 &
g2 | k = (g2 | (k + 1)) | k )
by A15, FINSEQ_1:59, FINSEQ_1:82;
then
g2 | (k + 1) = (g2 | k) ^ <*((g2 | (k + 1)) . (k + 1))*>
by FINSEQ_3:55;
then rng (g2 | (k + 1)) =
(rng (g2 | k)) \/ (rng <*((g2 | (k + 1)) . (k + 1))*>)
by FINSEQ_1:31
.=
(rng (g2 | k)) \/ {((g2 | (k + 1)) . (k + 1))}
by FINSEQ_1:38
.=
(rng (g2 | k)) \/ {(g2 . (k + 1))}
by FINSEQ_3:112
;
then A16:
union (rng (g2 | (k + 1))) =
(union (rng (g2 | k))) \/ (union {(g2 . (k + 1))})
by ZFMISC_1:78
.=
(union (rng (g2 | k))) \/ (g2 . (k + 1))
;
A24:
k + 1
in dom g2
by A15, FINSEQ_3:25, NAT_1:11;
A25:
now not union (rng (g2 | k)) meets g2 . (k + 1)assume
union (rng (g2 | k)) meets g2 . (k + 1)
;
contradictionthen consider x being
object such that A17:
(
x in union (rng (g2 | k)) &
x in g2 . (k + 1) )
by XBOOLE_0:3;
consider Z being
set such that A18:
(
x in Z &
Z in rng (g2 | k) )
by A17, TARSKI:def 4;
consider i being
object such that A19:
(
i in dom (g2 | k) &
Z = (g2 | k) . i )
by A18, FUNCT_1:def 3;
reconsider i =
i as
Nat by A19;
i <= len (g2 | k)
by A19, FINSEQ_3:25;
then A21:
i <= k
by A20, FINSEQ_1:59;
then A22:
Z = g2 . i
by A19, FINSEQ_3:112;
A23:
dom (g2 | k) c= dom g2
by RELAT_1:60;
i <> k + 1
by A21, NAT_1:13;
then
Z misses g2 . (k + 1)
by A11, A22, A23, A19, A24;
hence
contradiction
by A17, A18, XBOOLE_0:def 4;
verum end;
(
g2 . (k + 1) in rng g2 &
rng g2 c= DisUnion S )
by A24, FUNCT_1:3;
hence
union (rng (g2 | (k + 1))) in DisUnion S
by A14, A16, A25, lemma102;
verum end; end;
end;
for k being Nat holds S2[k]
from NAT_1:sch 2(A12, A13);
then C1:
S2[ len g2]
;
now for x being object st x in union (rng g2) holds
x in (union (rng g1)) \ A1let x be
object ;
( x in union (rng g2) implies x in (union (rng g1)) \ A1 )assume
x in union (rng g2)
;
x in (union (rng g1)) \ A1then consider y being
set such that B1:
(
x in y &
y in rng g2 )
by TARSKI:def 4;
consider k being
object such that B2:
(
k in dom g2 &
y = g2 . k )
by B1, FUNCT_1:def 3;
reconsider k =
k as
Nat by B2;
C3:
g2 . k = (g1 . k) \ A1
by B2, A8;
then B3:
(
x in g1 . k & not
x in A1 )
by B1, B2, XBOOLE_0:def 5;
k in dom g1
by B2, A8, FINSEQ_1:def 3;
then
g1 . k in rng g1
by FUNCT_1:3;
then
x in union (rng g1)
by C3, B1, B2, TARSKI:def 4;
hence
x in (union (rng g1)) \ A1
by B3, XBOOLE_0:def 5;
verum end;
then B4:
union (rng g2) c= (union (rng g1)) \ A1
;
then
(union (rng g1)) \ A1 c= union (rng g2)
;
then
(union (rng g1)) \ A1 = union (rng g2)
by B4;
hence
B \ A in DisUnion S
by A5, A6, C1, FINSEQ_1:58; verum