Description: Construct On using set recursion. When x e. On , the function F constructs the least ordinal greater than any of the elements of x , which is U. x for a limit ordinal and suc U. x for a successor ordinal.
For example, ( F{ 1o , 2o } ) = { U. { 1o , 2o } , suc U. { 1o , 2o } } = { 2o , 3o } which contains 3o , and ( F_om ) = { U.om , suc U. om } = {om , om +o 1o } , which contains _om . If we start with the empty set and keep applying F transfinitely many times, all ordinal numbers will be generated.
Any function F fulfilling lemmas onsetreclem2 and onsetreclem3 will recursively generate On ; for example, F = ( x e.V |-> suc suc U. x } ) also works. Whether this function or the function in the theorem is used, taking this theorem as a definition of On is unsatisfying because it relies on the different properties of limit and successor ordinals. A different approach could be to let F = ( x e. V |-> { y e. ~P x | Tr y } ) , based on dfon2 .
The proof of this theorem uses the dummy variable a rather than x to avoid a distinct variable condition between F and x . (Contributed by Emmett Weisz, 22-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | onsetrec.1 | |- F = ( x e. _V |-> { U. x , suc U. x } ) |
|
| Assertion | onsetrec | |- setrecs ( F ) = On |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | onsetrec.1 | |- F = ( x e. _V |-> { U. x , suc U. x } ) |
|
| 2 | eqid | |- setrecs ( F ) = setrecs ( F ) |
|
| 3 | 1 | onsetreclem2 | |- ( a C_ On -> ( F ` a ) C_ On ) |
| 4 | 3 | ax-gen | |- A. a ( a C_ On -> ( F ` a ) C_ On ) |
| 5 | 4 | a1i | |- ( T. -> A. a ( a C_ On -> ( F ` a ) C_ On ) ) |
| 6 | 2 5 | setrec2v | |- ( T. -> setrecs ( F ) C_ On ) |
| 7 | 6 | mptru | |- setrecs ( F ) C_ On |
| 8 | vex | |- a e. _V |
|
| 9 | 8 | a1i | |- ( a C_ setrecs ( F ) -> a e. _V ) |
| 10 | id | |- ( a C_ setrecs ( F ) -> a C_ setrecs ( F ) ) |
|
| 11 | 2 9 10 | setrec1 | |- ( a C_ setrecs ( F ) -> ( F ` a ) C_ setrecs ( F ) ) |
| 12 | 1 | onsetreclem3 | |- ( a e. On -> a e. ( F ` a ) ) |
| 13 | ssel | |- ( ( F ` a ) C_ setrecs ( F ) -> ( a e. ( F ` a ) -> a e. setrecs ( F ) ) ) |
|
| 14 | 11 12 13 | syl2im | |- ( a C_ setrecs ( F ) -> ( a e. On -> a e. setrecs ( F ) ) ) |
| 15 | 14 | com12 | |- ( a e. On -> ( a C_ setrecs ( F ) -> a e. setrecs ( F ) ) ) |
| 16 | 15 | rgen | |- A. a e. On ( a C_ setrecs ( F ) -> a e. setrecs ( F ) ) |
| 17 | tfi | |- ( ( setrecs ( F ) C_ On /\ A. a e. On ( a C_ setrecs ( F ) -> a e. setrecs ( F ) ) ) -> setrecs ( F ) = On ) |
|
| 18 | 7 16 17 | mp2an | |- setrecs ( F ) = On |