let X be set ; for BL being non trivial B_Lattice st ultraset BL = union X & X is Subset of (StoneR BL) holds
ex Y being Element of Fin X st ultraset BL = union Y
let BL be non trivial B_Lattice; ( ultraset BL = union X & X is Subset of (StoneR BL) implies ex Y being Element of Fin X st ultraset BL = union Y )
assume that
A1:
ultraset BL = union X
and
A2:
X is Subset of (StoneR BL)
; ex Y being Element of Fin X st ultraset BL = union Y
assume A3:
for Y being Element of Fin X holds not ultraset BL = union Y
; contradiction
consider Y being Element of Fin X such that
A4:
not Y is empty
by A1, Th27, ZFMISC_1:2;
A5:
Y c= X
by FINSUB_1:def 5;
then A6:
Y c= StoneR BL
by A2, XBOOLE_1:1;
set x = the Element of Y;
A7:
the Element of Y in X
by A4, A5;
the Element of Y in StoneR BL
by A4, A6;
then consider b being Element of BL such that
A8:
the Element of Y = (UFilter BL) . b
by Th23;
set CY = { (a `) where a is Element of BL : (UFilter BL) . a in X } ;
consider c being Element of BL such that
A9:
c = b `
;
A10:
c in { (a `) where a is Element of BL : (UFilter BL) . a in X }
by A7, A8, A9;
{ (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 A10;
set H = <.CY.);
for B being non empty Element of Fin the carrier of BL st B c= CY holds
FinMeet B <> Bottom BL
proof
let B be non
empty Element of
Fin the
carrier of
BL;
( B c= CY implies FinMeet B <> Bottom BL )
assume that A11:
B c= CY
and A12:
FinMeet B = Bottom BL
;
contradiction
A13:
B is
Subset of
BL
by FINSUB_1:16;
A14:
dom (UFilter BL) = the
carrier of
BL
by FUNCT_2:def 1;
(UFilter BL) .: B c= rng (UFilter BL)
by RELAT_1:111;
then reconsider D =
(UFilter BL) .: B as non
empty Subset-Family of
(ultraset BL) by A13, A14, XBOOLE_1:1;
deffunc H1(
Subset of
(ultraset BL),
Subset of
(ultraset BL))
-> Element of
K19(
(ultraset BL)) = $1
/\ $2;
consider G being
BinOp of
(bool (ultraset BL)) such that A16:
for
x,
y being
Subset of
(ultraset BL) holds
G . (
x,
y)
= H1(
x,
y)
from BINOP_1:sch 4();
A17:
G is
commutative
A18:
G is
associative
proof
let x,
y,
z be
Subset of
(ultraset BL);
BINOP_1:def 3 G . (x,(G . (y,z))) = G . ((G . (x,y)),z)
G . (
x,
(G . (y,z))) =
G . (
x,
(y /\ z))
by A16
.=
x /\ (y /\ z)
by A16
.=
(x /\ y) /\ z
by XBOOLE_1:16
.=
G . (
(x /\ y),
z)
by A16
.=
G . (
(G . (x,y)),
z)
by A16
;
hence
G . (
x,
(G . (y,z)))
= G . (
(G . (x,y)),
z)
;
verum
end;
A19:
G is
idempotent
A20:
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 A21:
(UFilter BL) . (FinMeet B) =
(UFilter BL) . (FinMeet (B,(id the carrier of BL)))
by LATTICE4:def 9
.=
(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 A17, A18, A19, A20, SETWISEO:30
.=
G $$ (
B,
(UFilter BL))
by FUNCT_2:17
.=
G $$ (
B,
((id (bool (ultraset BL))) * (UFilter BL)))
by FUNCT_2:17
.=
G $$ (
DD,
(id (bool (ultraset BL))))
by A17, A18, A19, SETWISEO:29
;
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;
A22:
S1[
{}. (bool (ultraset BL))]
;
A23:
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));
for b being Subset of (ultraset BL) st S1[DD] holds
S1[DD \/ {.b.}]let b be
Subset of
(ultraset BL);
( S1[DD] implies S1[DD \/ {.b.}] )
assume A24:
for
D being non
empty Subset-Family of
(ultraset BL) st
D = DD holds
G $$ (
DD,
(id (bool (ultraset BL))))
= meet D
;
S1[DD \/ {.b.}]
let D be non
empty Subset-Family of
(ultraset BL);
( D = DD \/ {.b.} implies G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D )
assume A25:
D = DD \/ {b}
;
G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D
now G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet Dper cases
( DD is empty or not DD is empty )
;
suppose A27:
not
DD is
empty
;
G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D
DD c= D
by A25, XBOOLE_1:7;
then reconsider D1 =
DD as non
empty Subset-Family of
(ultraset BL) by A27, 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 A17, A18, A19, A27, SETWISEO:20
.=
G . (
(G $$ (DD,(id (bool (ultraset BL))))),
b)
.=
(G $$ (DD,(id (bool (ultraset BL))))) /\ b
by A16
.=
(meet D1) /\ b
by A24
.=
(meet D1) /\ (meet {b})
by SETFAM_1:10
.=
meet D
by A25, SETFAM_1:9
;
verum end; end; end;
hence
G $$ (
(DD \/ {.b.}),
(id (bool (ultraset BL))))
= meet D
;
verum
end;
for
DD being
Element of
Fin (bool (ultraset BL)) holds
S1[
DD]
from SETWISEO:sch 4(A22, A23);
then
meet D = {} (ultraset BL)
by A12, A15, A21;
then A28:
union (COMPLEMENT D) =
([#] (ultraset BL)) \ {}
by SETFAM_1:34
.=
ultraset BL
;
A29:
COMPLEMENT D c= X
COMPLEMENT D is
finite
then
COMPLEMENT D is
Element of
Fin X
by A29, FINSUB_1:def 5;
hence
contradiction
by A3, A28;
verum
end;
then
<.CY.) <> the carrier of BL
by Th28;
then consider F being Filter of BL such that
A42:
<.CY.) c= F
and
A43:
F is being_ultrafilter
by FILTER_0:18;
A44:
CY c= <.CY.)
by FILTER_0:def 4;
not F in union X
hence
contradiction
by A1, A43; verum