Proving preservation under substitution System F Omega
Throughout $y$ should have type $T_1$ instead of $T_2$.

Let us be more careful about step 3. We are going to apply the following induction hypothesis:


  If $\Gamma, y : T_1, x : S \vdash t_1 : T_2$ and $\Gamma, y : T_1 \vdash s : S$ then $\Gamma, y : T_1 \vdash [x \mapsto s] t_1 : T_2$.


After that we will use abstraction to get $\Gamma \vdash (\lambda y : T_1 . [x \mapsto s] t_1) : T_2$, and finish the proof by observing that $(\lambda y : T_1 . [x \mapsto s] t_1) = [x \mapsto s](\lambda y : T_1 . t_1)$.

So let us make sure that the induction hypothesis is applicable:


First we need $\Gamma, y : T_1, x : S \vdash t_1 : T_2$: because $\Gamma, x : S \vdash (\lambda y : T_1 . t_1) : T_1 \to T_2$ by inversion we obtain $\Gamma, x : S, y : T_1 \vdash t_1 : T_2$ and then we use exchange to get $\Gamma, y : T_1, x : S \vdash t_1 : T_2$. This is your step 1. (The exchange is valid because types are non-dependent in this argument.)
Second, we need $\Gamma, y : T_1 \vdash s : S$: we already have $\Gamma \vdash s : S$. By weakening we obtain $\Gamma, y : T_1 \vdash s : S$, this is your step 2.


Supplemental: It seems unclear how induction works. To perform a proof by induction we need to specify what the induction is on. In this case the induction is on the derivation of $\Gamma, x : S \vdash t  : T$. Thus, we have to look at all the possible cases of deriving $\Gamma, x : S \vdash t  : T$. Each inference rule gives us one case, and we've just discussed the case of $\lambda$-abstraction. Each case has its own induction hypotheses, one for each premise of the rule.

Let me give you a simpler example. Suppose we only had the following typing rules:


Variables: $$\frac{(x : T) \in \Gamma}{\Gamma \vdash x : T}$$
Pairs: $$\frac{\Gamma \vdash e_1 : T_1 \qquad \Gamma \vdash e_2 : T_2}{\Gamma \vdash (e_1, e_2) : T_1 \times T_2}$$
First projection: $$\frac{\Gamma \vdash e : T_1 \times T_2}{\Gamma \vdash \mathsf{fst}\,e : T_1}$$


A derivation is a finite tree built from these rules (if you are not clear about that, you should first understand what a derivation is). Suppose we want to show that every derivable judgement has some given property $\phi$. To prove this by induction on the derivation, we need to show three things:


Variable case: if $(x : T) \in \Gamma$ then $\Gamma \vdash x : T$ has property $\phi$.
Pair case: if $\Gamma \vdash e_1 : T_1$ has property $\phi$ and $\Gamma \vdash e_2 : T_2$ has property $\phi$ then $\Gamma \vdash (e_1, e_2) : T_1 \times T_2$ has property $\phi$.
First projection case: if $\Gamma \vdash e : T_1 \times T_2$ has property $\phi$ then $\Gamma \vdash \mathsf{fst}\, e : T_1$ has property $\phi$.


The first case has no induction hypothesis, it is a base case. This is so because the corresponding inference rule has no premises (only the side condition $(x : T) \in \Gamma$). The second case has two induction hypotheses, namely that $\Gamma \vdash e_1 : T_1$ has property $\phi$ and that $\Gamma \vdash e_2 : T_2$ has property $\phi$. This is so because the corresponding inference rules has these two premises. The third case has one induction hypothesis, and you should be able to see why that is if you understood what I am saying.