Is the following system of infinite arithmetic consistent?

If so, can it interpret $\sf ZFC$?

Language: first order logic

Primitives: $\operatorname{Card}, <, + , \times,\text{^}$

where $\operatorname{Card}$ is one place predicate symbol denoting "is a cardinal".

We'll denote this language by the language of arithmetic.

**Areflexive:** $x \not < x$

**Transitive:** $x < y < z \to x < z$

**Connected:** $x \neq y \leftrightarrow [x < y \lor y < x]$

**Well-Founded:** if $\phi$ is a formula, then: $\phi(x) \to \exists a: \phi(a) \land \forall b: \phi(b) \to b \not < a$

**Cardinality:** if $\phi$ is a formula in two free variables; then:
$\operatorname{Card}(x) \land y < x \land [\phi: prior(y) \to prior(x), \phi \text { is one-one}] \\ \to \phi \text { is not surjective }$

**Successor Cardinals:** $\forall x \, \exists y: \operatorname{Card}(y) \land y > x$

**Replacement:** $[\phi: \psi \to prior(l), \phi \text{ is one-one}] \to \exists k: \forall x (\psi(x) \to k > x)$

* Define:* $x=0 \iff x=\min_{(<)} y: y=y$

* Define:* $S(x)=y \iff y= \min_{(<)} z: z > x$

**Infinity:** $\exists l \neq 0: \forall r < l \exists s: r < s < l$

**Addition:** $ a + 0 = a \\ a + S(b) = S(a+b) \\ a + b = b + a \\ \lambda + \zeta = \lim (\lambda + \alpha)_{\alpha<\zeta} \\\text{; for limits } \lambda, \zeta \text{; and } \lambda \geq \zeta $

**Multiplication:** $a \times 0 = 0 \\ a \times S(b) = a + (a \times b) \\ a \times b = b \times a \\ \lambda \times \zeta = \lim (\lambda \times \alpha)_{\alpha < \zeta} \\\text{; for limits } \lambda, \zeta \text{; and } \lambda \geq \zeta$

**Exponentiation:** $a \text{^} 0 = 1 \\ a \text{^} S(b) = a \times (a \text{^} b) \\ a \text{^} \lambda= \lim (a^\kappa)_{\kappa < \lambda} \text{; for limit
}\lambda$

/

Terminology:

$[\phi: \psi \to \pi, \phi \text { is one-one }]$ is the following formula: $\forall x \,[ \psi(x) \to \exists y: \pi(y) \land \phi(x,y)] \land \\ \forall a,b,c,d \, (\phi(a,b) \land \phi(c,d) \to [a=c \leftrightarrow b=d] )$

$prior(l)$ is the formula $(x < l) $

$( \phi \text { is not surjective})$ in the above expression, it is exactly the formula: $\exists b < x: \forall a \, [a < y \to \neg \phi(a,b)]$