# Can we have this sequence where choice fails and returns?

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.

Start with countably many inaccessible cardinals, $$\kappa_n$$, and now take the full support product adding $$\kappa_n^+$$ subsets to each $$\kappa_n$$. Then the $$n$$th model is the symmetric extension given by adding all the generics for the first $$n-1$$ coordinates, and violating choice in the $$n$$th one (e.g. a Cohen style model).