defpred S_{1}[ set ] means ex t9 being Element of F_{2}() st

( t9 in F_{3}() & $1 = F_{4}(t9) & P_{1}[$1,t9] );

set c = { F_{4}(t9) where t9 is Element of F_{2}() : t9 in F_{3}() } ;

set c1 = { tt where tt is Element of F_{1}() : S_{1}[tt] } ;

A1: { tt where tt is Element of F_{1}() : S_{1}[tt] } c= { F_{4}(t9) where t9 is Element of F_{2}() : t9 in F_{3}() }
_{1}() : S_{1}[tt] } c= F_{1}()
from FRAENKEL:sch 10();

A3: F_{3}() is finite
;

{ F_{4}(t9) where t9 is Element of F_{2}() : t9 in F_{3}() } is finite
from FRAENKEL:sch 21(A3);

then reconsider c1 = { tt where tt is Element of F_{1}() : S_{1}[tt] } as Element of Fin F_{1}() by A1, A2, FINSUB_1:def 5;

take c1 ; :: thesis: for t being Element of F_{1}() holds

( t in c1 iff ex t9 being Element of F_{2}() st

( t9 in F_{3}() & t = F_{4}(t9) & P_{1}[t,t9] ) )

let t be Element of F_{1}(); :: thesis: ( t in c1 iff ex t9 being Element of F_{2}() st

( t9 in F_{3}() & t = F_{4}(t9) & P_{1}[t,t9] ) )

( t in c1 implies ex tt being Element of F_{1}() st

( t = tt & ex t9 being Element of F_{2}() st

( t9 in F_{3}() & tt = F_{4}(t9) & P_{1}[tt,t9] ) ) )
;

hence ( t in c1 iff ex t9 being Element of F_{2}() st

( t9 in F_{3}() & t = F_{4}(t9) & P_{1}[t,t9] ) )
; :: thesis: verum

( t9 in F

set c = { F

set c1 = { tt where tt is Element of F

A1: { tt where tt is Element of F

proof

A2:
{ tt where tt is Element of F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { tt where tt is Element of F_{1}() : S_{1}[tt] } or x in { F_{4}(t9) where t9 is Element of F_{2}() : t9 in F_{3}() } )

assume x in { tt where tt is Element of F_{1}() : S_{1}[tt] }
; :: thesis: x in { F_{4}(t9) where t9 is Element of F_{2}() : t9 in F_{3}() }

then ex tt being Element of F_{1}() st

( x = tt & ex t9 being Element of F_{2}() st

( t9 in F_{3}() & tt = F_{4}(t9) & P_{1}[tt,t9] ) )
;

hence x in { F_{4}(t9) where t9 is Element of F_{2}() : t9 in F_{3}() }
; :: thesis: verum

end;assume x in { tt where tt is Element of F

then ex tt being Element of F

( x = tt & ex t9 being Element of F

( t9 in F

hence x in { F

A3: F

{ F

then reconsider c1 = { tt where tt is Element of F

take c1 ; :: thesis: for t being Element of F

( t in c1 iff ex t9 being Element of F

( t9 in F

let t be Element of F

( t9 in F

( t in c1 implies ex tt being Element of F

( t = tt & ex t9 being Element of F

( t9 in F

hence ( t in c1 iff ex t9 being Element of F

( t9 in F