Description: Define the made by function. This function carries an ordinal to all surreals made by sections of surreals older than it. Definition from Conway p. 29. (Contributed by Scott Fenton, 17-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-made | ⊢ M = recs ( ( 𝑓 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cmade | ⊢ M | |
| 1 | vf | ⊢ 𝑓 | |
| 2 | cvv | ⊢ V | |
| 3 | cscut | ⊢ |s | |
| 4 | 1 | cv | ⊢ 𝑓 |
| 5 | 4 | crn | ⊢ ran 𝑓 |
| 6 | 5 | cuni | ⊢ ∪ ran 𝑓 |
| 7 | 6 | cpw | ⊢ 𝒫 ∪ ran 𝑓 |
| 8 | 7 7 | cxp | ⊢ ( 𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓 ) |
| 9 | 3 8 | cima | ⊢ ( |s “ ( 𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓 ) ) |
| 10 | 1 2 9 | cmpt | ⊢ ( 𝑓 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓 ) ) ) |
| 11 | 10 | crecs | ⊢ recs ( ( 𝑓 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓 ) ) ) ) |
| 12 | 0 11 | wceq | ⊢ M = recs ( ( 𝑓 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓 ) ) ) ) |