let X be set ; :: thesis: for BL being non trivial B_Lattice st ultraset BL = union X & X is Subset of (StoneR BL) holds
ex Y being Finite_Subset of X st ultraset BL = union Y
let BL be non trivial B_Lattice; :: thesis: ( ultraset BL = union X & X is Subset of (StoneR BL) implies ex Y being Finite_Subset of X st ultraset BL = union Y )
assume A1:
( ultraset BL = union X & X is Subset of (StoneR BL) )
; :: thesis: ex Y being Finite_Subset of X st ultraset BL = union Y
assume A2:
for Y being Finite_Subset of X holds not ultraset BL = union Y
; :: thesis: contradiction
consider Y being Finite_Subset of X such that
A3:
not Y is empty
by A1, Th32, ZFMISC_1:2;
A4:
Y c= X
by FINSUB_1:def 5;
then A5:
Y c= StoneR BL
by A1, XBOOLE_1:1;
consider x being Element of Y;
A6:
x in X
by A3, A4, TARSKI:def 3;
x in StoneR BL
by A3, A5, TARSKI:def 3;
then consider b being Element of BL such that
A7:
x = (UFilter BL) . b
by Th26;
set CY = { (a ` ) where a is Element of BL : (UFilter BL) . a in X } ;
consider c being Element of BL such that
A8:
c = b `
;
A9:
c in { (a ` ) where a is Element of BL : (UFilter BL) . a in X }
by A6, A7, A8;
{ (a ` ) where a is Element of BL : (UFilter BL) . a in X } c= the carrier of BL
then reconsider CY = { (a ` ) where a is Element of BL : (UFilter BL) . a in X } as non empty Subset of BL by A9;
set H = <.CY.);
for B being non empty Finite_Subset of the carrier of BL st B c= CY holds
FinMeet B <> Bottom BL
proof
let B be non
empty Finite_Subset of the
carrier of
BL;
:: thesis: ( B c= CY implies FinMeet B <> Bottom BL )
assume that A11:
B c= CY
and A12:
FinMeet B = Bottom BL
;
:: thesis: contradiction
A13:
B is
Subset of
BL
by FINSUB_1:32;
A14:
dom (UFilter BL) = the
carrier of
BL
by FUNCT_2:def 1;
(UFilter BL) .: B c= rng (UFilter BL)
by RELAT_1:144;
then reconsider D =
(UFilter BL) .: B as non
empty Subset-Family of
(ultraset BL) by A13, A14, XBOOLE_1:1;
A16:
( the
L_meet of
BL is
commutative & the
L_meet of
BL is
associative & the
L_meet of
BL is
idempotent )
by LATTICE2:30, LATTICE2:31, LATTICE2:32;
deffunc H1(
Subset of
(ultraset BL),
Subset of
(ultraset BL))
-> Element of
bool (ultraset BL) = $1
/\ $2;
consider G being
BinOp of
(bool (ultraset BL)) such that A17:
for
x,
y being
Subset of
(ultraset BL) holds
G . x,
y = H1(
x,
y)
from BINOP_1:sch 4();
A18:
G is
commutative
A19:
G is
associative
proof
let x,
y,
z be
Subset of
(ultraset BL);
:: according to BINOP_1:def 14 :: thesis: G . x,(G . y,z) = G . (G . x,y),z
G . x,
(G . y,z) =
G . x,
(y /\ z)
by A17
.=
x /\ (y /\ z)
by A17
.=
(x /\ y) /\ z
by XBOOLE_1:16
.=
G . (x /\ y),
z
by A17
.=
G . (G . x,y),
z
by A17
;
hence
G . x,
(G . y,z) = G . (G . x,y),
z
;
:: thesis: verum
end;
A20:
G is
idempotent
A21:
for
x,
y being
Element of
BL holds
(UFilter BL) . (the L_meet of BL . x,y) = G . ((UFilter BL) . x),
((UFilter BL) . y)
reconsider DD =
D as
Element of
Fin (bool (ultraset BL)) ;
id BL = id the
carrier of
BL
;
then A22:
(UFilter BL) . (FinMeet B) =
(UFilter BL) . (FinMeet B,(id the carrier of BL))
by LATTICE4:def 13
.=
(UFilter BL) . (the L_meet of BL $$ B,(id the carrier of BL))
by LATTICE2:def 4
.=
G $$ B,
((UFilter BL) * (id the carrier of BL))
by A16, A18, A19, A20, A21, SETWISEO:39
.=
G $$ B,
(UFilter BL)
by FUNCT_2:23
.=
G $$ B,
((id (bool (ultraset BL))) * (UFilter BL))
by FUNCT_2:23
.=
G $$ DD,
(id (bool (ultraset BL)))
by A18, A19, A20, SETWISEO:38
;
defpred S1[
Element of
Fin (bool (ultraset BL))]
means for
D being non
empty Subset-Family of
(ultraset BL) st
D = $1 holds
G $$ $1,
(id (bool (ultraset BL))) = meet D;
A23:
S1[
{}. (bool (ultraset BL))]
;
A24:
for
DD being
Element of
Fin (bool (ultraset BL)) for
b being
Subset of
(ultraset BL) st
S1[
DD] holds
S1[
DD \/ {.b.}]
proof
let DD be
Element of
Fin (bool (ultraset BL));
:: thesis: for b being Subset of (ultraset BL) st S1[DD] holds
S1[DD \/ {.b.}]let b be
Subset of
(ultraset BL);
:: thesis: ( S1[DD] implies S1[DD \/ {.b.}] )
assume A25:
for
D being non
empty Subset-Family of
(ultraset BL) st
D = DD holds
G $$ DD,
(id (bool (ultraset BL))) = meet D
;
:: thesis: S1[DD \/ {.b.}]
let D be non
empty Subset-Family of
(ultraset BL);
:: thesis: ( D = DD \/ {.b.} implies G $$ (DD \/ {.b.}),(id (bool (ultraset BL))) = meet D )
assume A26:
D = DD \/ {b}
;
:: thesis: G $$ (DD \/ {.b.}),(id (bool (ultraset BL))) = meet D
now per cases
( DD is empty or not DD is empty )
;
suppose A28:
not
DD is
empty
;
:: thesis: G $$ (DD \/ {.b.}),(id (bool (ultraset BL))) = meet D
DD c= D
by A26, XBOOLE_1:7;
then reconsider D1 =
DD as non
empty Subset-Family of
(ultraset BL) by A28, XBOOLE_1:1;
reconsider D1 =
D1 as non
empty Subset-Family of
(ultraset BL) ;
thus G $$ (DD \/ {.b.}),
(id (bool (ultraset BL))) =
G . (G $$ DD,(id (bool (ultraset BL)))),
((id (bool (ultraset BL))) . b)
by A18, A19, A20, A28, SETWISEO:29
.=
G . (G $$ DD,(id (bool (ultraset BL)))),
b
by FUNCT_1:35
.=
(G $$ DD,(id (bool (ultraset BL)))) /\ b
by A17
.=
(meet D1) /\ b
by A25
.=
(meet D1) /\ (meet {b})
by SETFAM_1:11
.=
meet D
by A26, SETFAM_1:10
;
:: thesis: verum end;
hence
G $$ (DD \/ {.b.}),
(id (bool (ultraset BL))) = meet D
;
:: thesis: verum
end;
for
DD being
Element of
Fin (bool (ultraset BL)) holds
S1[
DD]
from SETWISEO:sch 4(A23, A24);
then
meet D = {} (ultraset BL)
by A12, A15, A22;
then A29:
union (COMPLEMENT D) =
([#] (ultraset BL)) \ {}
by SETFAM_1:48
.=
ultraset BL
;
COMPLEMENT D is
Finite_Subset of
X
hence
contradiction
by A2, A29;
:: thesis: verum
end;
then
<.CY.) <> the carrier of BL
by Th34;
then consider F being Filter of BL such that
A39:
( <.CY.) c= F & F is being_ultrafilter )
by FILTER_0:22;
consider F1 being Filter of BL such that
A40:
( F = F1 & F1 is being_ultrafilter )
by A39;
A41:
CY c= <.CY.)
by FILTER_0:def 5;
not F in union X
hence
contradiction
by A1, A40; :: thesis: verum