Definition df-r0 35798

Description: Define a particular set-like well-ordering of On × On using the lexicographical ordering LexOrd. Based on Definition 7.57 of [TakeutiZaring] p. 54. (Contributed by BTernaryTau, 2-Sep-2026.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-r0

Step	Hyp	Ref	Expression
1		cr0 35789	. 2 class 𝑅0
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	. . . . . . . 8 class 1st
12	3, 11	cfv 6527	. . . . . . 7 class (1st ‘𝑥)
13		c2nd 7983	. . . . . . . 8 class 2nd
14	3, 13	cfv 6527	. . . . . . 7 class (2nd ‘𝑥)
15	12, 14	cun 3896	. . . . . 6 class ((1st ‘𝑥) ∪ (2nd ‘𝑥))
16	8, 11	cfv 6527	. . . . . . 7 class (1st ‘𝑦)
17	8, 13	cfv 6527	. . . . . . 7 class (2nd ‘𝑦)
18	16, 17	cun 3896	. . . . . 6 class ((1st ‘𝑦) ∪ (2nd ‘𝑦))
19	15, 18	wcel 2145	. . . . 5 wff ((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ ((1st ‘𝑦) ∪ (2nd ‘𝑦))
20	15, 18	wceq 1570	. . . . . 6 wff ((1st ‘𝑥) ∪ (2nd ‘𝑥)) = ((1st ‘𝑦) ∪ (2nd ‘𝑦))
21		clexo 35788	. . . . . . 7 class LexOrd
22	3, 8, 21	wbr 5102	. . . . . 6 wff 𝑥LexOrd𝑦
23	20, 22	wa 401	. . . . 5 wff (((1st ‘𝑥) ∪ (2nd ‘𝑥)) = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∧ 𝑥LexOrd𝑦)
24	19, 23	wo 861	. . . 4 wff (((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∨ (((1st ‘𝑥) ∪ (2nd ‘𝑥)) = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∧ 𝑥LexOrd𝑦))
25	10, 24	wa 401	. . 3 wff ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ (((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∨ (((1st ‘𝑥) ∪ (2nd ‘𝑥)) = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∧ 𝑥LexOrd𝑦)))
26	25, 2, 7	copab 5166	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ (((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∨ (((1st ‘𝑥) ∪ (2nd ‘𝑥)) = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∧ 𝑥LexOrd𝑦)))}
27	1, 26	wceq 1570	1 wff 𝑅0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ (((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∨ (((1st ‘𝑥) ∪ (2nd ‘𝑥)) = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∧ 𝑥LexOrd𝑦)))}

This definition is used by: (None)