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 | ⊢ 𝐽0 = ◡ OrdIso ( 𝑅0 , ( On × On ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ccj0 | ⊢ 𝐽0 | |
| 1 | cr0 | ⊢ 𝑅0 | |
| 2 | con0 | ⊢ On | |
| 3 | 2 2 | cxp | ⊢ ( On × On ) |
| 4 | 3 1 | coi | ⊢ OrdIso ( 𝑅0 , ( On × On ) ) |
| 5 | 4 | ccnv | ⊢ ◡ OrdIso ( 𝑅0 , ( On × On ) ) |
| 6 | 0 5 | wceq | ⊢ 𝐽0 = ◡ OrdIso ( 𝑅0 , ( On × On ) ) |