per cases ( F₁() = {} or F₁() <> {} ) ;

suppose A3: F₁() = {} ; :: thesis: { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite

now

consider a being Element of { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } ;
assume { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } <> {} ; :: thesis: contradiction
then a in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } ;
then ex d being Element of F₂() st
( a = F₃(d) & F₄(d) in F₁() ) ;
hence contradiction by A3; :: thesis: verum

end;

hence { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite ; :: thesis: verum

end;

suppose F₁() <> {} ; :: thesis: { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite

then reconsider D = F₁() as non empty set ;
defpred S₁[ set ] means ex d being Element of F₂() st $1 = F₄(d);
set B = { d where d is Element of F₂() : F₄(d) in D } ;
set C = { a where a is Element of D : S₁[a] } ;
{ a where a is Element of D : S₁[a] } is Subset of D from DOMAIN_1:sch 7();
then A4: { a where a is Element of D : S₁[a] } is finite by A1, FINSET_1:13;
{ a where a is Element of D : S₁[a] } ,{ d where d is Element of F₂() : F₄(d) in D } are_equipotent

proof

take Z = { [F₄(d),d] where d is Element of F₂() : verum } ; :: according to TARSKI:def 6 :: thesis: ( ( for b₁ being set holds
( not b₁ in { a where a is Element of D : S₁[a] } or ex b₂ being set st
( b₂ in { d where d is Element of F₂() : F₄(d) in D } & [b₁,b₂] in Z ) ) ) & ( for b₁ being set holds
( not b₁ in { d where d is Element of F₂() : F₄(d) in D } or ex b₂ being set st
( b₂ in { a where a is Element of D : S₁[a] } & [b₂,b₁] in Z ) ) ) & ( for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in Z or not [b₃,b₄] in Z or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

hereby :: thesis: ( ( for b₁ being set holds
( not b₁ in { d where d is Element of F₂() : F₄(d) in D } or ex b₂ being set st
( b₂ in { a where a is Element of D : S₁[a] } & [b₂,b₁] in Z ) ) ) & ( for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in Z or not [b₃,b₄] in Z or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

let x be set ; :: thesis: ( x in { a where a is Element of D : S₁[a] } implies ex d being set st
( d in { d where d is Element of F₂() : F₄(d) in D } & [x,d] in Z ) )
assume x in { a where a is Element of D : S₁[a] } ; :: thesis: ex d being set st
( d in { d where d is Element of F₂() : F₄(d) in D } & [x,d] in Z )
then consider a being Element of D such that
A5: ( a = x & ex d being Element of F₂() st a = F₄(d) ) ;
consider d being Element of F₂() such that
A6: a = F₄(d) by A5;
reconsider d = d as set ;
take d = d; :: thesis: ( d in { d where d is Element of F₂() : F₄(d) in D } & [x,d] in Z )
thus ( d in { d where d is Element of F₂() : F₄(d) in D } & [x,d] in Z ) by A5, A6; :: thesis: verum

end;

hereby :: thesis: for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in Z or not [b₃,b₄] in Z or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) )

let y be set ; :: thesis: ( y in { d where d is Element of F₂() : F₄(d) in D } implies ex x being set st
( x in { a where a is Element of D : S₁[a] } & [x,y] in Z ) )
assume y in { d where d is Element of F₂() : F₄(d) in D } ; :: thesis: ex x being set st
( x in { a where a is Element of D : S₁[a] } & [x,y] in Z )
then consider d being Element of F₂() such that
A7: ( d = y & F₄(d) in D ) ;
reconsider x = F₄(d) as set ;
take x = x; :: thesis: ( x in { a where a is Element of D : S₁[a] } & [x,y] in Z )
thus ( x in { a where a is Element of D : S₁[a] } & [x,y] in Z ) by A7; :: thesis: verum

end;

let x, y, z, u be set ; :: thesis: ( not [x,y] in Z or not [z,u] in Z or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
assume [x,y] in Z ; :: thesis: ( not [z,u] in Z or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
then consider d1 being Element of F₂() such that
A8: [x,y] = [F₄(d1),d1] ;
assume [z,u] in Z ; :: thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )
then consider d2 being Element of F₂() such that
A9: [z,u] = [F₄(d2),d2] ;
A10: ( x = F₄(d1) & y = d1 ) by A8, ZFMISC_1:33;
( z = F₄(d2) & u = d2 ) by A9, ZFMISC_1:33;
hence ( ( not x = z or y = u ) & ( not y = u or x = z ) ) by A2, A10; :: thesis: verum

end;

then A11: { d where d is Element of F₂() : F₄(d) in D } is finite by A4, CARD_1:68;
A12: { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } is finite from FRAENKEL:sch 21(A11);
{ F₃(d) where d is Element of F₂() : F₄(d) in F₁() } = { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } }

proof

thus { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } c= { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } :: according to XBOOLE_0:def 10 :: thesis: { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } c= { F₃(d) where d is Element of F₂() : F₄(d) in F₁() }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } or x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } )
assume x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } ; :: thesis: x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } }
then consider d' being Element of F₂() such that
A13: ( x = F₃(d') & F₄(d') in F₁() ) ;
( x = F₃(d') & d' in { d where d is Element of F₂() : F₄(d) in D } ) by A13;
hence x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } or x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } )
assume x in { F₃(d) where d is Element of F₂() : d in { d where d is Element of F₂() : F₄(d) in D } } ; :: thesis: x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() }
then consider d1 being Element of F₂() such that
A14: ( x = F₃(d1) & d1 in { d where d is Element of F₂() : F₄(d) in D } ) ;
ex d3 being Element of F₂() st
( d3 = d1 & F₄(d3) in D ) by A14;
hence x in { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } by A14; :: thesis: verum

end;

hence { F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite by A12; :: thesis: verum

end;

end;