Definition df-lexo 35797

Description: Define the lexicographical ordering of On × On. Based on Definition 7.55 of [TakeutiZaring] p. 54. (Contributed by BTernaryTau, 2-Sep-2026.)

Assertion

Ref	Expression
df-lexo	⊢ LexOrd = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-lexo

Step	Hyp	Ref	Expression
1		clexo 35788	. 2 class LexOrd
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1569	. . . . . 6 class 𝑥
4		con0 6351	. . . . . . 7 class On
5	4, 4	cxp 5645	. . . . . 6 class (On × On)
6	3, 5	wcel 2145	. . . . 5 wff 𝑥 ∈ (On × On)
7		vy	. . . . . . 7 setvar 𝑦
8	7	cv 1569	. . . . . 6 class 𝑦
9	8, 5	wcel 2145	. . . . 5 wff 𝑦 ∈ (On × On)
10	6, 9	wa 401	. . . 4 wff (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On))
11		c1st 7982	. . . . . . 7 class 1st
12	3, 11	cfv 6527	. . . . . 6 class (1st ‘𝑥)
13	8, 11	cfv 6527	. . . . . 6 class (1st ‘𝑦)
14	12, 13	wcel 2145	. . . . 5 wff (1st ‘𝑥) ∈ (1st ‘𝑦)
15	12, 13	wceq 1570	. . . . . 6 wff (1st ‘𝑥) = (1st ‘𝑦)
16		c2nd 7983	. . . . . . . 8 class 2nd
17	3, 16	cfv 6527	. . . . . . 7 class (2nd ‘𝑥)
18	8, 16	cfv 6527	. . . . . . 7 class (2nd ‘𝑦)
19	17, 18	wcel 2145	. . . . . 6 wff (2nd ‘𝑥) ∈ (2nd ‘𝑦)
20	15, 19	wa 401	. . . . 5 wff ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))
21	14, 20	wo 861	. . . 4 wff ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦)))
22	10, 21	wa 401	. . 3 wff ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))
23	22, 2, 7	copab 5166	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))}
24	1, 23	wceq 1570	1 wff LexOrd = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))}

This definition is used by: (None)