let Y be non empty set ; for PA, PB being a_partition of Y
for y being Element of Y ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
let PA, PB be a_partition of Y; for y being Element of Y ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
let y be Element of Y; ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
A1:
union PA = Y
by EQREL_1:def 4;
A2:
for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) )
by EQREL_1:def 4;
A3:
( Y is_a_dependent_set_of PA & Y is_a_dependent_set_of PB )
by Th7;
defpred S1[ set ] means ( y in $1 & $1 is_a_dependent_set_of PA & $1 is_a_dependent_set_of PB );
reconsider XX = { X where X is Subset of Y : S1[X] } as Subset-Family of Y from DOMAIN_1:sch 7();
reconsider XX = XX as Subset-Family of Y ;
Y c= Y
;
then A4:
Y in XX
by A3;
for X1 being set st X1 in XX holds
y in X1
then A5:
y in meet XX
by A4, SETFAM_1:def 1;
then A6:
Intersect XX <> {}
by SETFAM_1:def 9;
take
Intersect XX
; ( y in Intersect XX & Intersect XX is_min_depend PA,PB )
for X1 being set st X1 in XX holds
X1 is_a_dependent_set_of PA
then A7:
Intersect XX is_a_dependent_set_of PA
by A6, Th8;
for X1 being set st X1 in XX holds
X1 is_a_dependent_set_of PB
then A8:
Intersect XX is_a_dependent_set_of PB
by A6, Th8;
for d being set st d c= Intersect XX & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = Intersect XX
proof
let d be
set ;
( d c= Intersect XX & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB implies d = Intersect XX )
assume that A9:
d c= Intersect XX
and A10:
d is_a_dependent_set_of PA
and A11:
d is_a_dependent_set_of PB
;
d = Intersect XX
consider Ad being
set such that A12:
Ad c= PA
and A13:
Ad <> {}
and A14:
d = union Ad
by A10;
A15:
d c= Y
by A1, A12, A14, ZFMISC_1:77;
per cases
( y in d or not y in d )
;
suppose A17:
not
y in d
;
d = Intersect XXreconsider d =
d as
Subset of
Y by A1, A12, A14, ZFMISC_1:77;
d ` = Y \ d
by SUBSET_1:def 4;
then A18:
y in d `
by A17, XBOOLE_0:def 5;
d misses d `
by SUBSET_1:24;
then A19:
d /\ (d `) = {}
by XBOOLE_0:def 7;
d <> Y
by A17;
then
(
d ` is_a_dependent_set_of PA &
d ` is_a_dependent_set_of PB )
by A10, A11, Th10;
then A20:
d ` in XX
by A18;
Intersect XX c= d `
then A21:
d /\ (Intersect XX) = {}
by A19, XBOOLE_1:3, XBOOLE_1:26;
d /\ d c= d /\ (Intersect XX)
by A9, XBOOLE_1:26;
then A22:
union Ad = {}
by A14, A21;
consider ad being
object such that A23:
ad in Ad
by A13, XBOOLE_0:def 1;
A24:
ad <> {}
by A2, A12, A23;
reconsider ad =
ad as
set by TARSKI:1;
ad c= {}
by A22, A23, ZFMISC_1:74;
hence
d = Intersect XX
by A24;
verum end; end;
end;
hence
( y in Intersect XX & Intersect XX is_min_depend PA,PB )
by A4, A5, A7, A8, SETFAM_1:def 9; verum