Theorem lexoweon

Description: Lexicographical order is a well-ordering of On X. On . Part of Proposition 7.56(1) of TakeutiZaring p. 54. Unlike _R0 , this order isnot set-like, as the preimage of <. 1o , (/) >. is the proper class ( { (/) } X. On ) . This theorem is leweon expressed using LexOrd . (Contributed by BTernaryTau, 19-Sep-2026)

	Ref	Expression
Assertion	lexoweon	⊢ LexOrd We ( On × On )

Proof

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