let S be Scott meet-continuous TopLattice; :: thesis: for F being finite Subset of S holds Int () c= union { () where x is Element of S : x in F }
let F be finite Subset of S; :: thesis: Int () c= union { () where x is Element of S : x in F }
defpred S1[ set ] means ex UU being Subset-Family of S st
( UU = { () where x is Element of S : x in \$1 } & (union UU) ^0 = union { (() ^0) where x is Element of S : x in \$1 } );
A1: for b, J being set st b in F & J c= F & S1[J] holds
S1[J \/ {b}]
proof
let b, J be set ; :: thesis: ( b in F & J c= F & S1[J] implies S1[J \/ {b}] )
assume that
A2: b in F and
J c= F ; :: thesis: ( not S1[J] or S1[J \/ {b}] )
reconsider bb = b as Element of S by A2;
A3: (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) = union { (() ^0) where x is Element of S : x in J \/ {b} }
proof
{ ((uparrow x) ^0) where x is Element of S : x in J } c= { (() ^0) where x is Element of S : x in J \/ {b} }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (() ^0) where x is Element of S : x in J } or a in { (() ^0) where x is Element of S : x in J \/ {b} } )
assume a in { (() ^0) where x is Element of S : x in J } ; :: thesis: a in { (() ^0) where x is Element of S : x in J \/ {b} }
then A4: ex y being Element of S st
( a = () ^0 & y in J ) ;
J c= J \/ {b} by XBOOLE_1:7;
hence a in { (() ^0) where x is Element of S : x in J \/ {b} } by A4; :: thesis: verum
end;
then A5: union { (() ^0) where x is Element of S : x in J } c= union { (() ^0) where x is Element of S : x in J \/ {b} } by ZFMISC_1:77;
A6: {b} c= J \/ {b} by XBOOLE_1:7;
b in {b} by TARSKI:def 1;
then (uparrow bb) ^0 in { (() ^0) where x is Element of S : x in J \/ {b} } by A6;
then (uparrow bb) ^0 c= union { (() ^0) where x is Element of S : x in J \/ {b} } by ZFMISC_1:74;
hence (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) c= union { (() ^0) where x is Element of S : x in J \/ {b} } by ; :: according to XBOOLE_0:def 10 :: thesis: union { (() ^0) where x is Element of S : x in J \/ {b} } c= (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (() ^0) where x is Element of S : x in J \/ {b} } or a in (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) )
assume a in union { (() ^0) where x is Element of S : x in J \/ {b} } ; :: thesis: a in (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)
then consider A being set such that
A7: a in A and
A8: A in { (() ^0) where x is Element of S : x in J \/ {b} } by TARSKI:def 4;
consider y being Element of S such that
A9: A = () ^0 and
A10: y in J \/ {b} by A8;
per cases ( y in J or y in {b} ) by ;
suppose y in J ; :: thesis: a in (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)
then (uparrow y) ^0 in { (() ^0) where x is Element of S : x in J } ;
then A11: a in union { (() ^0) where x is Element of S : x in J } by ;
union { (() ^0) where x is Element of S : x in J } c= (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by XBOOLE_1:7;
hence a in (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A11; :: thesis: verum
end;
suppose A12: y in {b} ; :: thesis: a in (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)
A13: (uparrow bb) ^0 c= (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by XBOOLE_1:7;
y = b by ;
hence a in (union { (() ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A13, A7, A9; :: thesis: verum
end;
end;
end;
assume S1[J] ; :: thesis: S1[J \/ {b}]
then consider UU being Subset-Family of S such that
A14: UU = { () where x is Element of S : x in J } and
A15: (union UU) ^0 = union { (() ^0) where x is Element of S : x in J } ;
reconsider I = UU \/ {(uparrow bb)} as Subset-Family of S ;
take I ; :: thesis: ( I = { () where x is Element of S : x in J \/ {b} } & () ^0 = union { (() ^0) where x is Element of S : x in J \/ {b} } )
thus I = { () where x is Element of S : x in J \/ {b} } :: thesis: () ^0 = union { (() ^0) where x is Element of S : x in J \/ {b} }
proof
thus I c= { () where x is Element of S : x in J \/ {b} } :: according to XBOOLE_0:def 10 :: thesis: { () where x is Element of S : x in J \/ {b} } c= I
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in I or a in { () where x is Element of S : x in J \/ {b} } )
assume A16: a in I ; :: thesis: a in { () where x is Element of S : x in J \/ {b} }
per cases ( a in UU or a in {(uparrow bb)} ) by ;
suppose A17: a in UU ; :: thesis: a in { () where x is Element of S : x in J \/ {b} }
A18: J c= J \/ {b} by XBOOLE_1:7;
ex x being Element of S st
( a = uparrow x & x in J ) by ;
hence a in { () where x is Element of S : x in J \/ {b} } by A18; :: thesis: verum
end;
suppose A19: a in {(uparrow bb)} ; :: thesis: a in { () where x is Element of S : x in J \/ {b} }
A20: b in {b} by TARSKI:def 1;
A21: {b} c= J \/ {b} by XBOOLE_1:7;
a = uparrow bb by ;
hence a in { () where x is Element of S : x in J \/ {b} } by ; :: thesis: verum
end;
end;
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { () where x is Element of S : x in J \/ {b} } or a in I )
assume a in { () where x is Element of S : x in J \/ {b} } ; :: thesis: a in I
then consider x being Element of S such that
A22: a = uparrow x and
A23: x in J \/ {b} ;
per cases ( x in J or x in {b} ) by ;
end;
end;
A29: (union UU) \/ (uparrow bb) = union I
proof
thus (union UU) \/ (uparrow bb) c= union I :: according to XBOOLE_0:def 10 :: thesis: union I c= (union UU) \/ (uparrow bb)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (union UU) \/ (uparrow bb) or a in union I )
assume A30: a in (union UU) \/ (uparrow bb) ; :: thesis: a in union I
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union I or a in (union UU) \/ (uparrow bb) )
assume a in union I ; :: thesis: a in (union UU) \/ (uparrow bb)
then consider A being set such that
A35: a in A and
A36: A in I by TARSKI:def 4;
end;
for X being Subset of S st X in UU holds
X is upper
proof
let X be Subset of S; :: thesis: ( X in UU implies X is upper )
assume X in UU ; :: thesis: X is upper
then ex x being Element of S st
( X = uparrow x & x in J ) by A14;
hence X is upper ; :: thesis: verum
end;
then union UU is upper by WAYBEL_0:28;
hence (union I) ^0 = union { (() ^0) where x is Element of S : x in J \/ {b} } by A3, A15, A29, Th28; :: thesis: verum
end;
A40: S1[ {} ]
proof
deffunc H1( Element of S) -> Subset of S = (uparrow \$1) ^0 ;
reconsider UU = {} as Subset-Family of S by XBOOLE_1:2;
take UU ; :: thesis: ( UU = { () where x is Element of S : x in {} } & (union UU) ^0 = union { (() ^0) where x is Element of S : x in {} } )
reconsider K = union UU as empty Subset of S ;
A41: K ^0 is empty ;
thus UU = { () where x is Element of S : x in {} } :: thesis: (union UU) ^0 = union { (() ^0) where x is Element of S : x in {} }
proof
deffunc H2( Element of S) -> Element of bool the carrier of S = uparrow \$1;
{ H2(x) where x is Element of S : x in {} } = {} from hence UU = { () where x is Element of S : x in {} } ; :: thesis: verum
end;
{ H1(x) where x is Element of S : x in {} } = {} from hence (union UU) ^0 = union { (() ^0) where x is Element of S : x in {} } by A41; :: thesis: verum
end;
A42: { ((uparrow x) ^0) where x is Element of S : x in F } = { () where x is Element of S : x in F }
proof
thus { ((uparrow x) ^0) where x is Element of S : x in F } c= { () where x is Element of S : x in F } :: according to XBOOLE_0:def 10 :: thesis: { () where x is Element of S : x in F } c= { (() ^0) where x is Element of S : x in F }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (() ^0) where x is Element of S : x in F } or a in { () where x is Element of S : x in F } )
assume a in { (() ^0) where x is Element of S : x in F } ; :: thesis: a in { () where x is Element of S : x in F }
then consider x being Element of S such that
A43: a = () ^0 and
A44: x in F ;
(uparrow x) ^0 = wayabove x by Th25;
hence a in { () where x is Element of S : x in F } by ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { () where x is Element of S : x in F } or a in { (() ^0) where x is Element of S : x in F } )
assume a in { () where x is Element of S : x in F } ; :: thesis: a in { (() ^0) where x is Element of S : x in F }
then consider x being Element of S such that
A45: a = wayabove x and
A46: x in F ;
(uparrow x) ^0 = wayabove x by Th25;
hence a in { (() ^0) where x is Element of S : x in F } by ; :: thesis: verum
end;
A47: F is finite ;
S1[F] from FINSET_1:sch 2(A47, A40, A1);
then (uparrow F) ^0 = union { () where x is Element of S : x in F } by ;
hence Int () c= union { () where x is Element of S : x in F } by Th26; :: thesis: verum