set A = { a where a is Element of F1() : ( P1[a] & P2[a] ) } ;
set A1 = { a1 where a1 is Element of F1() : P1[a1] } ;
set A2 = { a2 where a2 is Element of F1() : P2[a2] } ;
thus
{ a where a is Element of F1() : ( P1[a] & P2[a] ) } c= { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] }
XBOOLE_0:def 10 { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } c= { a where a is Element of F1() : ( P1[a] & P2[a] ) } proof
let x be
object ;
TARSKI:def 3 ( not x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } or x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } )
assume
x in { a where a is Element of F1() : ( P1[a] & P2[a] ) }
;
x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] }
then consider a being
Element of
F1()
such that A1:
x = a
and A2:
(
P1[
a] &
P2[
a] )
;
(
a in { a1 where a1 is Element of F1() : P1[a1] } &
a in { a2 where a2 is Element of F1() : P2[a2] } )
by A2;
hence
x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] }
by A1, XBOOLE_0:def 4;
verum
end;
let x be object ; TARSKI:def 3 ( not x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } or x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } )
assume A3:
x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] }
; x in { a where a is Element of F1() : ( P1[a] & P2[a] ) }
then
x in { a2 where a2 is Element of F1() : P2[a2] }
by XBOOLE_0:def 4;
then A4:
ex a being Element of F1() st
( x = a & P2[a] )
;
x in { a1 where a1 is Element of F1() : P1[a1] }
by A3, XBOOLE_0:def 4;
then
ex a being Element of F1() st
( x = a & P1[a] )
;
hence
x in { a where a is Element of F1() : ( P1[a] & P2[a] ) }
by A4; verum