defpred S1[ set ] means ex t9 being Element of F2() st
( t9 in F3() & $1 = F4(t9) & P1[$1,t9] );
set c = { F4(t9) where t9 is Element of F2() : t9 in F3() } ;
set c1 = { tt where tt is Element of F1() : S1[tt] } ;
A1:
{ tt where tt is Element of F1() : S1[tt] } c= { F4(t9) where t9 is Element of F2() : t9 in F3() }
proof
let x be
object ;
TARSKI:def 3 ( not x in { tt where tt is Element of F1() : S1[tt] } or x in { F4(t9) where t9 is Element of F2() : t9 in F3() } )
assume
x in { tt where tt is Element of F1() : S1[tt] }
;
x in { F4(t9) where t9 is Element of F2() : t9 in F3() }
then
ex
tt being
Element of
F1() st
(
x = tt & ex
t9 being
Element of
F2() st
(
t9 in F3() &
tt = F4(
t9) &
P1[
tt,
t9] ) )
;
hence
x in { F4(t9) where t9 is Element of F2() : t9 in F3() }
;
verum
end;
A2:
{ tt where tt is Element of F1() : S1[tt] } c= F1()
from FRAENKEL:sch 10();
A3:
F3() is finite
;
{ F4(t9) where t9 is Element of F2() : t9 in F3() } is finite
from FRAENKEL:sch 21(A3);
then reconsider c1 = { tt where tt is Element of F1() : S1[tt] } as Element of Fin F1() by A1, A2, FINSUB_1:def 5;
take
c1
; for t being Element of F1() holds
( t in c1 iff ex t9 being Element of F2() st
( t9 in F3() & t = F4(t9) & P1[t,t9] ) )
let t be Element of F1(); ( t in c1 iff ex t9 being Element of F2() st
( t9 in F3() & t = F4(t9) & P1[t,t9] ) )
( t in c1 implies ex tt being Element of F1() st
( t = tt & ex t9 being Element of F2() st
( t9 in F3() & tt = F4(t9) & P1[tt,t9] ) ) )
;
hence
( t in c1 iff ex t9 being Element of F2() st
( t9 in F3() & t = F4(t9) & P1[t,t9] ) )
; verum