A topological dynamical system is a topological space $X$ together with a continuous function $f : \ X \to X$. In the following, I will assume that $X$ is compact and Hausdorff (in other words, I work with compact topological dynamical systems).
Let $(X, f)$ be a compact topological dynamical system. A subset $A \subset X$ is said to induce a sub-system if it is non-empty, closed and $f$-invariant. Then $(A,f)$ is called a sub-system.
A sub-system $(A,f)$ is called minimal is it has no proper sub-system.
Now, a theorem by Birkhoff asserts that any compact topological dynamical system admits a minimal sub-system. The short and easy proof goes like this:
Proof
Let $\mathcal{M}$ be the set of sub-systems of $(X,f)$. This set is non-empty, as it contains $(X,f)$. The set $\mathcal{M}$ is ordered by inclusion: we write that $(A,f) \subset (A',f)$ whenever $A \subset A'$. Finally, any totally ordered subset $\{(A_i, f)\}$ of $\mathcal{M}$ has a minimal element, namely, $(\bigcap_i A_i,f)$ (which is non-empty, as a decreasing intersection of non-empty compact spaces is non-empty, closed, and $f$-invariant).
By Zorn's Lemma, $\mathcal{M}$ has minimal elements, which are minimal systems $\square$
This proof is somewhat unpalatable for me, as it uses the Axiom of Choice (which I find unintuitive when used in topology). I've seen mentioned that there exists a more technical proof which does not use the Axiom of Choice (but probably still uses the Axiom of Dependent Choice). Where may I find it (or, if the proof is short enough, what does it look like)?
Almost ten years later, I can give an answer to this question. I formalized what follows in Lean last year. As I suspected, we can weaken work with a weaker version of choice under an additional separability assumption. The proof is more technical, but I think gives more insight into the problem.
Theorem
Let $X$ be a second-countable compact topological space (i.e. a compact metrizable space) and $f \in \mathcal{C} (X, X)$. Under the axiom of dependent choice, $(X, f)$ has a minimal subsystem.
Proof
Since $X$ is secound-countable, let $(U_n)_{n \in \mathbb{N}}$ be a countable open basis of its topology. Given an open set $U$, we denote by $\text{Orb}(U)$ the set of points whose orbit visit $U$, i.e. the pre-orbit of $U$:
$$\text{Orb}(U) = \bigcup_{n \in \mathbb{N}} f^{-n} (U).$$
By continuity of $f$, the set $\text{Orb}(U)$ is also open. The set $\text{Orb}(U)$ is not $f$-invariant, but $\text{Orb}(U)^c$ is a closed (thus compact) invariant subset of $X$.
Now, define recursively a sequence $(K_n)_{n \in \mathbb{N}}$ of compact subsets of $X$ by setting $K_0 = X$ and, for all $n \geq 0$,
if $K_n \subset \text{Orb}(U_n)$, then $K_{n+1} := K_n$;
otherwise, $K_{n+1} := K_n \cap \text{Orb}(U_n)^c$.
The main idea is that the subsets $\text{Orb}(U_n)^c$ are a family of compact invariant subsets, and we take intersections as needed to obtain smaller and smaller compact invariant subsets.
Let $K := \bigcap_{n \in \mathbb{N}} K_n$. Then $K$ is a nonempty compact subset as a nonincreasing intersection of nonempty compact subsets, and invariant as an intersection of invariant subsets. All is left is to prove that $K$ is minimal, that is, it contains no smaller nonempty compact invariant subset.
Let $K' \subset K$ be a nonempty compact invariant subset. Assume that $K'$ is strictly smaller than $K$. Then, there exists $k \in \mathbb{N}$ such that $U_k \cap K'$ is empty and $U_k \cap K$ is nonempty (take for instance a small enough neighbourhood of a point $x \in K \setminus K'$).
Since $K'$ is invariant, for all $x \in K'$ and $n \geq 0$, we have $f^n (x) \in K'$, whence $f^n(x) \notin U_k$. Hence, $K' \subset \text{Orb}(U_k)^c$.
But then, $K' \cap \text{Orb}(U_k)^c \subset K \cap \text{Orb}(U_k)^c \subset K_k \cap \text{Orb}(U_k)^c$ is nonempty. By the recursive definition of the sequence $(K_n)_{n \in \mathbb{N}}$, we get $K_{k+1} = K_k \cap \text{Orb}(U_k)^c$, so that $K \subset K_{k+1} \subset \text{Orb}(U_k)^c$. This contradicts the assumption that $U_k \cap K$ is nonempty.
Hence, $K$ contains no smaller invariant compact subset, and is thus minimal.