Definition df-slt 31041

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

Assertion

Ref	Expression
df-slt	⊢ <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔‘𝑥)))}

Distinct variable group:   𝑓,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-slt

Step	Hyp	Ref	Expression
1		cslt 31038	. 2 class <s
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1474	. . . . . 6 class 𝑓
4		csur 31037	. . . . . 6 class No
5	3, 4	wcel 1977	. . . . 5 wff 𝑓 ∈ No
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1474	. . . . . 6 class 𝑔
8	7, 4	wcel 1977	. . . . 5 wff 𝑔 ∈ No
9	5, 8	wa 383	. . . 4 wff (𝑓 ∈ No ∧ 𝑔 ∈ No )
10		vy	. . . . . . . . . 10 setvar 𝑦
11	10	cv 1474	. . . . . . . . 9 class 𝑦
12	11, 3	cfv 5804	. . . . . . . 8 class (𝑓‘𝑦)
13	11, 7	cfv 5804	. . . . . . . 8 class (𝑔‘𝑦)
14	12, 13	wceq 1475	. . . . . . 7 wff (𝑓‘𝑦) = (𝑔‘𝑦)
15		vx	. . . . . . . 8 setvar 𝑥
16	15	cv 1474	. . . . . . 7 class 𝑥
17	14, 10, 16	wral 2896	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦)
18	16, 3	cfv 5804	. . . . . . 7 class (𝑓‘𝑥)
19	16, 7	cfv 5804	. . . . . . 7 class (𝑔‘𝑥)
20		c1o 7440	. . . . . . . . 9 class 1𝑜
21		c0 3874	. . . . . . . . 9 class ∅
22	20, 21	cop 4131	. . . . . . . 8 class ⟨1𝑜, ∅⟩
23		c2o 7441	. . . . . . . . 9 class 2𝑜
24	20, 23	cop 4131	. . . . . . . 8 class ⟨1𝑜, 2𝑜⟩
25	21, 23	cop 4131	. . . . . . . 8 class ⟨∅, 2𝑜⟩
26	22, 24, 25	ctp 4129	. . . . . . 7 class {⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}
27	18, 19, 26	wbr 4583	. . . . . 6 wff (𝑓‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔‘𝑥)
28	17, 27	wa 383	. . . . 5 wff (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔‘𝑥))
29		con0 5640	. . . . 5 class On
30	28, 15, 29	wrex 2897	. . . 4 wff ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔‘𝑥))
31	9, 30	wa 383	. . 3 wff ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔‘𝑥)))
32	31, 2, 6	copab 4642	. 2 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔‘𝑥)))}
33	1, 32	wceq 1475	1 wff <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔‘𝑥)))}

This definition is referenced by:  sltval  31044  sltso  31068