Induction on ℕ₀ from 0 for a Condition Expressed by a Predicative Formula

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\mathbb{N}_{0}$, $0$, $1$ and the sum $n+1$ be as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii) and The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv). Let $x$ be a set variable, and let $\varphi$ be a condition on $x$ that is expressed by a predicative formula, its parameters having their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). For a set $a$, $\varphi(a)$ means that $\varphi$ holds when $a$ is assigned to $x$.

(i) If $\varphi(0)$ holds, and $\varphi(k)$ implies $\varphi(S(k))$ for every $k\in\mathbb{N}_{0}$, where $S(k)$ is the successor of the set $k$, then $\varphi(k)$ holds for every $k\in\mathbb{N}_{0}$.

(ii) If $\varphi(0)$ holds, and $\varphi(n)$ implies $\varphi(n+1)$ for every $n\in\mathbb{N}_{0}$, then $\varphi(n)$ holds for every $n\in\mathbb{N}_{0}$.