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 X. On ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-lexo | |- 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 ) ) ) ) } |
|
| 2 | 1 | leweon | |- LexOrd We ( On X. On ) |