Definition df-j0 35799

Description: Define the 𝑅₀ order isomorphism from On × On to On. Equivalent to Definition 7.59 of [TakeutiZaring] p. 55. (Contributed by BTernaryTau, 2-Sep-2026.)

Assertion

Ref	Expression
df-j0	⊢ 𝐽0 = ◡OrdIso(𝑅0, (On × On))

Detailed syntax breakdown of Definition df-j0

Step	Hyp	Ref	Expression
1		ccj0 35790	. 2 class 𝐽0
2		con0 6351	. . . . 5 class On
3	2, 2	cxp 5645	. . . 4 class (On × On)
4		cr0 35789	. . . 4 class 𝑅0
5	3, 4	coi 9481	. . 3 class OrdIso(𝑅0, (On × On))
6	5	ccnv 5646	. 2 class ◡OrdIso(𝑅0, (On × On))
7	1, 6	wceq 1570	1 wff 𝐽0 = ◡OrdIso(𝑅0, (On × On))

This definition is used by: (None)