Definition df-lts 28006

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

Assertion

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

Distinct variable group:   𝑓,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-lts

Step	Hyp	Ref	Expression
1		clts 28003	. 2 class <s
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1568	. . . . . 6 class 𝑓
4		csur 28002	. . . . . 6 class No
5	3, 4	wcel 2144	. . . . 5 wff 𝑓 ∈ No
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1568	. . . . . 6 class 𝑔
8	7, 4	wcel 2144	. . . . 5 wff 𝑔 ∈ No
9	5, 8	wa 401	. . . 4 wff (𝑓 ∈ No ∧ 𝑔 ∈ No)
10		vy	. . . . . . . . . 10 setvar 𝑦
11	10	cv 1568	. . . . . . . . 9 class 𝑦
12	11, 3	cfv 6538	. . . . . . . 8 class (𝑓‘𝑦)
13	11, 7	cfv 6538	. . . . . . . 8 class (𝑔‘𝑦)
14	12, 13	wceq 1569	. . . . . . 7 wff (𝑓‘𝑦) = (𝑔‘𝑦)
15		vx	. . . . . . . 8 setvar 𝑥
16	15	cv 1568	. . . . . . 7 class 𝑥
17	14, 10, 16	wral 3076	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦)
18	16, 3	cfv 6538	. . . . . . 7 class (𝑓‘𝑥)
19	16, 7	cfv 6538	. . . . . . 7 class (𝑔‘𝑥)
20		c1o 8472	. . . . . . . . 9 class 1o
21		c0 4278	. . . . . . . . 9 class ∅
22	20, 21	cop 4834	. . . . . . . 8 class ⟨1o, ∅⟩
23		c2o 8473	. . . . . . . . 9 class 2o
24	20, 23	cop 4834	. . . . . . . 8 class ⟨1o, 2o⟩
25	21, 23	cop 4834	. . . . . . . 8 class ⟨∅, 2o⟩
26	22, 24, 25	ctp 4588	. . . . . . 7 class {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}
27	18, 19, 26	wbr 5102	. . . . . 6 wff (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)
28	17, 27	wa 401	. . . . 5 wff (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥))
29		con0 6362	. . . . 5 class On
30	28, 15, 29	wrex 3086	. . . 4 wff ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥))
31	9, 30	wa 401	. . 3 wff ((𝑓 ∈ No ∧ 𝑔 ∈ No) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))
32	31, 2, 6	copab 5166	. 2 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}
33	1, 32	wceq 1569	1 wff <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}

This definition is used by:  ltsval  28009  ltsso  28038