Top-down proof of a lemma used in Schröder-Bernstein theorem Please have a check whether it is fine or contains any error! Thank you so much!
Lemma:

Suppose that $Z \subseteq Y \subseteq X$ and that $f:X \to Z$ is bijective, then there exists a bijection $g : X \to Y$.

Proof:

Without loss of generality, we assume $Y \subsetneq X$.
Let $\mathcal{F}=\{ V\subseteq X | (X-Y) \subseteq V \text{ and } f(V) \subseteq V \}$ and $A=\bigcap_{V\in \mathcal{F}}V$
1. $A \in \mathcal{F}$
$\forall V \in\mathcal{F}, X-Y\subseteq V\implies X-Y\subseteq \bigcap_{V\in\mathcal{F}}V\implies X-Y\subseteq A$.
$x\in A\implies \forall V \in\mathcal{F},x\in V \implies \forall V \in\mathcal{F},f(x)\in f(V)\subseteq V \implies \forall V\in\mathcal{F},f(x)\in V$ $\implies f(x)\in\bigcap_{V\in\mathcal{F}}V\implies f(x)\in A\implies f(A)\subseteq A$.
To sum up, $X-Y\subseteq A$ and $f(A)\subseteq A \implies A\in\mathcal{F}$. Furthermore, $\forall V\in \mathcal{F}: A \subseteq V\implies A$ is the minimal element of $\mathcal{F}$.
2. We prove $A \neq \varnothing$
$X-Y \subseteq X$ and $f(X)=Z \subseteq X \implies X \in \mathcal{F} \implies \mathcal{F} \neq \varnothing.$ As a result, $f(A) \subseteq A$ and $(X-Y) \subseteq A$.
$\mathcal{F} \neq \varnothing$ and $\forall V \in \mathcal{F}, (X-Y) \subseteq V \implies (X-Y) \subseteq \bigcap_{V\in \mathcal{F}}V \implies (X-Y) \subseteq A \implies$ $A \neq \varnothing.$
3. We prove $f(A)=A \cap Y$ (Here I figure out two ways to prove this and I present both of them)
a. Approach 1
Let $B=f(A) \cup (X-Y)$
$f(A) \subseteq A$ and $(X-Y) \subseteq A \implies B \subseteq A$.
$f(A) \subseteq A \implies f(f(A)) \subseteq f(A)$; $(X-Y) \subseteq A \implies f(X-Y) \subseteq f(A)$.
First, $B=f(A) \cup (X-Y) \implies (X-Y) \subseteq B$.
Second, $f(B)=f(f(A) \cup (X-Y))=f(f(A)) \cup f(X-Y) \subseteq f(A) \subseteq B.$
Finally, $(X-Y) \subseteq B$ and $f(B) \subseteq B \implies B \in \mathcal{F},$ but $B \subseteq A$. From the minimality of $A$, $B=A$.
$A \cap Y=B \cap Y= (f(A) \cup (X-Y)) \cap Y=(f(A) \cap Y) \cup ((X-Y) \cap Y)=f(A) \cup \varnothing = f(A)$.
b. Approach 2
$f(A) \subseteq A$ and $f(A) \subseteq Z \subseteq Y \implies f(A) \subseteq (A \cap Y)$.
Assume $(A\cap Y) \not\subseteq f(A) \implies \exists p\in (A\cap Y)$ such that $p \notin f(A) \implies p \in Y$.
Let $B=A-\{p\}$.
First, $p \in Y \wedge (X-Y) \subseteq A \implies X-Y \subseteq A-\{p\} \implies (X-Y) \subseteq B$.
Second, $f(B)=f(A-\{p\})=f(A)-f(\{p\})$ [Since $f$ is injective] $\subseteq f(A) \subseteq f(A)-\{p\}$ [Since $p \notin f(A)$] $\subseteq A-\{p\}$ [Since $f(A) \subseteq A$]$=B$.
To sum up, we have $(X-Y) \subseteq B$ and $f(B)\subseteq B$, then $B \in \mathcal{F}$, but $B \subsetneq A$. This contradicts to the minimality of $A \implies (A \cap Y) \subseteq f(A)$.
$f(A) \subseteq (A \cap Y)$ and $A \cap Y \subseteq f(A) \implies A \cap Y=f(A)$.
4. $f(A) \cup (X-A)=Y$ and $f(A) \cap (X-A)=\varnothing$
$X-Y \subseteq A \implies X-A \subseteq X-(X-Y)=Y$.
$f(A) \cup (X-A)=(A \cap Y)\cup (X-A)=(A\cup (X-A)\cap (Y\cup (X-A))=X\cap (Y\cup (X-A))=Y\cup (X-A) \subseteq Y \cup Y=Y \implies f(A) \cup (X-A)=Y$.
$f(A) \cap (X-A)=(A \cap Y) \cap (X-A)=Y \cap (A \cap (X-A))=Y \cap \varnothing=\varnothing.$
5. We generate $g$ as follows
$$
g(x) =
\begin{cases}
\ f(x)      & \text {if $x \in A$} \\
x   & \text {if $x \in X \setminus A$} \\
\end{cases}
$$

 A: I see that you have already followed a reference in the comments to a proof of the S-B theorem. Still, here are my comments on your first part. You might find them instructive to compare with any new proof.

Let $\mathcal{F}=\{ V\subseteq X | (X-Y) \subseteq V \text{ and } f(V) \subseteq V \}$ and $A=\bigcap_{V\in \mathcal{F}}V$
From the definition of $A$, we have that $A \in \mathcal{F}$ and that $\forall V\in \mathcal{F}, A \subseteq V$, or equivalently $A$ is the minimal element of $\mathcal{F}$.

Do you think that you have already proven $A \in \mathcal{F}$ at this step, or are you proving that in Part 1? If the former, I do not see how it follows from the definition of $A$. If $x$ is an arbitrary element in $A$, why is $f(x) \in A$?

1. We prove $A \neq \varnothing$

Your rough idea seems to be to show that $A \in \mathcal{F}$, since that would imply $\varnothing \neq X - Y \subseteq A$. This would work.

$X-Y \subseteq X$ and $f(X)=Z \subseteq X \implies X \in \mathcal{F} \implies \mathcal{F} \neq \varnothing.$

This seems correct. You establish that $X$ itself is an element of $\mathcal{F}$, so $\mathcal{F}$ cannot be empty.

As a result, $f(A) \subseteq A$

For an arbitrary $x \in A$, thus far you have only justified $x \in X$. How do you conclude that $f(x) \in A$? (You have claimed that $A \in \mathcal{F}$, but I do not see why that is yet.)

and $(X-Y) \subseteq A$.

This seems correct, since $X - Y \subseteq V$ for all $V \in \mathcal{F}$.

$\mathcal{F} \neq \varnothing$ and $\forall V \in \mathcal{F}, (X-Y) \subseteq V \implies (X-Y) \subseteq \bigcap_{V\in \mathcal{F}}V \implies (X-Y) \subseteq A \implies$ $A \neq \varnothing.$

You might more simply state $\varnothing \neq X - Y \subseteq A$, but I'm still not sure why $A \in \mathcal{F}$.
I suspect that your ideas are correct, but more detail would further illuminate them.
Edit: Per the additional info in the comments, your first step seems correct. After looking over your second part (specifically approach b), it looks correct as well, including your proof by contradiction.
