Definition df-j0 35923

Description: Define the 𝑅₀ order isomorphism of On × On onto On. Equivalent to Definition 7.59 of [TakeutiZaring] p. 55 (see j0iso 35936). (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 35914	. 2 class 𝐽0
2		con0 6362	. . . . 5 class On
3	2, 2	cxp 5648	. . . 4 class (On × On)
4		cr0 35913	. . . 4 class 𝑅0
5	3, 4	coi 9504	. . 3 class OrdIso(𝑅0, (On × On))
6	5	ccnv 5649	. 2 class ◡OrdIso(𝑅0, (On × On))
7	1, 6	wceq 1569	1 wff 𝐽0 = ◡OrdIso(𝑅0, (On × On))

This definition is used by:  j0iso  35936