![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-left | Structured version Visualization version GIF version |
Description: Define the left options of a surreal. This is the set of surreals that are simpler and less than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.) |
Ref | Expression |
---|---|
df-left | ⊢ L = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑦 <s 𝑥}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cleft 27341 | . 2 class L | |
2 | vx | . . 3 setvar 𝑥 | |
3 | csur 27143 | . . 3 class No | |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 4 | cv 1541 | . . . . 5 class 𝑦 |
6 | 2 | cv 1541 | . . . . 5 class 𝑥 |
7 | cslt 27144 | . . . . 5 class <s | |
8 | 5, 6, 7 | wbr 5149 | . . . 4 wff 𝑦 <s 𝑥 |
9 | cbday 27145 | . . . . . 6 class bday | |
10 | 6, 9 | cfv 6544 | . . . . 5 class ( bday ‘𝑥) |
11 | cold 27339 | . . . . 5 class O | |
12 | 10, 11 | cfv 6544 | . . . 4 class ( O ‘( bday ‘𝑥)) |
13 | 8, 4, 12 | crab 3433 | . . 3 class {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑦 <s 𝑥} |
14 | 2, 3, 13 | cmpt 5232 | . 2 class (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑦 <s 𝑥}) |
15 | 1, 14 | wceq 1542 | 1 wff L = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑦 <s 𝑥}) |
Colors of variables: wff setvar class |
This definition is referenced by: leftval 27359 leftf 27361 |
Copyright terms: Public domain | W3C validator |