Definition df-j0

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	Could not format assertion : No typesetting found for |- _J0 = `' OrdIso ( _R0 , ( On X. On ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccj0	Could not format _J0 : No typesetting found for class _J0 with typecode class
1		cr0	Could not format _R0 : No typesetting found for class _R0 with typecode class
2		con0	$$class\mathrm{On}$$
3	2 2	cxp	$$class\left(\mathrm{On}\times \mathrm{On}\right)$$
4	3 1	coi	Could not format OrdIso ( _R0 , ( On X. On ) ) : No typesetting found for class OrdIso ( _R0 , ( On X. On ) ) with typecode class
5	4	ccnv	Could not format `' OrdIso ( _R0 , ( On X. On ) ) : No typesetting found for class `' OrdIso ( _R0 , ( On X. On ) ) with typecode class
6	0 5	wceq	Could not format _J0 = `' OrdIso ( _R0 , ( On X. On ) ) : No typesetting found for wff _J0 = `' OrdIso ( _R0 , ( On X. On ) ) with typecode wff