let C be complete Lattice; :: thesis: for X being set st X c= bool the carrier of C holds
"\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C)
let X be set ; :: thesis: ( X c= bool the carrier of C implies "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) )
set Z = { ("\/" Y) where Y is Subset of C : Y in X } ;
{ ("\/" Y) where Y is Subset of C : Y in X } is_less_than "\/" ((union X),C)
proof
let a be Element of C; :: according to LATTICE3:def 17 :: thesis: ( a in { ("\/" Y) where Y is Subset of C : Y in X } implies a [= "\/" ((union X),C) )
assume a in { ("\/" Y) where Y is Subset of C : Y in X } ; :: thesis: a [= "\/" ((union X),C)
then consider Y being Subset of C such that
A1: a = "\/" Y and
A2: Y in X ;
Y c= union X by A2, ZFMISC_1:74;
hence a [= "\/" ((union X),C) by A1, Th45; :: thesis: verum
end;
then A3: "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) [= "\/" ((union X),C) by Def21;
set V = { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ;
assume A4: X c= bool the carrier of C ; :: thesis: "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C)
union X c= { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } )
assume x in union X ; :: thesis: x in { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) }
then consider Y being set such that
A5: x in Y and
A6: Y in X by TARSKI:def 4;
reconsider Y = Y as Subset of C by A4, A6;
reconsider a = x as Element of C by A4, A5, A6;
A7: a [= "\/" Y by A5, Th38;
"\/" Y in { ("\/" Y) where Y is Subset of C : Y in X } by A6;
hence x in { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } by A7; :: thesis: verum
end;
then "\/" ((union X),C) [= "\/" ( { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ,C) by Th45;
then "\/" ((union X),C) [= "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) by Th46;
hence "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) by A3, LATTICES:8; :: thesis: verum