# Bijection of proper classes

I have two proper classes which intuitively are like bijectively equivalent, i.e. for every element of one of these two classes we can define an expression for the corresponding element of the other class, and these behave nicely (like a bijection).

I wonder, is the notion of bijection extended for proper classes? Where could I read about such generalized bijections?

-

If $X,Y$ are classes defined by formulas $\phi(x), \psi(y)$, then a map $X \to Y$ is just a formula $\alpha(x,y)$ such that $\forall x (\phi(x) \Rightarrow \exists^1 y (\psi(y) \wedge \alpha(x,y)))$. Here $\exists^1$ abbreviates "there exists exactly one ...". This defines the (meta)category of classes and maps of classes. The isomorphisms are exactly the bijections, i.e. with the above notation the maps $\alpha : X \to Y$ such that $\forall y (\psi(y) \Rightarrow \exists^1 x (\phi(x) \wedge \alpha(x,y)))$. In this MO thread it was shown that Schröder Bernstein holds in this setting.

I expect that you can find this notion of bijection in almost every introduction to set theory. A very basic example is the following: Define a (class) well ordering on $\text{On} \times \text{On}$ by

$(\alpha,\beta) < (\gamma,\delta) \Leftrightarrow \max(\alpha,\beta) < \max(\gamma,\delta) \vee (\max(\alpha,\beta) = \max(\gamma,\delta) \wedge$ $(\alpha < \gamma \vee (\alpha = \gamma \wedge \beta < \delta))$.

Its type can be used to define a bijection of classes $\text{On} \cong \text{On} \times \text{On}$, but also it yields the equality $\kappa^2=\kappa$ for every cardinal number $\kappa \geq \aleph_0$ (even without AC).

-
I don't like defining a map as a formula. This suppresses maps which are not expressible as a finite formula. Well, in my particular case I can deal with this special case when we consider only maps expressible with a finite formula, because in my example I can write explicit formulas down. But I just don't like it. –  porton Jun 14 '11 at 21:17
How do you define infinite formulas? –  Martin Brandenburg Jun 14 '11 at 21:56
@Martin: I don't think that the OP is positing infinite formulas. But only countably many of the maps from $\omega$ to $\omega$ (for example) are defined by formulas. –  John Bentin Jun 15 '11 at 11:06
@John: Perhaps we should allow parameters. –  Martin Brandenburg Jun 16 '11 at 8:27
How does this prove $\kappa^2=\kappa$ for every $\kappa \ge \aleph_0$? It seems to only work for alephs. –  Chris Eagle Jun 18 '11 at 10:18
ARC, an extension of Ackermann set theory (F.A.Muller, "Sets, Classes, and Categories", 2001, http://en.scientificcommons.org/49425946 PDF) proves the existence of the n-th powerclass of the set universe V for any $n \in \mathbb{N}$. That should make it possible to define pairs/triples of classes and thus functions and bijections the usual way.