Definition df-slt 33774

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 (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}

Distinct variable group:   𝑓,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-slt

Step	Hyp	Ref	Expression
1		cslt 33771	. 2 class <s
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1538	. . . . . 6 class 𝑓
4		csur 33770	. . . . . 6 class No
5	3, 4	wcel 2108	. . . . 5 wff 𝑓 ∈ No
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1538	. . . . . 6 class 𝑔
8	7, 4	wcel 2108	. . . . 5 wff 𝑔 ∈ No
9	5, 8	wa 395	. . . 4 wff (𝑓 ∈ No ∧ 𝑔 ∈ No )
10		vy	. . . . . . . . . 10 setvar 𝑦
11	10	cv 1538	. . . . . . . . 9 class 𝑦
12	11, 3	cfv 6418	. . . . . . . 8 class (𝑓‘𝑦)
13	11, 7	cfv 6418	. . . . . . . 8 class (𝑔‘𝑦)
14	12, 13	wceq 1539	. . . . . . 7 wff (𝑓‘𝑦) = (𝑔‘𝑦)
15		vx	. . . . . . . 8 setvar 𝑥
16	15	cv 1538	. . . . . . 7 class 𝑥
17	14, 10, 16	wral 3063	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦)
18	16, 3	cfv 6418	. . . . . . 7 class (𝑓‘𝑥)
19	16, 7	cfv 6418	. . . . . . 7 class (𝑔‘𝑥)
20		c1o 8260	. . . . . . . . 9 class 1o
21		c0 4253	. . . . . . . . 9 class ∅
22	20, 21	cop 4564	. . . . . . . 8 class ⟨1o, ∅⟩
23		c2o 8261	. . . . . . . . 9 class 2o
24	20, 23	cop 4564	. . . . . . . 8 class ⟨1o, 2o⟩
25	21, 23	cop 4564	. . . . . . . 8 class ⟨∅, 2o⟩
26	22, 24, 25	ctp 4562	. . . . . . 7 class {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}
27	18, 19, 26	wbr 5070	. . . . . 6 wff (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)
28	17, 27	wa 395	. . . . 5 wff (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥))
29		con0 6251	. . . . 5 class On
30	28, 15, 29	wrex 3064	. . . 4 wff ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥))
31	9, 30	wa 395	. . 3 wff ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))
32	31, 2, 6	copab 5132	. 2 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}
33	1, 32	wceq 1539	1 wff <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}

This definition is referenced by:  sltval  33777  sltso  33806