Metamath Proof Explorer

Definition df-slt

Description: Next, we introduce surreal less-than, a comparison relationship over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011)

Ref Expression
Assertion df-slt ⊢ < s = f g | f ∈ No ∧ g ∈ No ∧ ∃ x ∈ On ∀ y ∈ x f ⁡ y = g ⁡ y ∧ f ⁡ x 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 g ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cslt class < s
1 vf setvar f
2 vg setvar g
3 1 cv setvar f
4 csur class No
5 3 4 wcel wff f ∈ No
6 2 cv setvar g
7 6 4 wcel wff g ∈ No
8 5 7 wa wff f ∈ No ∧ g ∈ No
9 vx setvar x
10 con0 class On
11 vy setvar y
12 9 cv setvar x
13 11 cv setvar y
14 13 3 cfv class f ⁡ y
15 13 6 cfv class g ⁡ y
16 14 15 wceq wff f ⁡ y = g ⁡ y
17 16 11 12 wral wff ∀ y ∈ x f ⁡ y = g ⁡ y
18 12 3 cfv class f ⁡ x
19 c1o class 1 𝑜
20 c0 class ∅
21 19 20 cop class 1 𝑜 ∅
22 c2o class 2 𝑜
23 19 22 cop class 1 𝑜 2 𝑜
24 20 22 cop class ∅ 2 𝑜
25 21 23 24 ctp class 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜
26 12 6 cfv class g ⁡ x
27 18 26 25 wbr wff f ⁡ x 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 g ⁡ x
28 17 27 wa wff ∀ y ∈ x f ⁡ y = g ⁡ y ∧ f ⁡ x 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 g ⁡ x
29 28 9 10 wrex wff ∃ x ∈ On ∀ y ∈ x f ⁡ y = g ⁡ y ∧ f ⁡ x 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 g ⁡ x
30 8 29 wa wff f ∈ No ∧ g ∈ No ∧ ∃ x ∈ On ∀ y ∈ x f ⁡ y = g ⁡ y ∧ f ⁡ x 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 g ⁡ x
31 30 1 2 copab class f g | f ∈ No ∧ g ∈ No ∧ ∃ x ∈ On ∀ y ∈ x f ⁡ y = g ⁡ y ∧ f ⁡ x 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 g ⁡ x
32 0 31 wceq wff < s = f g | f ∈ No ∧ g ∈ No ∧ ∃ x ∈ On ∀ y ∈ x f ⁡ y = g ⁡ y ∧ f ⁡ x 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 g ⁡ x