let R be Semilattice; :: thesis: for D being non empty directed Subset of (InclPoset (Ids R))
for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }
let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }
let x be Element of (InclPoset (Ids R)); :: thesis: sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }
set I = InclPoset (Ids R);
set A = { (x /\ d) where d is Element of D : verum } ;
set xD = { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } ;
{ (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } c= the carrier of (InclPoset (Ids R))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } or a in the carrier of (InclPoset (Ids R)) )
assume a in { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } ; :: thesis: a in the carrier of (InclPoset (Ids R))
then ex d being Element of (InclPoset (Ids R)) st
( a = x "/\" d & d in D ) ;
hence a in the carrier of (InclPoset (Ids R)) ; :: thesis: verum
end;
then reconsider xD = { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } as Subset of (InclPoset (Ids R)) ;
A1: ex_sup_of {x} "/\" D, InclPoset (Ids R) by WAYBEL_2:1;
then ex_sup_of xD, InclPoset (Ids R) by YELLOW_4:42;
then A2: sup xD is_>=_than xD by YELLOW_0:def 9;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (x /\ d) where d is Element of D : verum } c= sup ({x} "/\" D)
set A = { (x /\ w) where w is Element of D : verum } ;
let a be object ; :: thesis: ( a in sup ({x} "/\" D) implies a in union { (x /\ w) where w is Element of D : verum } )
ex_sup_of D, InclPoset (Ids R) by WAYBEL_0:75;
then sup ({x} "/\" D) <= x "/\" (sup D) by A1, YELLOW_4:53;
then A3: sup ({x} "/\" D) c= x "/\" (sup D) by YELLOW_1:3;
assume a in sup ({x} "/\" D) ; :: thesis: a in union { (x /\ w) where w is Element of D : verum }
then a in x "/\" (sup D) by A3;
then A4: a in x /\ (sup D) by YELLOW_2:43;
then a in sup D by XBOOLE_0:def 4;
then a in union D by Th3;
then consider d being set such that
A5: a in d and
A6: d in D by TARSKI:def 4;
reconsider d = d as Element of (InclPoset (Ids R)) by A6;
A7: x /\ d in { (x /\ w) where w is Element of D : verum } by A6;
a in x by A4, XBOOLE_0:def 4;
then a in x /\ d by A5, XBOOLE_0:def 4;
hence a in union { (x /\ w) where w is Element of D : verum } by A7, TARSKI:def 4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (x /\ d) where d is Element of D : verum } or a in sup ({x} "/\" D) )
assume a in union { (x /\ d) where d is Element of D : verum } ; :: thesis: a in sup ({x} "/\" D)
then consider Z being set such that
A8: a in Z and
A9: Z in { (x /\ d) where d is Element of D : verum } by TARSKI:def 4;
consider d being Element of D such that
A10: Z = x /\ d and
verum by A9;
reconsider d = d as Element of (InclPoset (Ids R)) ;
A11: xD = {x} "/\" D by YELLOW_4:42;
then x "/\" d in {x} "/\" D ;
then sup xD >= x "/\" d by A2, A11;
then A12: x "/\" d c= sup xD by YELLOW_1:3;
x /\ d = x "/\" d by YELLOW_2:43;
then a in sup xD by A12, A8, A10;
hence a in sup ({x} "/\" D) by YELLOW_4:42; :: thesis: verum