Definition df-lts 27983

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 27980	. 2 class <s
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1569	. . . . . 6 class 𝑓
4		csur 27979	. . . . . 6 class No
5	3, 4	wcel 2145	. . . . 5 wff 𝑓 ∈ No
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1569	. . . . . 6 class 𝑔
8	7, 4	wcel 2145	. . . . 5 wff 𝑔 ∈ No
9	5, 8	wa 401	. . . 4 wff (𝑓 ∈ No ∧ 𝑔 ∈ No )
10		vy	. . . . . . . . . 10 setvar 𝑦
11	10	cv 1569	. . . . . . . . 9 class 𝑦
12	11, 3	cfv 6531	. . . . . . . 8 class (𝑓‘𝑦)
13	11, 7	cfv 6531	. . . . . . . 8 class (𝑔‘𝑦)
14	12, 13	wceq 1570	. . . . . . 7 wff (𝑓‘𝑦) = (𝑔‘𝑦)
15		vx	. . . . . . . 8 setvar 𝑥
16	15	cv 1569	. . . . . . 7 class 𝑥
17	14, 10, 16	wral 3077	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦)
18	16, 3	cfv 6531	. . . . . . 7 class (𝑓‘𝑥)
19	16, 7	cfv 6531	. . . . . . 7 class (𝑔‘𝑥)
20		c1o 8453	. . . . . . . . 9 class 1o
21		c0 4279	. . . . . . . . 9 class ∅
22	20, 21	cop 4590	. . . . . . . 8 class ⟨1o, ∅⟩
23		c2o 8454	. . . . . . . . 9 class 2o
24	20, 23	cop 4590	. . . . . . . 8 class ⟨1o, 2o⟩
25	21, 23	cop 4590	. . . . . . . 8 class ⟨∅, 2o⟩
26	22, 24, 25	ctp 4588	. . . . . . 7 class {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}
27	18, 19, 26	wbr 5103	. . . . . 6 wff (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)
28	17, 27	wa 401	. . . . 5 wff (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥))
29		con0 6355	. . . . 5 class On
30	28, 15, 29	wrex 3087	. . . 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 5167	. 2 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}
33	1, 32	wceq 1570	1 wff <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}

This definition is used by:  ltsval  27986  ltsso  28015