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	|- _J = ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cj	|- _J
1		vx	|- x
2		con0	|- On
3		vy	|- y
4		vn	|- n
5		c9o	|- 9o
6		comu	|- .o
7		ccj0	|- _J0
8	1	cv	|- x
9	3	cv	|- y
10	8 9	cop	|- <. x , y >.
11	10 7	cfv	|- ( _J0 ` <. x , y >. )
12	5 11 6	co	|- ( 9o .o ( _J0 ` <. x , y >. ) )
13		coa	|- +o
14	4	cv	|- n
15	12 14 13	co	|- ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n )
16	1 3 4 2 2 5 15	cmpt3	|- ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) )
17	0 16	wceq	|- _J = ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) )