![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-made | Structured version Visualization version GIF version |
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 |
---|---|
df-made | ⊢ M = recs((𝑓 ∈ V ↦ ( |s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmade 27337 | . 2 class M | |
2 | vf | . . . 4 setvar 𝑓 | |
3 | cvv 3475 | . . . 4 class V | |
4 | cscut 27284 | . . . . 5 class |s | |
5 | 2 | cv 1541 | . . . . . . . . 9 class 𝑓 |
6 | 5 | crn 5678 | . . . . . . . 8 class ran 𝑓 |
7 | 6 | cuni 4909 | . . . . . . 7 class ∪ ran 𝑓 |
8 | 7 | cpw 4603 | . . . . . 6 class 𝒫 ∪ ran 𝑓 |
9 | 8, 8 | cxp 5675 | . . . . 5 class (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓) |
10 | 4, 9 | cima 5680 | . . . 4 class ( |s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓)) |
11 | 2, 3, 10 | cmpt 5232 | . . 3 class (𝑓 ∈ V ↦ ( |s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓))) |
12 | 11 | crecs 8370 | . 2 class recs((𝑓 ∈ V ↦ ( |s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓)))) |
13 | 1, 12 | wceq 1542 | 1 wff M = recs((𝑓 ∈ V ↦ ( |s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓)))) |
Colors of variables: wff setvar class |
This definition is referenced by: madeval 27347 oldval 27349 newval 27350 madef 27351 |
Copyright terms: Public domain | W3C validator |