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\mathrm{\ne }0$, write $j_0=\sigma (p)$ and suppose $j_0\mathrm{\notin }K$; then every $k\in K$ satisfies $k\le j_0$ and $k\mathrm{\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\mathrm{\notin }\mathrm{span}(A)$. Then $A\cup \{w\}$ is linearly independent and $w\mathrm{\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 \mathrm{span}(A)$; and $\mathrm{span}(A)\subseteq U$ because $U$ is a linear subspace of $V$ containing $A$. So $\mathrm{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=\mathrm{\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=\mathrm{\varnothing }$ in step 3.1 is a linearly independent subset of $V$ with $A\approx n$ and $\mathrm{span}(A)=U$. If $U\mathrm{\ne }V$, pick $w\in V\setminus U=V\setminus \mathrm{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.