Can we have a sequence of transitive sets $\langle\mathcal V_0, \mathcal V_1, \mathcal V_2,...\rangle$, all modeling $\sf ZF$, such that $\mathcal P(V_n) \subset \mathcal V_{n+1}$, and the cardinality of each is inaccessible from the cardinalities of the sets preceding it, and where choice fails inside each one of them, yet each successor set $\mathcal V_{n+1}$ proves choice externally over its predecessor $\mathcal V_n$?

Formal workup:

Add a primitive total unary function symbol $\mathcal V$ to the language of set theory; as a notation we shall write $\mathcal V(x)$ as $\mathcal V_x$. To all axioms of $\sf ZF$ [in language $\{=,\in\}$], add the following axioms:

**Restriction:** $\forall x: x \not \in \omega \to \mathcal V_x= \emptyset$

**Modeling:** if $\phi$ is an axiom of $\sf ZF\neg C$, then: $\forall n \in \omega: \phi^{\mathcal V_n}$

**Transitivity:** $\forall n \in \omega: \mathcal V_n \text { is transitive}$

**Power :** $\forall n \forall x: n \in \omega \land x \subseteq \mathcal V_n \to x \in \mathcal V_{n+1}$

**Inaccessibility:** $\forall n \in \omega: \operatorname {icc}( |\mathcal V_n |)$

**Choice:** $\forall n \in \omega: \forall x \in \mathcal V_n \exists f \in \mathcal V_{n+1}: \\\operatorname {dom}(f)=x \setminus \{\emptyset\} \land \forall m \, (f(m) \in m ) $

Where for every $\Phi$ set of sentences, $[\Phi]^X$ is the relativization of all quantifiers in elements of $\Phi$ to $X$; and $``\operatorname {icc..}\!\!"$ stands for *".. is inaccessible"*, $``| \ |\!\!"$ stands for cardinality defined after Scott's. This means that the cardinality of each $\mathcal V_n$ is not reachable by set unions and powering from below, i.e. it is strictly larger than the cardinality of any set union of a set of strictly smaller cardinality whose elements are of strictly smaller cardinalities, and it is strictly larger than the cardinality of the power set of any set of a strictly smaller cardinality.