Metamath Proof Explorer

Definition df-left

Description: Define the left options of a surreal. This is the set of surreals that are "closest" on the left to the given surreal. (Contributed by Scott Fenton, 17-Dec-2021)

Ref Expression
Assertion df-left ⊢ L = x ∈ No ⟼ y ∈ Old ⁡ bday ⁡ x | ∀ z ∈ No y < s z ∧ z < s x → bday ⁡ y ∈ bday ⁡ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cleft class L
1 vx setvar x
2 csur class No
3 vy setvar y
4 cold class Old
5 cbday class bday
6 1 cv setvar x
7 6 5 cfv class bday ⁡ x
8 7 4 cfv class Old ⁡ bday ⁡ x
9 vz setvar z
10 3 cv setvar y
11 cslt class < s
12 9 cv setvar z
13 10 12 11 wbr wff y < s z
14 12 6 11 wbr wff z < s x
15 13 14 wa wff y < s z ∧ z < s x
16 10 5 cfv class bday ⁡ y
17 12 5 cfv class bday ⁡ z
18 16 17 wcel wff bday ⁡ y ∈ bday ⁡ z
19 15 18 wi wff y < s z ∧ z < s x → bday ⁡ y ∈ bday ⁡ z
20 19 9 2 wral wff ∀ z ∈ No y < s z ∧ z < s x → bday ⁡ y ∈ bday ⁡ z
21 20 3 8 crab class y ∈ Old ⁡ bday ⁡ x | ∀ z ∈ No y < s z ∧ z < s x → bday ⁡ y ∈ bday ⁡ z
22 1 2 21 cmpt class x ∈ No ⟼ y ∈ Old ⁡ bday ⁡ x | ∀ z ∈ No y < s z ∧ z < s x → bday ⁡ y ∈ bday ⁡ z
23 0 22 wceq wff L = x ∈ No ⟼ y ∈ Old ⁡ bday ⁡ x | ∀ z ∈ No y < s z ∧ z < s x → bday ⁡ y ∈ bday ⁡ z