set Z = { F2(z) where z is Element of F1() : P1[z] } ;
set X = { (varcl F2(z)) where z is Element of F1() : P1[z] } ;
A1: union { F2(z) where z is Element of F1() : P1[z] } c= union { (varcl F2(z)) where z is Element of F1() : P1[z] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { F2(z) where z is Element of F1() : P1[z] } or x in union { (varcl F2(z)) where z is Element of F1() : P1[z] } )
assume x in union { F2(z) where z is Element of F1() : P1[z] } ; :: thesis: x in union { (varcl F2(z)) where z is Element of F1() : P1[z] }
then consider Y being set such that
A2: x in Y and
A3: Y in { F2(z) where z is Element of F1() : P1[z] } by TARSKI:def 4;
A4: ex z being Element of F1() st
( Y = F2(z) & P1[z] ) by A3;
A5: Y c= varcl Y by Def1;
varcl Y in { (varcl F2(z)) where z is Element of F1() : P1[z] } by A4;
hence x in union { (varcl F2(z)) where z is Element of F1() : P1[z] } by A2, A5, TARSKI:def 4; :: thesis: verum
end;
now :: thesis: for x, y being set st [x,y] in union { (varcl F2(z)) where z is Element of F1() : P1[z] } holds
x c= union { (varcl F2(z)) where z is Element of F1() : P1[z] }
let x, y be set ; :: thesis: ( [x,y] in union { (varcl F2(z)) where z is Element of F1() : P1[z] } implies x c= union { (varcl F2(z)) where z is Element of F1() : P1[z] } )
assume [x,y] in union { (varcl F2(z)) where z is Element of F1() : P1[z] } ; :: thesis: x c= union { (varcl F2(z)) where z is Element of F1() : P1[z] }
then consider Y being set such that
A6: [x,y] in Y and
A7: Y in { (varcl F2(z)) where z is Element of F1() : P1[z] } by TARSKI:def 4;
ex z being Element of F1() st
( Y = varcl F2(z) & P1[z] ) by A7;
then A8: x c= Y by A6, Def1;
Y c= union { (varcl F2(z)) where z is Element of F1() : P1[z] } by A7, ZFMISC_1:74;
hence x c= union { (varcl F2(z)) where z is Element of F1() : P1[z] } by A8; :: thesis: verum
end;
hence varcl (union { F2(z) where z is Element of F1() : P1[z] } ) c= union { (varcl F2(z)) where z is Element of F1() : P1[z] } by A1, Def1; :: according to XBOOLE_0:def 10 :: thesis: union { (varcl F2(z)) where z is Element of F1() : P1[z] } c= varcl (union { F2(z) where z is Element of F1() : P1[z] } )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (varcl F2(z)) where z is Element of F1() : P1[z] } or x in varcl (union { F2(z) where z is Element of F1() : P1[z] } ) )
assume x in union { (varcl F2(z)) where z is Element of F1() : P1[z] } ; :: thesis: x in varcl (union { F2(z) where z is Element of F1() : P1[z] } )
then consider Y being set such that
A9: x in Y and
A10: Y in { (varcl F2(z)) where z is Element of F1() : P1[z] } by TARSKI:def 4;
consider z being Element of F1() such that
A11: Y = varcl F2(z) and
A12: P1[z] by A10;
F2(z) in { F2(z) where z is Element of F1() : P1[z] } by A12;
then Y c= varcl (union { F2(z) where z is Element of F1() : P1[z] } ) by A11, Th9, ZFMISC_1:74;
hence x in varcl (union { F2(z) where z is Element of F1() : P1[z] } ) by A9; :: thesis: verum