Suppose that $Y \subseteq X$ and that $f:X \to Y$ is injective. Then there is a bijection from $X$ to $Y$.
My attempt:
For $B\subseteq X$, $B$ is closed $\iff$ $f[B]\subseteq B$.
The closure of $A$, to be denoted by $\overline A$, is the least closed set that contains all elements of $A$ and thus defined by $\overline A=\bigcap\{B\in\mathcal P(X)\mid A\subseteq B \text{ and }B \text{ is closed}\}$.
Let $A=X\setminus Y$. We first prove that $f[\overline A]\cup A=\overline A$.
- $(f[\overline A]\cup A) \subseteq \overline A$
$\overline A$ is closed $\implies$ $f[\overline A] \subseteq \overline A$. Moreover, $\overline A$ is the closure of $A \implies A \subseteq \overline A$. Thus $(f[\overline A]\cup A) \subseteq \overline A$.
- $\overline A\subseteq (f[\overline A]\cup A)$
For $a\in \overline A$, there are only two cases.
If $a\in A$, then it follows immediately that $a\in f[\overline A]\cup A$.
If $a\notin A$, then assume the contrary that $a\notin f[\overline A]\cup A$, then $a\notin f[\overline A]$. Let $A'=\overline A \setminus \{a\}$. Since $a\notin A$, $A\subseteq A'$. We have $f[A']=f[\overline A \setminus \{a\}]=f[\overline A] \setminus \{f(a)\}$ since $f$ is injective. Since $a\notin f[\overline A]$, $f[\overline A] \setminus \{a\}=f[\overline A]$. Thus $f[A']=(f[\overline A] \setminus \{a\}) \setminus \{f(a)\} \subseteq (\overline A \setminus \{a\}) \setminus \{f(a)\} \subseteq \overline A \setminus \{a\}$. Hence $f[A'] \subseteq A'$ and consequently $A'$ is closed. To sum up, $A\subseteq A'$ and $A'$ is closed $\implies \overline A \subseteq A' \implies \overline A \subseteq (\overline A \setminus \{a\})$. This is clearly a contradiction. Hence $a\in f[\overline A]\cup A$. It follows that $\overline A\subseteq (f[\overline A]\cup A)$.
As a result, $A = f[\overline A]\cup A$. Next we prove $X\setminus \overline A= Y\setminus f[\overline A]$.
$X\setminus \overline A=X\setminus (f[\overline A]\cup A)=(X\setminus f[\overline A])\cap(X\setminus A)=(X\setminus f[\overline A])\cap Y=Y\setminus f[\overline A]$ since $Y\subseteq X$.
We define a bijection $g:X\to Y$ by $g=f_{\restriction \overline A} \cup \operatorname{id}_{X\setminus \overline A}$.
Does this proof look fine or contain gaps? Do you have suggestions? Many thanks for your dedicated help!
Yes, your proof is perfectly correct.
There are just two typos (that I noticed): your final string of equations should end in $Y \setminus f[\overline{A}]$, and in the middle of your paragraph you use the expression $\overline{A}\setminus \{a\}A'$, where you accidentally add $A'$.
For formatting it would help if you put some of the longer strings of equations/inclusions in displays. Also, the proof of (2) doesn't need two cases: you can go straight to "Assume towards a contradiction that $a \notin f[\overline{A}] \cup A$, so that $a \notin A$ and $a \notin f[\overline{A}]$", because that is what you do in the second case anyway.