Is it provable from Zermelo–Fraenkel Set Theory, that if a countable set of sets exists, then this other countable set of sets exists?

Question

Zermelo–Fraenkel Set Theory is a system of axioms for describing set theory.

Suppose we assume the following:

For some set $B$ there exists a function $f_{1}$ subset of $(\mathbb{N} \times \mathcal{P}(B))$ such that for every $k \in \mathbb{N}$ $f_{1}(k)$ is a non-empty subset of $B$.
$\mathcal{P}(B)$ denotes the "power set" of $B$.

Can we then show that the following also exists?

$f_{2} = \{ (k, T) \text{ such that } k \in \mathbb{N} \text{ and } T = \{ (k, x): x \in f_{1}(k) \} \}$

Notice that we are not enumerating the elements of $f_{1}(k)$
The sets in question are not necessarily countable.
The numbering scheme for $f_{1}(k)$ is $1, 1, 1, 1, 1, 1, ...$ not $1, 2, 3, 4, 5, 6, ...$

BEGIN FORMAL CONJECTURE

If, for some set $B$, there exists a function $f_{1}$ subset of $(\mathbb{N} \times \mathcal{P}(B))$ such that for every $k \in \mathbb{N}$, $f_{1}(k)$ is a non-empty subset of $B$ then if $f_{2} = \{ (k, T) \text{ such that } k \in \mathbb{N} \text{ and } T = \{ (k, x): x \in f_{1}(k) \} \}$ and $\forall k \in \mathbb{N}, f_{2}(k) = \{ (k, x): x \in f_{1}(k) \}$ then all of the following are true:

• $f_{2}$ is well-defined
• $f_{2}$ exists
• $f_{2}$ is a function.

Note that $f_{2}$ is a subset of $\mathbb{N} \times (\mathbb{N} \times \mathcal{P}(B))$, so, we must also have $\mathbb{N} \times (\mathbb{N} \times \mathcal{P}(B))$ exists or is well-defined.

By "function" we mean that:

for all $k \in \mathbb{N}$ there exists $b \in B$ such that $(k, b) \in f$
and
for all $k \in \mathbb{N}$ and for all $b1, b2 \in B$ if $(k, b1) \in f$ and $(k, b2) \in f$ then $b1 = b2$

My question is, "Is my conjecture provable using only Zermelo–Fraenkel Set Theory (ZF) and basic logic?" The conjecture is obviously true, but is it provable in ZF?

END FORMAL CONJECTURE

BEGIN INFORMAL, INTUITIVE, SLOPPY, CONJECTURE

If we have a bunch of sets, $S(1), S(2), S(3)$, etc..., then we can make some new sets $T(1), T(2), T(3), ...$ with a very simple change: we take all of the elements of $S(1)$ and prefix them with the number $1$. For example,

• If "apple" was a set of $S(1)$ then $(1, ``\text{apple}")$ is an element of $T(1)$
• If $y$ was an element of set $S(2)$ then $(2, y)$ is an element of $T(2)$.
• If $z$ was an element of set $S(3)$ then $(3, z)$ is an element of $T(3)$.

END INFORMAL, INTUITIVE, SLOPPY, CONJECTURE

Answer 1

As it is now written, $f_2$ is functional; it's also injective. It obviously exists since it's a subset of $\mathbb{N}\times \mathcal{P}(\mathbb{N}\times B)$, which exists for any $B$; it's not clear what you mean by "well-defined", but if you mean whether there's such a thing as $f_2(k)$ for any $k$, then the answer is yes, regardless of whether $f_1(k)$ is non-empty or even defined.

First, functionality.

To see why it's functional, suppose that we had $(k,T)$ and $(k,S)$ both in $f_2$. Then by the definition of $f_2$, $T=\{(k,x)\;|\; x\in f_1(k)\}$; also by the definition of $f_2$, $S$ is the exact same set. That's really it, there's nothing else to prove.

To see that it's injective, suppose $f_2(k)=f_2(j)$. Then $$\{(k,x)\;|\;x\in f_1(k)\}\subseteq\{(j,y)\;|\;y\in f_1(j)\}$$ and vice versa. Since both are non-empty by our assumption on $f_1$, there is a $(k,x)$ that is identical to $(j,y)$ for some $y$; but then $k=j$. Hence injective.

To understand why it's defined, let's look at $T=\{(k,x)\;|\; x\in f_1(k)\}$ a little more closely. If $f_1(k)$ is defined and empty, then $T$ is simply empty; there are no pairs satisfying its defining condition. What if $f_1$ isn't defined at $k$? Just by expanding out definitions, one can see that $$T=\{(k,x)\;|\; \exists A((k,A)\in f_1\wedge x\in A)\}.$$ Given our assumption that $f_1$ isn't defined at $k$ (i.e. that no pair $(k,A)$ is in $f_1$), $T$ is simply empty again. So worst case scenario here is that $f_2=\mathbb{N}\times\{\varnothing\}$, which is indeed a function.

TL;DR, At no point is Choice even a useful axiom to apply, much less a necessary one.

By the way, you somewhat puzzlingly say the following in your conjecture:

. . . if $f_{2} = \{ (k, T) \text{ such that } k \in \mathbb{N} \text{ and } T = \{ (k, x): x \in f_{1}(k) \} \}$ and $\forall k \in \mathbb{N}, f_{2}(k) = \{ (k, x): x \in f_{1}(k) \}$ then . . .

The second part of this conjunction either begs the question of why you're writing a functional expression if you don't know if $f_2$ is a function, or it's entirely redundant because that's just what $f_2$'s definition already says in the first conjunct.