let S be Subset-Family of F1(); :: thesis: ( S = { X where X is Subset of F1() : P1[X] } implies uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] } )
assume A1: S = { X where X is Subset of F1() : P1[X] } ; :: thesis: uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] }
A2: union { (uparrow X) where X is Subset of F1() : P1[X] } c= uparrow (union S)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union { (uparrow X) where X is Subset of F1() : P1[X] } or z in uparrow (union S) )
assume z in union { (uparrow X) where X is Subset of F1() : P1[X] } ; :: thesis: z in uparrow (union S)
then consider Z being set such that
A3: z in Z and
A4: Z in { (uparrow X) where X is Subset of F1() : P1[X] } by TARSKI:def 4;
consider X1 being Subset of F1() such that
A5: Z = uparrow X1 and
A6: P1[X1] by A4;
reconsider z1 = z as Element of F1() by A3, A5;
consider y1 being Element of F1() such that
A7: y1 <= z1 and
A8: y1 in X1 by A3, A5, WAYBEL_0:def 16;
X1 in S by A1, A6;
then y1 in union S by A8, TARSKI:def 4;
hence z in uparrow (union S) by A7, WAYBEL_0:def 16; :: thesis: verum
end;
uparrow (union S) c= union { (uparrow X) where X is Subset of F1() : P1[X] }
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in uparrow (union S) or z in union { (uparrow X) where X is Subset of F1() : P1[X] } )
assume A9: z in uparrow (union S) ; :: thesis: z in union { (uparrow X) where X is Subset of F1() : P1[X] }
then reconsider z1 = z as Element of F1() ;
consider y1 being Element of F1() such that
A10: y1 <= z1 and
A11: y1 in union S by A9, WAYBEL_0:def 16;
consider Z being set such that
A12: y1 in Z and
A13: Z in S by A11, TARSKI:def 4;
consider X1 being Subset of F1() such that
A14: Z = X1 and
A15: P1[X1] by A1, A13;
A16: uparrow X1 in { (uparrow X) where X is Subset of F1() : P1[X] } by A15;
z in uparrow X1 by A10, A12, A14, WAYBEL_0:def 16;
hence z in union { (uparrow X) where X is Subset of F1() : P1[X] } by A16, TARSKI:def 4; :: thesis: verum
end;
hence uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] } by A2, XBOOLE_0:def 10; :: thesis: verum