What does this ZF+[AOC-Lite] Look Like? We use the notation $[n] = \{0,1,2,3,\cdots ,n-1 \}$.
Remove AOC completly from ZFC and then replace it with
Axiom asdf: Let $X$ be any nonempty set such that
$\;\text{For every injective } f:[n]\to X$
$\;\;\; \text{ there exist an injective}\, g:[n+1]\to X \text{ such that } g(k) = f(k) \text{ for } k \le n-1$
Then if $h :[n] \to X$ is any injective function there exist an injective $\hat h: \mathbb N \to X$ such that $\hat h(k) = h(k) \text{ for } k \le n-1$.
Question: Is this equivalent to adding the Axiom of Choice from a 'Countable Family of Finite Sets' to ZF?
Axiom AOC.CFFS/ f̶d̶s̶a̶: If ${\displaystyle (S_{i })_{\,i \in \mathbb N}}$ is a family of non-empty finite sets indexed by the natural numbers, then
$\;{\displaystyle \prod _{i \in \mathbb N}S_{i }\neq \emptyset }$.

Note: I am an amateur set theorist fiddling around in these areas. I would like to show my reserach effort but this is more of an 'intuitive thing'.
Any answers will be appreciated.
 A: What you call "asdf" is really just a formulation of "Every Dedekind-finite set is finite" (or "every infinite set is Dedekind-infinite"). What you call "fdsa" is just countable choice for families of finite sets.
To see the first statement I made is true, note that $X$ is infinite if and only if it has a subset of size $n$ for any $n<\omega$. And every set of size $n$ is really just the range of an injective function from $[n]$, and so it can be extended to a set of size $n+1$ by tucking on a new element. So your "asdf" axiom just states that every finite subset can be extended to a countable subset.
And so the implication you need follows in the following method:
Let $X=\bigcup_{n<\omega}\prod_{k<n}S_k$, namely all the initial approximations of a choice function. Then this set has a countable subset now, say $\{s_n\mid n<\omega\}$. But since each $S_k$ is finite, $\prod_{k<n}S_k$ is finite for all $n$, so for every $m$ there is some $n>m$ such that $s_n$, from our countable set, has $m$ in its domain.
Define a choice function $s$ as follows: $s(k)=s_n(k)$ where $n$ is the least index for which $s_n(k)$ is defined. Therefore $\prod_{n<\omega}S_n$ is non-empty.
