# 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'.

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.
Let $$X=\bigcup_{n<\omega}\prod_{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 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.