To the language of first order logic with equality, add a constant symbol $X_i$ for each natural $i$, add a one place function symbol $P$.
Axiomatize: all axioms of identity theory and of ZFC except power set axiom. Add to that:
Restriction $\omega$-Inference rule: If $\phi(x)$ is a formula in which only $x$ occur free, and only free, and if $\phi(X_i)$ is the formula obtained by merely replacing each occurrence of $x$ by $X_i$, then:
From scheme $[$ for $i=0,1,2,3,...\\ \phi(X_i) ]$
________________Infer
$\forall x [\phi(x)]$
Power set inclusion schema: If $\phi(y)$ is a formula in one free variable $y$ and $y$ only occurs free in it, and in which $X$ doesn't occur, then:
$\forall A \forall X [X=\{y|y \in A \land \phi(y)\} \to X \in P(A)]$
is an axiom.
Power set exclusion $\omega$-Inference rules: if $``\phi_1(y), \phi_2(y),\phi_3(y),..."$ are all formulas in which only $y$ occur free, and only occurs free, then
for $i=1,2,3,...,j=1,2,3,...$
From scheme: $[$ for $n=1,2,3,...\\X_i \neq \{y|y \in X_j \land \phi_n(y)\}]$
_________________________Infer
$X_i \not \in P(X_j)$
Question: I think it is consistent with this theory to have all sets being countable. But is the followings true:
1- Is it consistent with this theory to have every set being strictly smaller in cardinality than its power set?
2- Is it consistent with this theory to stop cardinal increment at any infinite cardinal, i.e. for each infinite cardinal $\kappa$ we can have models of the theory that internally see all sets having their cardinality smaller than or equal to $\kappa$
3- Is it consistent with this theory to have an external automorphism $j$ that move ranks?