df-lexo

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clexo	⊢ LexOrd
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	7 10	cfv	⊢ ( 1^st ‘ 𝑦 )
13	11 12	wcel	⊢ ( 1^st ‘ 𝑥 ) ∈ ( 1^st ‘ 𝑦 )
14	11 12	wceq	⊢ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 )
15		c2nd	⊢ 2^nd
16	3 15	cfv	⊢ ( 2^nd ‘ 𝑥 )
17	7 15	cfv	⊢ ( 2^nd ‘ 𝑦 )
18	16 17	wcel	⊢ ( 2^nd ‘ 𝑥 ) ∈ ( 2^nd ‘ 𝑦 )
19	14 18	wa	⊢ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 2^nd ‘ 𝑦 ) )
20	13 19	wo	⊢ ( ( 1^st ‘ 𝑥 ) ∈ ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 2^nd ‘ 𝑦 ) ) )
21	9 20	wa	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 2^nd ‘ 𝑦 ) ) ) )
22	21 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 2^nd ‘ 𝑦 ) ) ) ) }
23	0 22	wceq	⊢ LexOrd = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 2^nd ‘ 𝑦 ) ) ) ) }

Metamath Proof Explorer

Definition df-lexo

Detailed syntax breakdown