B: F₁() is finite ;
set Z = { F₃(w) where w is Element of F₁() : w in F₁() } ;
{ F₃(w) where w is Element of F₁() : w in F₁() } is finite from FRAENKEL:sch 21(B);
then reconsider Z = { F₃(w) where w is Element of F₁() : w in F₁() } as finite set ;
C: Z = { F₃(w) where w is Element of F₁() : w in F₁() } ;
D: card Z <= card F₁() from TREES_2:sch 3(C);
F₂() c= Z

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F₂() or x in Z )
assume x in F₂() ; :: thesis: x in Z
then ex w being Element of F₁() st
( x = F₃(w) & P₁[w] ) by A;
hence x in Z ; :: thesis: verum

end;

then card F₂() <= card Z by NAT_1:44;
hence card F₂() <= card F₁() by D, XXREAL_0:2; :: thesis: verum