Natural deduction from non-first-order premises

Solution 1:

As Mauro said, you did not express "$A$ is finite" in a logical form. So how would it be possible to do anything with it? Suppose you use this Fitch-style system. Then the simplest way to express it would be as follows.

Given any set $A$, define $A$ to be finite iff:
  $∃c{∈}ℕ\ ∃f{∈}FN(ℕ_{<c},A)\ ∀x{∈}A\ ∃k{∈}ℕ_{<c}\ ( \ f(k)=x \ )$.

In English, $A$ is finite iff there is some $c{∈}ℕ$ and some surjection from $ℕ_{<c}$ onto $A$. Here $ℕ_{<c}$ is defined as $\{ k : k{∈}ℕ ∧ k<c \}$. If you want to minimize set theory, you can use the following alternative (which is equivalent over set theory).

Given any set $A$, define $A$ to be finite iff:
  $∃c{∈}ℕ\ ∃f{∈}FN(ℕ,A)\ ∀x{∈}A\ ∃k{∈}ℕ\ ( \ k<c \land f(k)=x \ )$.

You are correct that you cannot automatically swap the quantifiers. To prove your desired theorem, you would need the induction rule (see under "Set Theory" in the linked post). See if you can find a proof!