Description: _R0 is a set-like well-ordering of On X. On . Part of Proposition 7.58 of TakeutiZaring p. 54. This theorem is r0weon expressed using _R0 . (Contributed by BTernaryTau, 19-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r0weseon | |- ( _R0 We ( On X. On ) /\ _R0 Se ( 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 | df-r0 | |- _R0 = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z LexOrd w ) ) ) } |
|
| 3 | 1 2 | r0weon | |- ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) ) |