df-r0

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cr0	⊢ 𝑅₀
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		con0	⊢ On
5	4 4	cxp	⊢ ( On × On )
6	3 5	wcel	⊢ 𝑥 ∈ ( On × On )
7	2	cv	⊢ 𝑦
8	7 5	wcel	⊢ 𝑦 ∈ ( On × On )
9	6 8	wa	⊢ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) )
10		c1st	⊢ 1^st
11	3 10	cfv	⊢ ( 1^st ‘ 𝑥 )
12		c2nd	⊢ 2^nd
13	3 12	cfv	⊢ ( 2^nd ‘ 𝑥 )
14	11 13	cun	⊢ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) )
15	7 10	cfv	⊢ ( 1^st ‘ 𝑦 )
16	7 12	cfv	⊢ ( 2^nd ‘ 𝑦 )
17	15 16	cun	⊢ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) )
18	14 17	wcel	⊢ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) )
19	14 17	wceq	⊢ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) )
20		clexo	⊢ LexOrd
21	3 7 20	wbr	⊢ 𝑥 LexOrd 𝑦
22	19 21	wa	⊢ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 )
23	18 22	wo	⊢ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) )
24	9 23	wa	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) )
25	24 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) }
26	0 25	wceq	⊢ 𝑅₀ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) }

Metamath Proof Explorer

Definition df-r0

Detailed syntax breakdown