As has been shown on this site before, it is possible to prove the CantorBernsteinSchröder theorem without the axiom of infinity or the axiom of substitution (most simply by using an argument based on the KnasterTarski lemma, but there are other ways that use naturals without assuming they form a set). We have also seen, in "Does CantorBernstein hold for classes?" that the theorem can be proven for injections between classes in, e.g., NBG. However, the question has not arisen whether it is possible to prove it for classes without using the axiom of infinity (and, I suspect, the axiom of substitution). The "sequence of sets" approach doesn't work because there'a no such thing as a sequence of classes. It's possible to flip that approach around, I believe, by instead considering a class of sequences, but that requires the axiom of infinity and the axiom of substitution. I don't see a way to make the KnasterTarski approach work, because classes don't form anything that looks much like a complete lattice. Any thoughts?
