Metamath Proof Explorer

Definition df-right

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cright class R
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 cslt class < s
11 9 cv setvar z
12 6 11 10 wbr wff x < s z
13 3 cv setvar y
14 11 13 10 wbr wff z < s y
15 12 14 wa wff x < s z ∧ z < s y
16 13 5 cfv class bday ⁡ y
17 11 5 cfv class bday ⁡ z
18 16 17 wcel wff bday ⁡ y ∈ bday ⁡ z
19 15 18 wi wff x < s z ∧ z < s y → bday ⁡ y ∈ bday ⁡ z
20 19 9 2 wral wff ∀ z ∈ No x < s z ∧ z < s y → bday ⁡ y ∈ bday ⁡ z
21 20 3 8 crab class y ∈ Old ⁡ bday ⁡ x | ∀ z ∈ No x < s z ∧ z < s y → bday ⁡ y ∈ bday ⁡ z
22 1 2 21 cmpt class x ∈ No ⟼ y ∈ Old ⁡ bday ⁡ x | ∀ z ∈ No x < s z ∧ z < s y → bday ⁡ y ∈ bday ⁡ z
23 0 22 wceq wff R = x ∈ No ⟼ y ∈ Old ⁡ bday ⁡ x | ∀ z ∈ No x < s z ∧ z < s y → bday ⁡ y ∈ bday ⁡ z