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 Finite_Subset of the carrier of BL st B c= SetImp AF holds
ex B0 being Finite_Subset of 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 Finite_Subset of the carrier of BL st B c= SetImp AF holds
ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin B,(comp BL) = FinMeet B0 ) )
assume A1: ( Bottom BL in AF & Top BL in AF ) ; :: thesis: for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds
ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin B,(comp BL) = FinMeet B0 )
let B be Finite_Subset of the carrier of BL; :: thesis: ( B c= SetImp AF implies ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin B,(comp BL) = FinMeet B0 ) )
assume A2: B c= SetImp AF ; :: thesis: ex B0 being Finite_Subset of 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 Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ;
defpred S1[ Finite_Subset of the carrier of BL] means ( $1 c= SetImp AF implies ex B0 being Finite_Subset of the carrier of BL st
( B0 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin $1,(comp BL) = FinMeet B0 ) );
A3: S1[ {}. the carrier of BL]
proof
assume {}. the carrier of BL c= SetImp AF ; :: thesis: ex B0 being Finite_Subset of the carrier of BL st
( B0 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of 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 Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ({}. the carrier of BL),(comp BL) = FinMeet B0 )
A4: FinJoin ({}. the carrier of BL),(comp BL) = Bottom BL by Lm1
.= FinMeet {.(Bottom BL).} by Th17 ;
B0 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B0 or x in { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of 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 Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
then A5: x = Bottom BL by TARSKI:def 1;
ex A1, A2 being Finite_Subset of 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 Finite_Subset of 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 A5, LATTICES:17
.= (Bottom BL) "\/" ((Top BL) ` ) by Th36
.= (FinJoin A1) "\/" ((Top BL) ` ) by Th16
.= (FinJoin A1) "\/" ((FinMeet A2) ` ) by Th17
.= (FinJoin A1) "\/" (FinJoin A2,(comp BL)) by Th48 ; :: thesis: ( A1 c= AF & A2 c= AF )
thus A1 c= AF by A1, ZFMISC_1:37; :: thesis: A2 c= AF
thus A2 c= AF by A1, ZFMISC_1:37; :: thesis: verum
end;
hence x in { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: verum
end;
hence ( B0 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ({}. the carrier of BL),(comp BL) = FinMeet B0 ) by A4; :: thesis: verum
end;
A6: for B' being Finite_Subset of the carrier of BL
for b being Element of BL st S1[B'] holds
S1[B' \/ {.b.}]
proof
let B' be Finite_Subset of the carrier of BL; :: thesis: for b being Element of BL st S1[B'] holds
S1[B' \/ {.b.}]
let b be Element of BL; :: thesis: ( S1[B'] implies S1[B' \/ {.b.}] )
assume A7: ( B' c= SetImp AF implies ex B1 being Finite_Subset of the carrier of BL st
( B1 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin B',(comp BL) = FinMeet B1 ) ) ; :: thesis: S1[B' \/ {.b.}]
assume A8: B' \/ {b} c= SetImp AF ; :: thesis: ex B0 being Finite_Subset of the carrier of BL st
( B0 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B' \/ {.b.}),(comp BL) = FinMeet B0 )
then A9: ( B' c= SetImp AF & b in SetImp AF ) by SETWISEO:8;
consider B1 being Finite_Subset of the carrier of BL such that
A10: ( B1 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin B',(comp BL) = FinMeet B1 ) by A7, A8, SETWISEO:8;
consider p, q being Element of BL such that
A11: ( b = (p ` ) "\/" q & p in AF & q in AF ) by A9, Th44;
A12: b ` = ((p ` ) ` ) "/\" (q ` ) by A11, LATTICES:51
.= p "/\" (q ` ) by LATTICES:49 ;
set J = the L_join of BL;
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 Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B' \/ {.b.}),(comp BL) = FinMeet (((the L_join of BL [:] (id BL),p) .: B1) \/ ((the L_join of BL [:] (id BL),(q ` )) .: B1)) )
A13: FinJoin (B' \/ {.b.}),(comp BL) = (FinMeet B1) "\/" (p "/\" (q ` )) by A10, A12, Th45
.= ((FinMeet B1) "\/" p) "/\" ((FinMeet B1) "\/" (q ` )) by LATTICES:31
.= (FinMeet ((the L_join of BL [:] (id BL),p) .: B1)) "/\" ((FinMeet B1) "\/" (q ` )) by Th32
.= (FinMeet ((the L_join of BL [:] (id BL),p) .: B1)) "/\" (FinMeet ((the L_join of BL [:] (id BL),(q ` )) .: B1)) by Th32
.= FinMeet (((the L_join of BL [:] (id BL),p) .: B1) \/ ((the L_join of BL [:] (id BL),(q ` )) .: B1)) by Th30 ;
A14: 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 A15: 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:44;
then reconsider x = x as Element of BL by A15;
consider a being Element of BL such that
A16: ( a in B1 & x = (the L_join of BL [:] (id BL),b) . a ) by A15, FUNCT_2:116;
x = the L_join of BL . ((id BL) . a),b by A16, FUNCOP_1:60
.= a "\/" b by TMAP_1:91 ;
hence ex a being Element of BL st
( a in B1 & x = a "\/" b ) by A16; :: thesis: verum
end;
A17: (the L_join of BL [:] (id BL),p) .: B1 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
proof
let x be set ; :: 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 Finite_Subset of 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 Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
then consider a being Element of BL such that
A18: ( a in B1 & x = a "\/" p ) by A14;
a in { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A10, A18;
then consider A1, A2 being Finite_Subset of the carrier of BL such that
A19: ( a = (FinJoin A1) "\/" (FinJoin A2,(comp BL)) & A1 c= AF & A2 c= AF ) ;
ex A1', A2' being Finite_Subset of the carrier of BL st
( x = (FinJoin A1') "\/" (FinJoin A2',(comp BL)) & A1' c= AF & A2' c= AF )
proof
take A1' = A1 \/ {.p.}; :: thesis: ex A2' being Finite_Subset of the carrier of BL st
( x = (FinJoin A1') "\/" (FinJoin A2',(comp BL)) & A1' c= AF & A2' c= AF )
take A2' = A2; :: thesis: ( x = (FinJoin A1') "\/" (FinJoin A2',(comp BL)) & A1' c= AF & A2' c= AF )
x = ((FinJoin A1) "\/" p) "\/" (FinJoin A2,(comp BL)) by A18, A19, LATTICES:def 5
.= (FinJoin A1') "\/" (FinJoin A2',(comp BL)) by Th21 ;
hence ( x = (FinJoin A1') "\/" (FinJoin A2',(comp BL)) & A1' c= AF & A2' c= AF ) by A11, A19, SETWISEO:8; :: thesis: verum
end;
hence x in { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: verum
end;
(the L_join of BL [:] (id BL),(q ` )) .: B1 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
proof
let x be set ; :: 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 Finite_Subset of 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 Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
then consider a being Element of BL such that
A20: ( a in B1 & x = a "\/" (q ` ) ) by A14;
a in { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A10, A20;
then consider A1, A2 being Finite_Subset of the carrier of BL such that
A21: ( a = (FinJoin A1) "\/" (FinJoin A2,(comp BL)) & A1 c= AF & A2 c= AF ) ;
ex A1', A2' being Finite_Subset of the carrier of BL st
( x = (FinJoin A1') "\/" (FinJoin A2',(comp BL)) & A1' c= AF & A2' c= AF )
proof
take A1' = A1; :: thesis: ex A2' being Finite_Subset of the carrier of BL st
( x = (FinJoin A1') "\/" (FinJoin A2',(comp BL)) & A1' c= AF & A2' c= AF )
take A2' = A2 \/ {.q.}; :: thesis: ( x = (FinJoin A1') "\/" (FinJoin A2',(comp BL)) & A1' c= AF & A2' c= AF )
x = (FinJoin A1) "\/" ((FinJoin A2,(comp BL)) "\/" (q ` )) by A20, A21, LATTICES:def 5
.= (FinJoin A1') "\/" (FinJoin A2',(comp BL)) by Th45 ;
hence ( x = (FinJoin A1') "\/" (FinJoin A2',(comp BL)) & A1' c= AF & A2' c= AF ) by A11, A21, SETWISEO:8; :: thesis: verum
end;
hence x in { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: verum
end;
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 Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B' \/ {.b.}),(comp BL) = FinMeet (((the L_join of BL [:] (id BL),p) .: B1) \/ ((the L_join of BL [:] (id BL),(q ` )) .: B1)) ) by A13, A17, XBOOLE_1:8; :: thesis: verum
end;
for B being Finite_Subset of the carrier of BL holds S1[B] from SETWISEO:sch 4(A3, A6);
 then consider B1 being Finite_Subset of the carrier of BL such that
A22: ( B1 c= { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin B,(comp BL) = FinMeet B1 ) by A2;
{ ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } c= SetImp AF
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((FinJoin A1) "\/" (FinJoin A2,(comp BL))) where A1, A2 is Finite_Subset of 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 Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: x in SetImp AF
then consider A1, A2 being Finite_Subset of the carrier of BL such that
A23: ( x = (FinJoin A1) "\/" (FinJoin A2,(comp BL)) & A1 c= AF & A2 c= AF ) ;
consider p, q being Element of BL such that
A24: ( p = FinMeet A2 & q = FinJoin A1 ) ;
A25: ( p in AF & q in AF ) by A1, A23, A24, Th24, Th31;
x = (p ` ) "\/" q by A23, A24, Th48;
hence x in SetImp AF by A25, Th44; :: thesis: verum
end;
hence ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin B,(comp BL) = FinMeet B0 ) by A22, XBOOLE_1:1; :: thesis: verum