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	Could not format assertion : No typesetting found for |- LexOrd We ( On X. On ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-lexo	Could not format LexOrd = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } : No typesetting found for |- LexOrd = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } with typecode |-
2	1	leweon	Could not format LexOrd We ( On X. On ) : No typesetting found for |- LexOrd We ( On X. On ) with typecode |-