Theorem dfj2

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

	Ref	Expression
Assertion	dfj2	Could not format assertion : No typesetting found for |- _J = ( x e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` x ) ) ) +o ( 2nd ` x ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-j	Could not format _J = ( y e. On , z e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. y , z >. ) ) +o n ) ) : No typesetting found for |- _J = ( y e. On , z e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. y , z >. ) ) +o n ) ) with typecode |-
2		df-ot	$$⊢⟨y,z,n⟩=⟨⟨y,z⟩,n⟩$$
3	2	eqeq2i	$$⊢x=⟨y,z,n⟩\leftrightarrow x=⟨⟨y,z⟩,n⟩$$
4		opex	$$⊢⟨y,z⟩\in \mathrm{V}$$
5		vex	$$⊢n\in \mathrm{V}$$
6	4 5	op1std	$$⊢x=⟨⟨y,z⟩,n⟩\to 1^{st}\left(x\right)=⟨y,z⟩$$
7	3 6	sylbi	$$⊢x=⟨y,z,n⟩\to 1^{st}\left(x\right)=⟨y,z⟩$$
8	7	fveq2d	Could not format ( x = <. y , z , n >. -> ( _J0 ` ( 1st ` x ) ) = ( _J0 ` <. y , z >. ) ) : No typesetting found for |- ( x = <. y , z , n >. -> ( _J0 ` ( 1st ` x ) ) = ( _J0 ` <. y , z >. ) ) with typecode |-
9	8	oveq2d	Could not format ( x = <. y , z , n >. -> ( 9o .o ( _J0 ` ( 1st ` x ) ) ) = ( 9o .o ( _J0 ` <. y , z >. ) ) ) : No typesetting found for |- ( x = <. y , z , n >. -> ( 9o .o ( _J0 ` ( 1st ` x ) ) ) = ( 9o .o ( _J0 ` <. y , z >. ) ) ) with typecode |-
10	4 5	op2ndd	$$⊢x=⟨⟨y,z⟩,n⟩\to 2^{nd}\left(x\right)=n$$
11	3 10	sylbi	$$⊢x=⟨y,z,n⟩\to 2^{nd}\left(x\right)=n$$
12	9 11	oveq12d	Could not format ( x = <. y , z , n >. -> ( ( 9o .o ( _J0 ` ( 1st ` x ) ) ) +o ( 2nd ` x ) ) = ( ( 9o .o ( _J0 ` <. y , z >. ) ) +o n ) ) : No typesetting found for |- ( x = <. y , z , n >. -> ( ( 9o .o ( _J0 ` ( 1st ` x ) ) ) +o ( 2nd ` x ) ) = ( ( 9o .o ( _J0 ` <. y , z >. ) ) +o n ) ) with typecode |-
13	12	mpt3mpt	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
14	1 13	eqtr4i	Could not format _J = ( x e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` x ) ) ) +o ( 2nd ` x ) ) ) : No typesetting found for |- _J = ( x e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` x ) ) ) +o ( 2nd ` x ) ) ) with typecode |-