Definition df-j

Description: Define an order isomorphism from ( On X. On ) X. 9o to On . Based on Definition 15.2 of TakeutiZaring p. 155. (Contributed by BTernaryTau, 2-Sep-2026)

	Ref	Expression
Assertion	df-j	Could not format assertion : No typesetting found for |- _J = ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cj	Could not format _J : No typesetting found for class _J with typecode class
1		vx	$$setvarx$$
2		con0	$$class\mathrm{On}$$
3		vy	$$setvary$$
4		vn	$$setvarn$$
5		c9o	Could not format 9o : No typesetting found for class 9o with typecode class
6		comu	$$class{\cdot }_{𝑜}$$
7		ccj0	Could not format _J0 : No typesetting found for class _J0 with typecode class
8	1	cv	$$setvarx$$
9	3	cv	$$setvary$$
10	8 9	cop	$$class⟨x,y⟩$$
11	10 7	cfv	Could not format ( _J0 ` <. x , y >. ) : No typesetting found for class ( _J0 ` <. x , y >. ) with typecode class
12	5 11 6	co	Could not format ( 9o .o ( _J0 ` <. x , y >. ) ) : No typesetting found for class ( 9o .o ( _J0 ` <. x , y >. ) ) with typecode class
13		coa	$$class{+}_{𝑜}$$
14	4	cv	$$setvarn$$
15	12 14 13	co	Could not format ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) : No typesetting found for class ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) with typecode class
16	1 3 4 2 2 5 15	cmpt3	Could not format ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) : No typesetting found for class ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) with typecode class
17	0 16	wceq	Could not format _J = ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) : No typesetting found for wff _J = ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) with typecode wff