Can we have a strong class theory in which all sets are Dedekindian finite, and that has some of its sets being Tarski infinite? By strong I mean that it can interpret $\sf ZFC$ and its extensions. Like for example a class theory where sets are defined as elements of classes with axioms of:
Extensionality: $\forall x,y [\forall z(z \in x \leftrightarrow z \in y) \to x=y]$
Impredicatie class comprehension: if $\phi$ is a formula in which $x$ doesn't occur free, then each closure of $(\exists x \forall y (y \in x \leftrightarrow \text {set}(y) \wedge \phi))$ is an axiom.
Pairing for sets: $\forall \text{ sets } a,b \ \exists \text{ set } x \ ( x=\{a,b\})$
Set Union: $\forall \text { set } a \ \exists \text { set } x \ (x = \bigcup (a))$
Replacement for sets: $\forall \text { set } x \ \forall y \ [\exists f (f: y \rightarrowtail x) \to \text {set}(y)] $
Finitude: $\forall \text{ set } x \ \forall y \subsetneq x \neg \exists f (f: x \rightarrowtail y)$
Infinity: $\exists \text{ set } x [\neg \exists n,f \ (natural(n) \wedge f: x \rightarrowtail \{0,..,n\})] $
Question: can this theory be extended to the degree of interpreting $\sf ZFC$ and its extensions.