let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for y being Element of Y st G <> {} holds
ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
let G be Subset of (PARTITIONS Y); for y being Element of Y st G <> {} holds
ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
let y be Element of Y; ( G <> {} implies ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G ) )
defpred S1[ set ] means ( y in $1 & ( for d being a_partition of Y st d in G holds
$1 is_a_dependent_set_of d ) );
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 ;
assume
G <> {}
; ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
then consider g being object such that
A1:
g in G
by XBOOLE_0:def 1;
reconsider g = g as a_partition of Y by A1, PARTIT1:def 3;
A2:
union g = Y
by EQREL_1:def 4;
take
Intersect XX
; ( y in Intersect XX & Intersect XX is_upper_min_depend_of G )
( Y c= Y & ( for d being a_partition of Y st d in G holds
Y is_a_dependent_set_of d ) )
by PARTIT1:7;
then A3:
Y in XX
;
A4:
for A being set st A in g holds
( A <> {} & ( for B being set holds
( not B in g or A = B or A misses B ) ) )
by EQREL_1:def 4;
A5:
for e being set st e c= Intersect XX & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) holds
e = Intersect XX
proof
let e be
set ;
( e c= Intersect XX & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) implies e = Intersect XX )
assume that A6:
e c= Intersect XX
and A7:
for
d being
a_partition of
Y st
d in G holds
e is_a_dependent_set_of d
;
e = Intersect XX
consider Ad being
set such that A8:
Ad c= g
and A9:
Ad <> {}
and A10:
e = union Ad
by A1, A7, PARTIT1:def 1;
A11:
e c= Y
by A2, A8, A10, ZFMISC_1:77;
per cases
( y in e or not y in e )
;
suppose A13:
not
y in e
;
e = Intersect XXreconsider e =
e as
Subset of
Y by A2, A8, A10, ZFMISC_1:77;
e ` = Y \ e
by SUBSET_1:def 4;
then A14:
y in e `
by A13, XBOOLE_0:def 5;
e <> Y
by A13;
then
for
d being
a_partition of
Y st
d in G holds
e ` is_a_dependent_set_of d
by A7, PARTIT1:10;
then A15:
e ` in XX
by A14;
A16:
Intersect XX c= e `
A17:
e /\ e = e
;
consider ad being
object such that A18:
ad in Ad
by A9, XBOOLE_0:def 1;
reconsider ad =
ad as
set by TARSKI:1;
e /\ (e `) = {}
by SUBSET_1:24, XBOOLE_0:def 7;
then
e /\ (Intersect XX) = {}
by A16, XBOOLE_1:3, XBOOLE_1:26;
then
e c= {}
by A6, A17, XBOOLE_1:26;
then
union Ad = {}
by A10;
then A19:
ad c= {}
by A18, ZFMISC_1:74;
ad <> {}
by A4, A8, A18;
hence
e = Intersect XX
by A19;
verum end; end;
end;
for X1 being set st X1 in XX holds
y in X1
then A20:
y in meet XX
by A3, SETFAM_1:def 1;
then A21:
Intersect XX <> {}
by SETFAM_1:def 9;
for d being a_partition of Y st d in G holds
Intersect XX is_a_dependent_set_of d
hence
( y in Intersect XX & Intersect XX is_upper_min_depend_of G )
by A3, A20, A5, SETFAM_1:def 9; verum