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 | ⊢ 𝐹 = ( 𝑥 ∈ V ↦ { ∪ 𝑥 , suc ∪ 𝑥 } ) | |
| Assertion | onsetrec | ⊢ setrecs ( 𝐹 ) = On |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | onsetrec.1 | ⊢ 𝐹 = ( 𝑥 ∈ V ↦ { ∪ 𝑥 , suc ∪ 𝑥 } ) | |
| 2 | eqid | ⊢ setrecs ( 𝐹 ) = setrecs ( 𝐹 ) | |
| 3 | 1 | onsetreclem2 | ⊢ ( 𝑎 ⊆ On → ( 𝐹 ‘ 𝑎 ) ⊆ On ) |
| 4 | 3 | ax-gen | ⊢ ∀ 𝑎 ( 𝑎 ⊆ On → ( 𝐹 ‘ 𝑎 ) ⊆ On ) |
| 5 | 4 | a1i | ⊢ ( ⊤ → ∀ 𝑎 ( 𝑎 ⊆ On → ( 𝐹 ‘ 𝑎 ) ⊆ On ) ) |
| 6 | 2 5 | setrec2v | ⊢ ( ⊤ → setrecs ( 𝐹 ) ⊆ On ) |
| 7 | 6 | mptru | ⊢ setrecs ( 𝐹 ) ⊆ On |
| 8 | vex | ⊢ 𝑎 ∈ V | |
| 9 | 8 | a1i | ⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝑎 ∈ V ) |
| 10 | id | ⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝑎 ⊆ setrecs ( 𝐹 ) ) | |
| 11 | 2 9 10 | setrec1 | ⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → ( 𝐹 ‘ 𝑎 ) ⊆ setrecs ( 𝐹 ) ) |
| 12 | 1 | onsetreclem3 | ⊢ ( 𝑎 ∈ On → 𝑎 ∈ ( 𝐹 ‘ 𝑎 ) ) |
| 13 | ssel | ⊢ ( ( 𝐹 ‘ 𝑎 ) ⊆ setrecs ( 𝐹 ) → ( 𝑎 ∈ ( 𝐹 ‘ 𝑎 ) → 𝑎 ∈ setrecs ( 𝐹 ) ) ) | |
| 14 | 11 12 13 | syl2im | ⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → ( 𝑎 ∈ On → 𝑎 ∈ setrecs ( 𝐹 ) ) ) |
| 15 | 14 | com12 | ⊢ ( 𝑎 ∈ On → ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝑎 ∈ setrecs ( 𝐹 ) ) ) |
| 16 | 15 | rgen | ⊢ ∀ 𝑎 ∈ On ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝑎 ∈ setrecs ( 𝐹 ) ) |
| 17 | tfi | ⊢ ( ( setrecs ( 𝐹 ) ⊆ On ∧ ∀ 𝑎 ∈ On ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝑎 ∈ setrecs ( 𝐹 ) ) ) → setrecs ( 𝐹 ) = On ) | |
| 18 | 7 16 17 | mp2an | ⊢ setrecs ( 𝐹 ) = On |