let BL be Boolean Lattice; :: thesis: for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds
for B being Element of Fin the carrier of BL st B c= SetImp AF holds
ex B0 being Element of Fin the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )
let AF be non empty ClosedSubset of BL; :: thesis: ( Bottom BL in AF & Top BL in AF implies for B being Element of Fin the carrier of BL st B c= SetImp AF holds
ex B0 being Element of Fin the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) )
assume that
A1: Bottom BL in AF and
A2: Top BL in AF ; :: thesis: for B being Element of Fin the carrier of BL st B c= SetImp AF holds
ex B0 being Element of Fin the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )
set C = { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } ;
A3: { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } c= SetImp AF
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } or x in SetImp AF )
assume x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: x in SetImp AF
then consider A1, A2 being Element of Fin the carrier of BL such that
A4: x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and
A5: ( A1 c= AF & A2 c= AF ) ;
consider p, q being Element of BL such that
A6: ( p = FinMeet A2 & q = FinJoin A1 ) ;
A7: x = (p `) "\/" q by A4, A6, Th41;
( p in AF & q in AF ) by A1, A2, A5, A6, Th17, Th24;
hence x in SetImp AF by A7, Th37; :: thesis: verum
end;
defpred S1[ Element of Fin the carrier of BL] means ( $1 c= SetImp AF implies ex B0 being Element of Fin the carrier of BL st
( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ($1,(comp BL)) = FinMeet B0 ) );
let B be Element of Fin the carrier of BL; :: thesis: ( B c= SetImp AF implies ex B0 being Element of Fin the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) )
assume A8: B c= SetImp AF ; :: thesis: ex B0 being Element of Fin the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )
A9: for B9 being Element of Fin the carrier of BL
for b being Element of BL st S1[B9] holds
S1[B9 \/ {.b.}]
proof
set J = the L_join of BL;
let B9 be Element of Fin the carrier of BL; :: thesis: for b being Element of BL st S1[B9] holds
S1[B9 \/ {.b.}]
let b be Element of BL; :: thesis: ( S1[B9] implies S1[B9 \/ {.b.}] )
assume A10: ( B9 c= SetImp AF implies ex B1 being Element of Fin the carrier of BL st
( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B9,(comp BL)) = FinMeet B1 ) ) ; :: thesis: S1[B9 \/ {.b.}]
assume A11: B9 \/ {b} c= SetImp AF ; :: thesis: ex B0 being Element of Fin the carrier of BL st
( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet B0 )
then consider B1 being Element of Fin the carrier of BL such that
A12: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } and
A13: FinJoin (B9,(comp BL)) = FinMeet B1 by A10, ZFMISC_1:137;
b in SetImp AF by A11, ZFMISC_1:137;
then consider p, q being Element of BL such that
A14: b = (p `) "\/" q and
A15: p in AF and
A16: q in AF by Th37;
A17: for x being set
for b being Element of BL st x in ( the L_join of BL [:] ((id BL),b)) .: B1 holds
ex a being Element of BL st
( a in B1 & x = a "\/" b )
proof
let x be set ; :: thesis: for b being Element of BL st x in ( the L_join of BL [:] ((id BL),b)) .: B1 holds
ex a being Element of BL st
( a in B1 & x = a "\/" b )
let b be Element of BL; :: thesis: ( x in ( the L_join of BL [:] ((id BL),b)) .: B1 implies ex a being Element of BL st
( a in B1 & x = a "\/" b ) )
assume A18: x in ( the L_join of BL [:] ((id BL),b)) .: B1 ; :: thesis: ex a being Element of BL st
( a in B1 & x = a "\/" b )
( the L_join of BL [:] ((id BL),b)) .: B1 c= the carrier of BL by FUNCT_2:36;
then reconsider x = x as Element of BL by A18;
consider a being Element of BL such that
A19: a in B1 and
A20: x = ( the L_join of BL [:] ((id BL),b)) . a by A18, FUNCT_2:65;
x = the L_join of BL . (((id BL) . a),b) by A20, FUNCOP_1:48
.= a "\/" b by FUNCT_1:18 ;
hence ex a being Element of BL st
( a in B1 & x = a "\/" b ) by A19; :: thesis: verum
end;
A21: ( the L_join of BL [:] ((id BL),p)) .: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ( the L_join of BL [:] ((id BL),p)) .: B1 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } )
assume x in ( the L_join of BL [:] ((id BL),p)) .: B1 ; :: thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
then consider a being Element of BL such that
A22: a in B1 and
A23: x = a "\/" p by A17;
a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A22;
then consider A1, A2 being Element of Fin the carrier of BL such that
A24: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and
A25: ( A1 c= AF & A2 c= AF ) ;
ex A19, A29 being Element of Fin the carrier of BL st
( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
proof
take A19 = A1 \/ {.p.}; :: thesis: ex A29 being Element of Fin the carrier of BL st
( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
take A29 = A2; :: thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
x = ((FinJoin A1) "\/" p) "\/" (FinJoin (A2,(comp BL))) by A23, A24, LATTICES:def 5
.= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th14 ;
hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A15, A25, ZFMISC_1:137; :: thesis: verum
end;
hence x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: verum
end;
A26: ( the L_join of BL [:] ((id BL),(q `))) .: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ( the L_join of BL [:] ((id BL),(q `))) .: B1 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } )
assume x in ( the L_join of BL [:] ((id BL),(q `))) .: B1 ; :: thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
then consider a being Element of BL such that
A27: a in B1 and
A28: x = a "\/" (q `) by A17;
a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A27;
then consider A1, A2 being Element of Fin the carrier of BL such that
A29: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and
A30: ( A1 c= AF & A2 c= AF ) ;
ex A19, A29 being Element of Fin the carrier of BL st
( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
proof
take A19 = A1; :: thesis: ex A29 being Element of Fin the carrier of BL st
( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
take A29 = A2 \/ {.q.}; :: thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
x = (FinJoin A1) "\/" ((FinJoin (A2,(comp BL))) "\/" (q `)) by A28, A29, LATTICES:def 5
.= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th38 ;
hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A16, A30, ZFMISC_1:137; :: thesis: verum
end;
hence x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: verum
end;
take (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) ; :: thesis: ( (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) )
b ` = ((p `) `) "/\" (q `) by A14, LATTICES:24
.= p "/\" (q `) ;
then FinJoin ((B9 \/ {.b.}),(comp BL)) = (FinMeet B1) "\/" (p "/\" (q `)) by A13, Th38
.= ((FinMeet B1) "\/" p) "/\" ((FinMeet B1) "\/" (q `)) by LATTICES:11
.= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" ((FinMeet B1) "\/" (q `)) by Th25
.= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" (FinMeet (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th25
.= FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th23 ;
hence ( (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) ) by A21, A26, XBOOLE_1:8; :: thesis: verum
end;
A31: S1[ {}. the carrier of BL]
proof
assume {}. the carrier of BL c= SetImp AF ; :: thesis: ex B0 being Element of Fin the carrier of BL st
( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 )
take B0 = {.(Bottom BL).}; :: thesis: ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 )
A32: B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B0 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } )
assume x in B0 ; :: thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
then A33: x = Bottom BL by TARSKI:def 1;
ex A1, A2 being Element of Fin the carrier of BL st
( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )
proof
take A1 = {.(Bottom BL).}; :: thesis: ex A2 being Element of Fin the carrier of BL st
( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )
take A2 = {.(Top BL).}; :: thesis: ( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )
thus x = (Bottom BL) "\/" (Bottom BL) by A33
.= (Bottom BL) "\/" ((Top BL) `) by Th29
.= (FinJoin A1) "\/" ((Top BL) `) by Th9
.= (FinJoin A1) "\/" ((FinMeet A2) `) by Th10
.= (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) by Th41 ; :: thesis: ( A1 c= AF & A2 c= AF )
thus A1 c= AF by A1, ZFMISC_1:31; :: thesis: A2 c= AF
thus A2 c= AF by A2, ZFMISC_1:31; :: thesis: verum
end;
hence x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: verum
end;
FinJoin (({}. the carrier of BL),(comp BL)) = Bottom BL by Lm1
.= FinMeet {.(Bottom BL).} by Th10 ;
hence ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 ) by A32; :: thesis: verum
end;
for B being Element of Fin the carrier of BL holds S1[B] from SETWISEO:sch 4(A31, A9);
 then ex B1 being Element of Fin the carrier of BL st
( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B,(comp BL)) = FinMeet B1 ) by A8;
hence ex B0 being Element of Fin the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) by A3, XBOOLE_1:1; :: thesis: verum