Can Z + Ranks + Successor cardinals + Ordinal inaccessibility be equal to ZF? [EDIT: The axiom of successor cardinals was found by an answer by Greg Kirmayer, not to be capturing the intended meaning of it, which is simply reflected by its name, i.e. the existence of a successor cardinal for every cardinal. A corrective note had been inserted below that axiom.
Is Z + Rank + Successor cardinals + Ordinal inaccessibility = ZF?
Where:
Ranks: $\forall x \exists \alpha: x \in V_\alpha$
where $V_\alpha$ is the $\alpha^{th}$ stage of Von Neumann's universe (the cumulative hierarchy).
Successor cardinals:  if $f$ is a definable function, then: $$\forall \text{ordinal } \alpha \ \exists \text{ ordinal }\beta \, (\neg \forall \gamma < \beta \exists \lambda < \alpha : f(\lambda)=\gamma)$$ By $\text{ordinal}$ it means a von Neumann ordinal defined in the usual manner.
For every ordinal there is an ordinal such that no surjective function (definable in the language of set theory) from the former to the latter can exist.
[NOTE]: The above formulation suffers a flaw, therefore the correct formulation is: $$\forall \text{ordinal } \alpha \, \exists \text{ordinal } \beta: \not \exists f (f: \beta \hookrightarrow \alpha)$$, where $\hookrightarrow$ signify "injective function".
Ordinal inaccessibility: if $f$ is a definable function, then: $$ \forall \gamma \, (\neg \forall \text{ ordinal } \alpha \,\exists \beta < \gamma : \alpha \leq f(\beta))$$ Any function [definable in the language of set theory] coming from an ordinal cannot have every ordinal being smaller than or equal to some ordinal in its range. That is, its range cannot be a cofinal subclass of the class of all ordinals.
The idea is that every uncountable cardinal in ZF is either Regular and therefore a successor cardinal, or otherwise a singular limit cardinal. Here, both of those kinds would be constructed from below, and the axiom of Rank assures that all sets are built successively within those ordinally indexed stages. Ordinal inaccessibility is I think equivalent to Ordinal Replacement which by itself is actually weak, it can only build stages up to $V_{\omega_1}$, and of course successor cardinals can only build the next stages, but together it seems that they can act to build up the whole of Von Neumann's universe. So, I thought that the above would prove full Replacement. Its easy to prove the result with Choice (in the form of every set is bijective to some von Neumann ordinal); but without it the proof is elluding me?
 A: This theory doesn't prove Replacement (assuming the consistency of an inaccessible, at least).
Assume ZFC + $\kappa$ is inaccessible and force over $V$ to add  $\kappa$-many Cohen reals (i.e. the forcing is finite support product $\Pi_{\alpha<\kappa}\mathbb{C}_\alpha$  where each $\mathbb{C}_\alpha$ is just Cohen forcing). This forcing is ccc, so preserves all cardinals and cofinalities. So $\kappa$ is still a weakly inaccessible cardinal in $V[G]$. Now let $M=V_\kappa^{V[G]}$. Note that $M$ models the axioms you mention (in particular as $\kappa$ is regular in $V[G]$). But it does not satisfy Replacement: Working in $V[G]$,
let $X$ be the set of all wellorders of $V_{\omega+1}$ of ordertype ${<\kappa}$. Then $X\in V_\kappa$. Consider the function sending $W\in X$ to the ordertype of $W$. This is definable over $V_\kappa^{V[G]}$ (actually without parameters), and is a surjection $X\to\kappa$ there.
Note that $M$ does satisfy Choice, formulated as "for every function there is a choice function". However, it does not satisfy the statement that "every wellorderable set is bijectable with an ordinal". (The set $X'$ of equivalence classes of wellorders in $X$, where they are equivalent if they have the same ordertype, is such a set.) Although ordinal inaccessibility holds in $M$, $X'$ is wellorderable in ordertype that of the class of ordinals.
Note that "ordinal" can also be defined as  (i) the equivalence class of all wellordered sets of a given ordertype. Under ZF, this is equivalent to (ii) the von Neumann ordinals  "transitive sets whose elements are strictly linearly ordered by $\in$" (which  under ZF is equivalent to (ii') "transitive sets whose elements are well ordered by $\in$"). But in the model $M$, (i) and (ii) do not coincide (but (ii) and (ii') do).
A: We are assuming that a formula (x,y) with 2 free variables defines a function means that for every x there is a unique y such that (x,y).
We assume that the axiom schema of Successor cardinals and the axiom schema of Ordinal inaccessibility are the result of replacing "f is a definable function" by "(x,y)
defines a function", replacing "()=" by (,), and replacing ≤() by "there is a b such that (,b) and  ≤b".
We note that the axiom schema of Successor cardinals, is an immediate consequence of the axiom schema of Ordinal inaccessibility.(Suppose that (x,y) defines a function and c ia an ordinal.
By Ordinal inaccessibility, there is an ordinal  with the property that ∀<c:(,b)-->("b is not an ordinal" or b<).  Then ¬∀<(+1)∃<c:(,), since ¬(,) for all  <c.)
Z + Ranks + Ordinal inaccessibility has the same consequences as Z + Ranks + Ordinal Replacement.
Proof: Suppose Ordinal Replacement holds, (x,y) defines a function,  is an ordinal, and for every ordinal  (∃<∃b:≤b∧(,b)). Let (x,y) be the formula ("x is an ordinal" and "y is an ordinal" and (x,y)) or ("x is an ordinal" and (∀t((x,y)-->"t is not an ordinal") and y=0) or ("x is not an ordinal" and y=x). By Ordinal Replacement ∃∀(∈↔∃∈(,)). But then every ordinal is in UB. Now suppose Ordinal inaccessibility holds, (x,y) is a formula in two free variables x,y, ∀[()→∃!(()∧(,))], and A is a set of ordinals. Let (x,y) be the formula ("x is an ordinal" and "y is an ordinal" and (x,y)) or ("x is not an ordinal" and x=y).  Then (x,y) defines a function. By Ordinal inaccessibility, there is an ordinal  with the property ∀<(UA)∀b((,b)-->b<). Then there is a set B such that
   b∈B<-->b∈∧∃∈((x,b)). Therefore Ordinal Replacement holds.

If ZF is consistent then Z + Ranks + Ordinal inaccessibility + Choice does not prove Replacement.
Proof: See the answer of Joel David Hamkins to  "Is full Replacement provable in Z + Ordinal Replacement?". (His argument shows that in a model of ZFC, ⟨1,∈⟩ satisfies Z + Ranks + Ordinal Replacement + Choice but not all instancess of Replacement.)
