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

Definition df-new 33678
Description: Define the newer than function. This function carries an ordinal to all surreals made on that day. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.)
Assertion
Ref Expression
df-new N = (𝑥 ∈ On ↦ (( M ‘𝑥) ∖ ( O ‘𝑥)))

Detailed syntax breakdown of Definition df-new
StepHypRef Expression
1 cnew 33673 . 2 class N
2 vx . . 3 setvar 𝑥
3 con0 6172 . . 3 class On
42cv 1541 . . . . 5 class 𝑥
5 cmade 33671 . . . . 5 class M
64, 5cfv 6339 . . . 4 class ( M ‘𝑥)
7 cold 33672 . . . . 5 class O
84, 7cfv 6339 . . . 4 class ( O ‘𝑥)
96, 8cdif 3840 . . 3 class (( M ‘𝑥) ∖ ( O ‘𝑥))
102, 3, 9cmpt 5110 . 2 class (𝑥 ∈ On ↦ (( M ‘𝑥) ∖ ( O ‘𝑥)))
111, 10wceq 1542 1 wff N = (𝑥 ∈ On ↦ (( M ‘𝑥) ∖ ( O ‘𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  newval  33684  newf  33687
  Copyright terms: Public domain W3C validator