Monotone convergence theorem by Fatou's lemma

I want to prove the monotone convergence theorem using Fatou's lemma (and its reverse) as exercise, and I need a check; I will use also the following properties of limit inferior and limit superior:

Let $f,g: D \to \mathbb{R}$ be functions. Then if $\lim_{x \to c} f(x)$ exists in $\tilde{\mathbb{R}}=\mathbb{R} \cup \{-\infty, + \infty \}$ we have $$\liminf_{x \to c} (f(x) +g(x))=\lim_{x \to c} f(x) + \liminf_{x \to c} g(x)$$ and the same for limit superior.

Statement. Let $(X, \mathcal{M}, \mu)$ be a measure space. Assume that $f_0 \le f_1 \le f_2 \le \dots$ is an increasing sequence of functions in $L^{+}(X)$ ($=$ the set of all extended real valued positive measurable functions), such that $f_n \uparrow f$ pointwise. Then $$ \int_X f = \lim_{n \to \infty} \int_X f_n $$

Proof. $g_n=(f-f_n)$ is a sequence of positive measurable functions, and then I can apply Fatou's lemma; it is $$\int_X \liminf_n (f-f_n) d\mu \le \liminf_n \int_X (f-f_n) d \mu$$Using the property above we have that $$\int_X \liminf_n (f-f_n) d\mu =\int_X (f - \liminf_n f_n) d \mu=0$$ and $$\liminf_n \int_X (f-f_n) d \mu=\liminf_n \left[ \int_X f d\mu - \int_X f_n d\mu \right]=\int_X f d \mu - \liminf_n \int_X f_n d \mu$$ So it is $$\int_X f d \mu \ge \liminf_n \int_X f_ d \mu \ge \int_X \liminf_n f_n d \mu=\int_X f d \mu$$using the lemma on $f_n$, which implies $$\int_X f d \mu = \liminf_n \int_X f_n d \mu$$Now: if $$\begin{split} \int_X f d \mu=\infty & \ \longrightarrow \ \underbrace{\liminf_n \int_X f_n d \mu}_{=\infty} \le \limsup_n \int_X f_n d \mu = \infty \\ & \ \longrightarrow \ \int_X f d \mu = \lim_n \int_X f_n d \mu = \infty \end{split}$$ and if $$\int_X f d \mu < \infty$$ We can apply, in a similar way as above, the reverse of Fatou's lemma considering that $f-f_n \le f - f_0$ and that $f-f_0$ is integrable ( - here I've used the fundamental hypothesis of $(f_n)_{n \in \mathbb{N}}$ increasing). We obtain $$ \int_X f d \mu=\limsup_n \int_X f_n d \mu $$and then the thesis.

What do you think about it?

Thank you very much.

I think your proof is basically fine, but it looks to me as if there are a few places where you were a bit careless.

$$\int_X \liminf_n (f-f_n) d\mu =\int_X (f - \liminf_n f_n) d \mu=0$$

While what you wrote here is all technically true, your choice of $\int (f - \liminf f_n)$ as the intermediary expression is unnatural because it suggests that you used the assertion $$\liminf (-a_n) = - \liminf a_n,$$ which is false in general. Instead, $$\liminf (-a_n) = -\boldsymbol\limsup a_n.$$ So in our case, it would be more straightforward to argue that $$\int \liminf(f - f_n) = \int(f - \limsup f_n) = \int(f-f) = 0.$$

$$\liminf_n \int_X (f-f_n) d \mu=\liminf_n \left[ \color{maroon}{\int_X f d\mu - \int_X f_n d\mu} \right] = \color{maroon}{\int_X f d \mu - \liminf_n \int_X f_n d \mu}$$

Aside from another potential mix-up of $\liminf$ and $\limsup$, note that the two highlighted expressions may not be well-defined because they could take the form $\infty - \infty$. You would need to prove more carefully that $$ \liminf \int (f - f_n) \geq 0 \implies \int f \geq \limsup \int f_n \geq \liminf \int f_n. $$

A cleaner approach was brought up by user1876508 in their comment. We have, using Fatou's lemma along the way, that $$ \int f = \int \liminf f_n \leq \liminf \int f_n \leq \limsup \int f_n. $$ For all $n$, we can deduce from $f_n \leq f$ that $\int f_n \leq \int f$. It follows that $$\limsup \int f_n \leq \int f.$$ Hence $\lim \int f_n$ exists and is equal to $\int f$.