Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-made Structured version   Visualization version   GIF version

Definition df-made 34031
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.)
Assertion
Ref Expression
df-made M = recs((𝑓 ∈ V ↦ ( |s “ (𝒫 ran 𝑓 × 𝒫 ran 𝑓))))

Detailed syntax breakdown of Definition df-made
StepHypRef Expression
1 cmade 34026 . 2 class M
2 vf . . . 4 setvar 𝑓
3 cvv 3432 . . . 4 class V
4 cscut 33977 . . . . 5 class |s
52cv 1538 . . . . . . . . 9 class 𝑓
65crn 5590 . . . . . . . 8 class ran 𝑓
76cuni 4839 . . . . . . 7 class ran 𝑓
87cpw 4533 . . . . . 6 class 𝒫 ran 𝑓
98, 8cxp 5587 . . . . 5 class (𝒫 ran 𝑓 × 𝒫 ran 𝑓)
104, 9cima 5592 . . . 4 class ( |s “ (𝒫 ran 𝑓 × 𝒫 ran 𝑓))
112, 3, 10cmpt 5157 . . 3 class (𝑓 ∈ V ↦ ( |s “ (𝒫 ran 𝑓 × 𝒫 ran 𝑓)))
1211crecs 8201 . 2 class recs((𝑓 ∈ V ↦ ( |s “ (𝒫 ran 𝑓 × 𝒫 ran 𝑓))))
131, 12wceq 1539 1 wff M = recs((𝑓 ∈ V ↦ ( |s “ (𝒫 ran 𝑓 × 𝒫 ran 𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  madeval  34036  oldval  34038  newval  34039  madef  34040
  Copyright terms: Public domain W3C validator