Epsilon-recursion Theorem

Let be a Function Class defined everywhere.
Then there is a function class defined everywhere
such that:

Also is unique.
Note is the set
which is a set by Axiom of Replacement

Proof

Uniqueness by Principle of Epsilon-Induction

We say is an attempt if

• is a function
• is transitive
  and

Note that makes sense as is transitive.
Now use induction to show two attempts agree on intersection of their domains
Another induction shows every set is in domain for some
Then is defined by