How do i prove that a subset of a finite subset is finite? Let $n\in\omega$ and $F\subset n$.
How do i prove that $F$ is finite?
I know that this can be proven by constructing a function in a following way: take $f(0)$ as the least element of $F$ and then take $f(1)$ as the least element of $F\setminus \{f(0)\}$ and continue this process. Since $F\subset n$, $F$ has a maximal element. Thus this process must be done in a finite step.
However, i don't know how to prove this precisely. How do i write down "this process must be done in a finite step" in first-order logic and so on. Please help :)
 A: When we write something in the flavor of "the process must be done in a finite number of steps", what we often mean to say is that we are hiding some inductive construction, and that induction cannot proceed through all the natural numbers.
That is, we define some construction $\varphi(n)$ by recursion. We have $\varphi(0)$ defined somehow, and then given $\varphi(k)$ we have some pool of available resources, which "shrinks" from each steps, and if it hasn't dried out we do something nontrivial to define $\varphi(k+1)$.
So when we say that the process can only go through a finite number of steps, we mean to say that the pool is necessarily shrinking from time to time, and that the pool is finite (or necessarily becomes finite at some step), so that shrinkage is bound to stabilize and the recursive definition becomes trivialized (i.e. $\varphi(k+1)=\varphi(k)$).
In the case of proving that a subset of a finite set is finite, we define some bijection between a subset and a finite ordinal; we begin by ordering the finite set, then our construction is a function from the subset to some other finite ordinal, and the recursion does exactly that. It picks "the next element", but since there are finitely many elements in the larger set, the recursion must trivialize at some finite point.

As a whole, this sort of sentence is tricky, and you have to gain a lot of experience before you can use it without [too many] mistakes. Until such time, my suggestion is to try and understand what is it that you define, and how the induction and recursion methods are applied in this sort of claim. Then you can write them explicitly.
After some time, your brain will do that automatically and you can resort to "this is a finite process, so it must terminate." again.
