Theorem dfj2

Description: Alternate definition of _J as a one-argument function. (Contributed by BTernaryTau, 4-Oct-2026)

	Ref	Expression
Assertion	dfj2	|- _J = ( x e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` x ) ) ) +o ( 2nd ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-j	|- _J = ( y e. On , z e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. y , z >. ) ) +o n ) )
2		df-ot	|- <. y , z , n >. = <. <. y , z >. , n >.
3	2	eqeq2i	|- ( x = <. y , z , n >. <-> x = <. <. y , z >. , n >. )
4		opex	|- <. y , z >. e. _V
5		vex	|- n e. _V
6	4 5	op1std	|- ( x = <. <. y , z >. , n >. -> ( 1st ` x ) = <. y , z >. )
7	3 6	sylbi	|- ( x = <. y , z , n >. -> ( 1st ` x ) = <. y , z >. )
8	7	fveq2d	|- ( x = <. y , z , n >. -> ( _J0 ` ( 1st ` x ) ) = ( _J0 ` <. y , z >. ) )
9	8	oveq2d	|- ( x = <. y , z , n >. -> ( 9o .o ( _J0 ` ( 1st ` x ) ) ) = ( 9o .o ( _J0 ` <. y , z >. ) ) )
10	4 5	op2ndd	|- ( x = <. <. y , z >. , n >. -> ( 2nd ` x ) = n )
11	3 10	sylbi	|- ( x = <. y , z , n >. -> ( 2nd ` x ) = n )
12	9 11	oveq12d	|- ( x = <. y , z , n >. -> ( ( 9o .o ( _J0 ` ( 1st ` x ) ) ) +o ( 2nd ` x ) ) = ( ( 9o .o ( _J0 ` <. y , z >. ) ) +o n ) )
13	12	mpt3mpt	|- ( x e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` x ) ) ) +o ( 2nd ` x ) ) ) = ( y e. On , z e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. y , z >. ) ) +o n ) )
14	1 13	eqtr4i	|- _J = ( x e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` x ) ) ) +o ( 2nd ` x ) ) )