If $\dim_F V = n$ and $U$ is a linear subspace of $V$, then $U$ is finite-dimensional, $\dim_F U \le n$, and $\dim_F U = n$ if and only if $U = V$

Fix a basis $B$ of $V$ with $B \approx n$. It spans $V$ and is finite of size $n$, so every linearly independent subset of $V$ is finite with at most $n$ elements.

A subset $A \subseteq U$ is linearly independent as a subset of $U$ exactly when it is linearly independent as a subset of $V$, and its span is the same set computed in either space; so "basis of $U$" is unambiguous, and every linearly independent subset of $U$ is a linearly independent subset of $V$.

A nonempty $K \subseteq \mathbb{N}$ with an upper bound has a greatest element. Let $M$ be the set of upper bounds of $K$ in $\mathbb{N}$, nonempty by hypothesis, and let $j_0$ be its least element. If $j_0 = 0$ then every $k \in K$ satisfies $k \le 0$, hence $k = 0$, and $K$ is nonempty, so $0 \in K$. If $j_0 \ne 0$, write $j_0 = \sigma(p)$ and suppose $j_0 \notin K$; then every $k \in K$ satisfies $k \le j_0$ and $k \ne j_0$, hence $k < \sigma(p)$, hence $k \le p$, so $p \in M$ with $p < j_0$, contradicting leastness. Either way $j_0 \in K$, and $j_0$ is an upper bound, so it is the greatest element of $K$.

Fix a linearly independent $A_0 \subseteq U$, possibly empty, and let $K := \{\, p \in \mathbb{N} : \text{some linearly independent } A \text{ with } A_0 \subseteq A \subseteq U \text{ has } A \approx p \,\}$. Then $K$ is nonempty: by step 1.2 the set $A_0$ is a linearly independent subset of $V$, so it is finite by step 1.1, say $A_0 \approx a_0$, and $A_0$ itself witnesses $a_0 \in K$. And every $p \in K$ satisfies $p \le n$, since the witnessing $A$ is likewise a linearly independent subset of $V$ and step 1.1 bounds its size, the size being unique. So $K$ is nonempty and bounded by $n$, and step 1.3 gives it a greatest element $d \le n$; fix a linearly independent $A$ with $A_0 \subseteq A \subseteq U$ and $A \approx d$.

That $A$ is a basis of $U$ containing $A_0$. Suppose some $w \in U$ had $w \notin \operatorname{span}(A)$. Then $A \cup \{w\}$ is linearly independent and $w \notin A$, and $A_0 \subseteq A \cup \{w\} \subseteq U$; moreover a bijection $d \to A$ extends to a bijection $\sigma(d) \to A \cup \{w\}$ by sending $d$ to $w$, so $A \cup \{w\} \approx \sigma(d)$ and $\sigma(d) \in K$, contradicting the maximality of $d$ in $K$. Hence $U \subseteq \operatorname{span}(A)$; and $\operatorname{span}(A) \subseteq U$ because $U$ is a linear subspace of $V$ containing $A$. So $\operatorname{span}(A) = U$ and $A$ is a basis of $U$ with $A_0 \subseteq A$.

Claim 1. Run steps 2.1 and 3.1 at $A_0 = \varnothing$, which is linearly independent and contained in $U$. They produce a basis $A$ of $U$ with $A \approx d$, so $U$ is finite-dimensional with $\dim_F U = d$, and $d \le n$ by step 2.1.

Claim 3. For an arbitrary linearly independent $A_0 \subseteq U$, steps 2.1 and 3.1 produce a basis $A$ of $U$ with $A_0 \subseteq A \subseteq U$, which is the assertion. Every selection made along the way is a single existential instantiation from a nonempty set, and the greatest element supplied by step 1.3 is determined by $K$ rather than chosen from it, so no choice principle is used. Applying this with $V$ in the roles of both $V$ and $U$, which is legitimate because $V$ is a linear subspace of itself, gives the statement for an arbitrary finite-dimensional vector space over $F$.

Claim 2. If $U = V$ then $\dim_F U = \dim_F V = n$. Conversely suppose $\dim_F U = n$; then $d = n$ by step 4.1, so the basis $A$ produced at $A_0 = \varnothing$ in step 3.1 is a linearly independent subset of $V$ with $A \approx n$ and $\operatorname{span}(A) = U$. If $U \ne V$, pick $w \in V \setminus U = V \setminus \operatorname{span}(A)$; then $A \cup \{w\}$ is a linearly independent subset of $V$ with $A \cup \{w\} \approx \sigma(n)$, and $\sigma(n) \le n$ by step 1.1, which is impossible since $n < \sigma(n)$. So $U = V$.

Claim 1 is step 4.1, claim 2 is step 5.1 and claim 3 is step 4.2.