set X = { F2(x) where x is Subset of F1() : P1[x] } ;
set Y = { (F3() " F2(y)) where y is Subset of F1() : P1[y] } ;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (F3() " F2(y)) where y is Subset of F1() : P1[y] } c= F3() " (union { F2(x) where x is Subset of F1() : P1[x] } )
let x be object ; :: thesis: ( x in F3() " (union { F2(x) where x is Subset of F1() : P1[x] } ) implies x in union { (F3() " F2(y)) where y is Subset of F1() : P1[y] } )
assume A1: x in F3() " (union { F2(x) where x is Subset of F1() : P1[x] } ) ; :: thesis: x in union { (F3() " F2(y)) where y is Subset of F1() : P1[y] }
then A2: x in dom F3() by FUNCT_1:def 7;
F3() . x in union { F2(x) where x is Subset of F1() : P1[x] } by A1, FUNCT_1:def 7;
then consider y being set such that
A3: F3() . x in y and
A4: y in { F2(x) where x is Subset of F1() : P1[x] } by TARSKI:def 4;
consider a being Subset of F1() such that
A5: y = F2(a) and
A6: P1[a] by A4;
A7: x in F3() " F2(a) by A2, A3, A5, FUNCT_1:def 7;
F3() " F2(a) in { (F3() " F2(y)) where y is Subset of F1() : P1[y] } by A6;
hence x in union { (F3() " F2(y)) where y is Subset of F1() : P1[y] } by A7, TARSKI:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (F3() " F2(y)) where y is Subset of F1() : P1[y] } or x in F3() " (union { F2(x) where x is Subset of F1() : P1[x] } ) )
assume x in union { (F3() " F2(y)) where y is Subset of F1() : P1[y] } ; :: thesis: x in F3() " (union { F2(x) where x is Subset of F1() : P1[x] } )
then consider y being set such that
A8: x in y and
A9: y in { (F3() " F2(y)) where y is Subset of F1() : P1[y] } by TARSKI:def 4;
consider a being Subset of F1() such that
A10: y = F3() " F2(a) and
A11: P1[a] by A9;
A12: F3() . x in F2(a) by A8, A10, FUNCT_1:def 7;
F2(a) in { F2(x) where x is Subset of F1() : P1[x] } by A11;
then A13: F3() . x in union { F2(x) where x is Subset of F1() : P1[x] } by A12, TARSKI:def 4;
x in dom F3() by A8, A10, FUNCT_1:def 7;
hence x in F3() " (union { F2(x) where x is Subset of F1() : P1[x] } ) by A13, FUNCT_1:def 7; :: thesis: verum