Description: Define the _R0 order isomorphism from On X. On to On . Equivalent to Definition 7.59 of TakeutiZaring p. 55. (Contributed by BTernaryTau, 2-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-j0 | |- _J0 = `' OrdIso ( _R0 , ( On X. On ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ccj0 | |- _J0 |
|
| 1 | cr0 | |- _R0 |
|
| 2 | con0 | |- On |
|
| 3 | 2 2 | cxp | |- ( On X. On ) |
| 4 | 3 1 | coi | |- OrdIso ( _R0 , ( On X. On ) ) |
| 5 | 4 | ccnv | |- `' OrdIso ( _R0 , ( On X. On ) ) |
| 6 | 0 5 | wceq | |- _J0 = `' OrdIso ( _R0 , ( On X. On ) ) |