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 Element of Fin 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 Element of Fin X st ultraset BL = union Y )

assume that

A1: ultraset BL = union X and

A2: X is Subset of (StoneR BL) ; :: thesis: 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 ; :: thesis: 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

set H = <.CY.);

for B being non empty Element of Fin the carrier of BL st B c= CY holds

FinMeet B <> Bottom BL

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

ex Y being Element of Fin 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 Element of Fin X st ultraset BL = union Y )

assume that

A1: ultraset BL = union X and

A2: X is Subset of (StoneR BL) ; :: thesis: 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 ; :: thesis: 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

proof

then reconsider CY = { (a `) where a is Element of BL : (UFilter BL) . a in X } as non empty Subset of BL by A10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a `) where a is Element of BL : (UFilter BL) . a in X } or x in the carrier of BL )

assume x in { (a `) where a is Element of BL : (UFilter BL) . a in X } ; :: thesis: x in the carrier of BL

then ex b being Element of BL st

( x = b ` & (UFilter BL) . b in X ) ;

hence x in the carrier of BL ; :: thesis: verum

end;assume x in { (a `) where a is Element of BL : (UFilter BL) . a in X } ; :: thesis: x in the carrier of BL

then ex b being Element of BL st

( x = b ` & (UFilter BL) . b in X ) ;

hence x in the carrier of BL ; :: thesis: verum

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

then
<.CY.) <> the carrier of BL
by Th28;
let B be non empty Element of Fin 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: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;

_{1}( 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) = H_{1}(x,y)
from BINOP_1:sch 4();

A17: G is commutative

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 S_{1}[ 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: S_{1}[ {}. (bool (ultraset BL))]
;

A23: for DD being Element of Fin (bool (ultraset BL))

for b being Subset of (ultraset BL) st S_{1}[DD] holds

S_{1}[DD \/ {.b.}]
_{1}[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

hence contradiction by A3, A28; :: thesis: verum

end;assume that

A11: B c= CY and

A12: FinMeet B = Bottom BL ; :: thesis: 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;

A15: now :: thesis: not {} (ultraset BL) <> (UFilter BL) . (Bottom BL)

deffunc Hset x = the Element of (UFilter BL) . (Bottom BL);

assume {} (ultraset BL) <> (UFilter BL) . (Bottom BL) ; :: thesis: contradiction

then ex F being Filter of BL st

( F = the Element of (UFilter BL) . (Bottom BL) & F is being_ultrafilter & Bottom BL in F ) by Th17;

hence contradiction by Th29; :: thesis: verum

end;assume {} (ultraset BL) <> (UFilter BL) . (Bottom BL) ; :: thesis: contradiction

then ex F being Filter of BL st

( F = the Element of (UFilter BL) . (Bottom BL) & F is being_ultrafilter & Bottom BL in F ) by Th17;

hence contradiction by Th29; :: thesis: verum

consider G being BinOp of (bool (ultraset BL)) such that

A16: for x, y being Subset of (ultraset BL) holds G . (x,y) = H

A17: G is commutative

proof

A18:
G is associative
let x, y be Subset of (ultraset BL); :: according to BINOP_1:def 2 :: thesis: G . (x,y) = G . (y,x)

G . (x,y) = y /\ x by A16

.= G . (y,x) by A16 ;

hence G . (x,y) = G . (y,x) ; :: thesis: verum

end;G . (x,y) = y /\ x by A16

.= G . (y,x) by A16 ;

hence G . (x,y) = G . (y,x) ; :: thesis: verum

proof

A19:
G is idempotent
let x, y, z be Subset of (ultraset BL); :: according to BINOP_1:def 3 :: thesis: 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) ; :: thesis: verum

end;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) ; :: thesis: verum

proof

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))
let x be Subset of (ultraset BL); :: according to BINOP_1:def 4 :: thesis: G . (x,x) = x

G . (x,x) = x /\ x by A16

.= x ;

hence G . (x,x) = x ; :: thesis: verum

end;G . (x,x) = x /\ x by A16

.= x ;

hence G . (x,x) = x ; :: thesis: verum

proof

reconsider DD = D as Element of Fin (bool (ultraset BL)) ;
let x, y be Element of BL; :: thesis: (UFilter BL) . ( the L_meet of BL . (x,y)) = G . (((UFilter BL) . x),((UFilter BL) . y))

thus (UFilter BL) . ( the L_meet of BL . (x,y)) = (UFilter BL) . (x "/\" y)

.= ((UFilter BL) . x) /\ ((UFilter BL) . y) by Th20

.= G . (((UFilter BL) . x),((UFilter BL) . y)) by A16 ; :: thesis: verum

end;thus (UFilter BL) . ( the L_meet of BL . (x,y)) = (UFilter BL) . (x "/\" y)

.= ((UFilter BL) . x) /\ ((UFilter BL) . y) by Th20

.= G . (((UFilter BL) . x),((UFilter BL) . y)) by A16 ; :: thesis: verum

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 S

G $$ ($1,(id (bool (ultraset BL)))) = meet D;

A22: S

A23: for DD being Element of Fin (bool (ultraset BL))

for b being Subset of (ultraset BL) st S

S

proof

for DD being Element of Fin (bool (ultraset BL)) holds S
let DD be Element of Fin (bool (ultraset BL)); :: thesis: for b being Subset of (ultraset BL) st S_{1}[DD] holds

S_{1}[DD \/ {.b.}]

let b be Subset of (ultraset BL); :: thesis: ( S_{1}[DD] implies S_{1}[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 ; :: thesis: S_{1}[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 A25: D = DD \/ {b} ; :: thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D

end;S

let b be Subset of (ultraset BL); :: thesis: ( S

assume A24: for D being non empty Subset-Family of (ultraset BL) st D = DD holds

G $$ (DD,(id (bool (ultraset BL)))) = meet D ; :: thesis: S

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 A25: D = DD \/ {b} ; :: thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D

now :: thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet Dend;

hence
G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D
; :: thesis: verumper cases
( DD is empty or not DD is empty )
;

end;

suppose A26:
DD is empty
; :: thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D

hence G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) =
(id (bool (ultraset BL))) . b
by A17, A18, SETWISEO:17

.= b

.= meet D by A25, A26, SETFAM_1:10 ;

:: thesis: verum

end;.= b

.= meet D by A25, A26, SETFAM_1:10 ;

:: thesis: verum

suppose A27:
not DD is empty
; :: thesis: 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 ; :: thesis: verum

end;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 ; :: thesis: verum

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

proof

COMPLEMENT D is finite
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT D or x in X )

assume A30: x in COMPLEMENT D ; :: thesis: x in X

then reconsider c = x as Subset of (ultraset BL) ;

c ` in D by A30, SETFAM_1:def 7;

then consider a being object such that

A31: a in dom (UFilter BL) and

A32: a in B and

A33: c ` = (UFilter BL) . a by FUNCT_1:def 6;

reconsider a = a as Element of BL by A31;

a in CY by A11, A32;

then (a `) ` in CY ;

then consider b being Element of BL such that

A34: b ` = (a `) ` and

A35: (UFilter BL) . b in X ;

x = ((UFilter BL) . a) ` by A33

.= (UFilter BL) . (a `) by Th25

.= (UFilter BL) . ((b `) `) by A34

.= (UFilter BL) . b ;

hence x in X by A35; :: thesis: verum

end;assume A30: x in COMPLEMENT D ; :: thesis: x in X

then reconsider c = x as Subset of (ultraset BL) ;

c ` in D by A30, SETFAM_1:def 7;

then consider a being object such that

A31: a in dom (UFilter BL) and

A32: a in B and

A33: c ` = (UFilter BL) . a by FUNCT_1:def 6;

reconsider a = a as Element of BL by A31;

a in CY by A11, A32;

then (a `) ` in CY ;

then consider b being Element of BL such that

A34: b ` = (a `) ` and

A35: (UFilter BL) . b in X ;

x = ((UFilter BL) . a) ` by A33

.= (UFilter BL) . (a `) by Th25

.= (UFilter BL) . ((b `) `) by A34

.= (UFilter BL) . b ;

hence x in X by A35; :: thesis: verum

proof

then
COMPLEMENT D is Element of Fin X
by A29, FINSUB_1:def 5;
A36:
D is finite
;

deffunc H_{2}( Subset of (ultraset BL)) -> Element of K19((ultraset BL)) = $1 ` ;

A37: { H_{2}(w) where w is Subset of (ultraset BL) : w in D } is finite
from FRAENKEL:sch 21(A36);

{ (w `) where w is Subset of (ultraset BL) : w in D } = COMPLEMENT D

end;deffunc H

A37: { H

{ (w `) where w is Subset of (ultraset BL) : w in D } = COMPLEMENT D

proof

assume A40: x in COMPLEMENT D ; :: thesis: x in { (w `) where w is Subset of (ultraset BL) : w in D }

then reconsider x9 = x as Subset of (ultraset BL) ;

A41: x9 ` in D by A40, SETFAM_1:def 7;

(x9 `) ` = x9 ;

hence x in { (w `) where w is Subset of (ultraset BL) : w in D } by A41; :: thesis: verum

end;

hence
COMPLEMENT D is finite
by A37; :: thesis: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: COMPLEMENT D c= { (w `) where w is Subset of (ultraset BL) : w in D }

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT D or x in { (w `) where w is Subset of (ultraset BL) : w in D } )let x be object ; :: thesis: ( x in { (w `) where w is Subset of (ultraset BL) : w in D } implies x in COMPLEMENT D )

assume x in { (w `) where w is Subset of (ultraset BL) : w in D } ; :: thesis: x in COMPLEMENT D

then consider w being Subset of (ultraset BL) such that

A38: w ` = x and

A39: w in D ;

(w `) ` in D by A39;

hence x in COMPLEMENT D by A38, SETFAM_1:def 7; :: thesis: verum

end;assume x in { (w `) where w is Subset of (ultraset BL) : w in D } ; :: thesis: x in COMPLEMENT D

then consider w being Subset of (ultraset BL) such that

A38: w ` = x and

A39: w in D ;

(w `) ` in D by A39;

hence x in COMPLEMENT D by A38, SETFAM_1:def 7; :: thesis: verum

assume A40: x in COMPLEMENT D ; :: thesis: x in { (w `) where w is Subset of (ultraset BL) : w in D }

then reconsider x9 = x as Subset of (ultraset BL) ;

A41: x9 ` in D by A40, SETFAM_1:def 7;

(x9 `) ` = x9 ;

hence x in { (w `) where w is Subset of (ultraset BL) : w in D } by A41; :: thesis: verum

hence contradiction by A3, A28; :: thesis: verum

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

proof

hence
contradiction
by A1, A43; :: thesis: verum
assume
F in union X
; :: thesis: contradiction

then consider Y being set such that

A45: F in Y and

A46: Y in X by TARSKI:def 4;

consider a being object such that

A47: a in dom (UFilter BL) and

A48: Y = (UFilter BL) . a by A2, A46, FUNCT_1:def 3;

reconsider a = a as Element of BL by A47;

a ` in CY by A46, A48;

then A49: a ` in <.CY.) by A44;

a in F by A45, A48, Th18;

hence contradiction by A42, A43, A49, FILTER_0:46; :: thesis: verum

end;then consider Y being set such that

A45: F in Y and

A46: Y in X by TARSKI:def 4;

consider a being object such that

A47: a in dom (UFilter BL) and

A48: Y = (UFilter BL) . a by A2, A46, FUNCT_1:def 3;

reconsider a = a as Element of BL by A47;

a ` in CY by A46, A48;

then A49: a ` in <.CY.) by A44;

a in F by A45, A48, Th18;

hence contradiction by A42, A43, A49, FILTER_0:46; :: thesis: verum