If $\psi$ is a predicate that is definable in $FOL(\in,=)$ by a formula from parameters in $V$, then if $\psi$ hold of the class $\small ORD$ of all ordinals in $V$, then the class of all cardinals in $V$ satisfying $\psi$ is non empty and is isomorphic on membership with $\small ORD$

Formally this is: $\psi(\small ORD) \to \forall x (x = \{y| \ y \text{ is a cardinal } \wedge \psi(y)\} \to x \neq \emptyset \wedge x \cong \small ORD)$

Now this axiom scheme is to be added on top of axioms of the following theory formulated in first order predicate logic with extra-logical primitives of equality, membership and a single primitive constant symbol $V$ denoting the class of all sets.

The axioms are those of first order identity theory +

1. Extensionality: $\forall x (x \in a \leftrightarrow x \in b) \to a=b$
2. Foundation over all classes: $\exists m \in x \to \exists y \in x (y \cap x = \emptyset)$
3. Class comprehension axiom: if $\phi(y)$ is a formula in which the symbol $``y"$ occurs free, then all closures of: $\exists x \forall y (y \in x \leftrightarrow y \in V \wedge \phi(y))$ are axioms.

Define $\{|\}: x=\{y|\phi(y)\} \iff \forall y (y \in x \leftrightarrow y \in V \wedge \phi(y))$

4. Transitivity: $x \in V \wedge y \in x \to y \in V$

5. Supertransitivity: $x \in V \wedge y \subseteq x \to y \in V$

6. Pairing: $a,b \in V \to \{a,b\} \in V$

7. Set Union: $a \in V \to \{x| \exists y \in a (x \in y)\} \in V$

8. Power: $a \in V \to \{x| x \subseteq a\} \in V$

9. Limitation of size: $|x| < |V| \to x \in V$

Where $``||"$ denotes cardinality function defined in the usual manner.

Now its clear that this theory goes beyond $ZFC$, since $\small ORD$ would provably be a regular cardinal and so the set of all regular cardinals in $ORD$ must be isomorphic on membership with $ORD$, and so we must have inaccessible cardinals in $ORD$, actually it is even simpler than that, simply take the property of being "inaccessible cardinal" which is definable in the pure language of set theory, clearly $ORD$ fulfills that, so there must be an inaccessible cardinal in $ORD$. However it is not clear to me how far this theory can go to?

Question: what is the consistency strength of this theory?

If $\psi$ is a predicate that is definable in $FOL(\in,=)$ by a formula from parameters in $V$, then if $\psi$ hold of the class $\small ORD$ of all ordinals in $V$, then the class of all cardinals in $V$ satisfying $\psi$ is non empty and is isomorphic on membership with $\small ORD$

Formally this is: $\psi(\small ORD) \to \forall x (x = \{y| \ y \text{ is a cardinal } \wedge \psi(y)\} \to x \neq \emptyset \wedge x \cong \small ORD)$

Now this axiom scheme is to be added on top of axioms of the following theory formulated in first order predicate logic with extra-logical primitives of equality, membership and a single primitive constant symbol $V$ denoting the class of all sets.

The axioms are those of first order identity theory +

1. Extensionality: $\forall x (x \in a \leftrightarrow x \in b) \to a=b$
2. Foundation over all classes: $\exists m \in x \to \exists y \in x (y \cap x = \emptyset)$
3. Class comprehension axiom: if $\phi(y)$ is a formula in which the symbol $``y"$ occurs free, then all closures of: $\exists x \forall y (y \in x \leftrightarrow y \in V \wedge \phi(y))$ are axioms.

Define $\{|\}: x=\{y|\phi(y)\} \iff \forall y (y \in x \leftrightarrow y \in V \wedge \phi(y))$

4. Transitivity: $x \in V \wedge y \in x \to y \in V$

5. Supertransitivity: $x \in V \wedge y \subseteq x \to y \in V$

6. Pairing: $a,b \in V \to \{a,b\} \in V$

7. Set Union: $a \in V \to \{x| \exists y \in a (x \in y)\} \in V$

8. Power: $a \in V \to \{x| x \subseteq a\} \in V$

9. Limitation of size: $|x| < |V| \wedge x \subset V \to x \in V$

Where $``||"$ denotes cardinality function defined in the usual manner.

Now its clear that this theory goes beyond $ZFC$, since $\small ORD$ would provably be a regular cardinal and so the set of all regular cardinals in $ORD$ must be isomorphic on membership with $ORD$, and so we must have inaccessible cardinals in $ORD$, actually it is even simpler than that, simply take the property of being "inaccessible cardinal" which is definable in the pure language of set theory, clearly $ORD$ fulfills that, so there must be an inaccessible cardinal in $ORD$. However it is not clear to me how far this theory can go to?

Question: what is the consistency strength of this theory?

If $\psi$ is a predicate that is definable in $FOL(\in,=)$ by a formula from parameters in $V$, then if $\psi$ hold of the class $\small ORD$ of all ordinals in $V$, then the class of all cardinals in $V$ satisfying $\psi$ is non empty and is isomorphic on membership with $\small ORD$

Formally this is: $\psi(\small ORD) \to \forall x (x = \{y| \ y \text{ is a cardinal } \wedge \psi(y)\} \to x \neq \emptyset \wedge x \cong \small ORD)$

Now this axiom scheme is to be added on top of the axioms of following theory formulated in the language of set theory with the addition of a single primitive constant symbol $V$ denoting the class of all sets.

The axioms are those of first order identity theory +

1. Extensionality: $\forall x (x \in a \leftrightarrow x \in b) \to a=b$
2. Foundation over all classes: $\exists m \in x \to \exists y \in x (y \cap x = \emptyset)$
3. Class comprehension axiom: if $\phi(y)$ is a formula in which the symbol $``y"$ occurs free, then all closures of: $\exists x \forall y (y \in x \leftrightarrow y \in V \wedge \phi(y))$ are axioms.

Define $\{|\}: x=\{y|\phi(y)\} \iff \forall y (y \in x \leftrightarrow y \in V \wedge \phi(y))$

4. Transitivity: $x \in V \wedge y \in x \to y \in V$

5. Supertransitivity: $x \in V \wedge y \subseteq x \to y \in V$

6. Pairing: $a,b \in V \to \{a,b\} \in V$

7. Set Union: $a \in V \to \{x| \exists y \in a (x \in y)\} \in V$

8. Power: $a \in V \to \{x| x \subseteq a\} \in V$

9. Limitation of size: $|x| < |V| \to x \in V$

Where $``||"$ denotes cardinality function defined in the usual manner.

Now its clear that this theory goes beyond $ZFC$, since $\small ORD$ would provably be a regular cardinal and so the set of all regular cardinals in $ORD$ must be isomorphic on membership with $ORD$, and so we must have inaccessible cardinals in $ORD$, actually it is even simpler than that, simply take the property of being "inaccessible cardinal" which is definable in the pure language of set theory, clearly $ORD$ fulfills that, so there must be an inaccessible cardinal in $ORD$. However it is not clear to me how far this theory can go to?

Question: what is the consistency strength of this theory?

If $\psi$ is a predicate that is definable in $FOL(\in,=)$ by a formula from parameters in $V$, then if $\psi$ hold of the class $\small ORD$ of all ordinals in $V$, then the class of all cardinals in $V$ satisfying $\psi$ is non empty and is isomorphic on membership with $\small ORD$

Formally this is: $\psi(\small ORD) \to \forall x (x = \{y| \ y \text{ is a cardinal } \wedge \psi(y)\} \to x \neq \emptyset \wedge x \cong \small ORD)$

Now this axiom scheme is to be added on top of axioms of the following theory formulated in first order predicate logic with extra-logical primitives of equality, membership and a single primitive constant symbol $V$ denoting the class of all sets.

The axioms are those of first order identity theory +

1. Extensionality: $\forall x (x \in a \leftrightarrow x \in b) \to a=b$
2. Foundation over all classes: $\exists m \in x \to \exists y \in x (y \cap x = \emptyset)$
3. Class comprehension axiom: if $\phi(y)$ is a formula in which the symbol $``y"$ occurs free, then all closures of: $\exists x \forall y (y \in x \leftrightarrow y \in V \wedge \phi(y))$ are axioms.

Define $\{|\}: x=\{y|\phi(y)\} \iff \forall y (y \in x \leftrightarrow y \in V \wedge \phi(y))$

4. Transitivity: $x \in V \wedge y \in x \to y \in V$

5. Supertransitivity: $x \in V \wedge y \subseteq x \to y \in V$

6. Pairing: $a,b \in V \to \{a,b\} \in V$

7. Set Union: $a \in V \to \{x| \exists y \in a (x \in y)\} \in V$

8. Power: $a \in V \to \{x| x \subseteq a\} \in V$

9. Limitation of size: $|x| < |V| \to x \in V$

Where $``||"$ denotes cardinality function defined in the usual manner.

Now its clear that this theory goes beyond $ZFC$, since $\small ORD$ would provably be a regular cardinal and so the set of all regular cardinals in $ORD$ must be isomorphic on membership with $ORD$, and so we must have inaccessible cardinals in $ORD$, actually it is even simpler than that, simply take the property of being "inaccessible cardinal" which is definable in the pure language of set theory, clearly $ORD$ fulfills that, so there must be an inaccessible cardinal in $ORD$. However it is not clear to me how far this theory can go to?

Question: what is the consistency strength of this theory?