Definition df-lts

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clts	⊢ <s
1		vf	⊢ 𝑓
2		vg	⊢ 𝑔
3	1	cv	⊢ 𝑓
4		csur	⊢ No
5	3 4	wcel	⊢ 𝑓 ∈ No
6	2	cv	⊢ 𝑔
7	6 4	wcel	⊢ 𝑔 ∈ No
8	5 7	wa	⊢ ( 𝑓 ∈ No ∧ 𝑔 ∈ No )
9		vx	⊢ 𝑥
10		con0	⊢ On
11		vy	⊢ 𝑦
12	9	cv	⊢ 𝑥
13	11	cv	⊢ 𝑦
14	13 3	cfv	⊢ ( 𝑓 ‘ 𝑦 )
15	13 6	cfv	⊢ ( 𝑔 ‘ 𝑦 )
16	14 15	wceq	⊢ ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 )
17	16 11 12	wral	⊢ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 )
18	12 3	cfv	⊢ ( 𝑓 ‘ 𝑥 )
19		c1o	⊢ 1o
20		c0	⊢ ∅
21	19 20	cop	⊢ ⟨ 1o , ∅ ⟩
22		c2o	⊢ 2o
23	19 22	cop	⊢ ⟨ 1o , 2o ⟩
24	20 22	cop	⊢ ⟨ ∅ , 2o ⟩
25	21 23 24	ctp	⊢ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ }
26	12 6	cfv	⊢ ( 𝑔 ‘ 𝑥 )
27	18 26 25	wbr	⊢ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 )
28	17 27	wa	⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) )
29	28 9 10	wrex	⊢ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) )
30	8 29	wa	⊢ ( ( 𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) )
31	30 1 2	copab	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ) }
32	0 31	wceq	⊢ <s = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ) }