I want to know if the following theory stand a chance of being consistent?
$Language:$ Mono-sorted first order predicate logic + primitives of equality $``="$ and class membership $``\in"$:
Define: $set(x) \iff \exists y \, (x \in y)$
Axioms:
Extensionality: $\forall z ( z \in x \leftrightarrow z \in y) \implies x=y$
Class Comprehension: $\exists x \forall y (y \in x \iff set(y) \phi)$; for any formula $\phi$ in which $``x"$ doesn't occur.
Define: $x=V \equiv_{df} \forall \text { set } y \, (y \in x)$
Sets: $\sf ZFC$$^V$
That is: all axioms of $\sf ZFC$ written with all of their quantifiers bounded $``\in V"$.
Size: $\forall x \in V (|x| \leq \aleph_\omega)$
Exchange: $\forall a,b \in V: |a|=|b| \to \\\exists f (f: a \to b \land bijection(f) \land \\ \forall k \in V [k \subseteq a \to f``k \in V ] \, \land \\\forall l \in V [l \subseteq b \to f^{-1} ``l \in V] )$
Where: $f``x = \{f(y): y \in x\}$, and $f^{-1}= \{\langle b,a \rangle: \langle a, b \rangle \in f\}$
The point here is that the last axiom does add sets through the use of an external function! So sets are not just left a lone to be built after the set world ZFC rules. No! Sets can be constructed after external functions here.
Can this theory be consistent???
