Theorem dfj2

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

	Ref	Expression
Assertion	dfj2	⊢ 𝐽 = ( 𝑥 ∈ ( ( On × On ) × 9o ) ↦ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑥 ) ) ) +o ( 2nd ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-j	⊢ 𝐽 = ( 𝑦 ∈ On , 𝑧 ∈ On , 𝑛 ∈ 9o ↦ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ) +o 𝑛 ) )
2		df-ot	⊢ ⟨ 𝑦 , 𝑧 , 𝑛 ⟩ = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑛 ⟩
3	2	eqeq2i	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑛 ⟩ ↔ 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑛 ⟩ )
4		opex	⊢ ⟨ 𝑦 , 𝑧 ⟩ ∈ V
5		vex	⊢ 𝑛 ∈ V
6	4 5	op1std	⊢ ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑛 ⟩ → ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 𝑧 ⟩ )
7	3 6	sylbi	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑛 ⟩ → ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 𝑧 ⟩ )
8	7	fveq2d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑛 ⟩ → ( 𝐽0 ‘ ( 1st ‘ 𝑥 ) ) = ( 𝐽0 ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
9	8	oveq2d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑛 ⟩ → ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑥 ) ) ) = ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ) )
10	4 5	op2ndd	⊢ ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑛 ⟩ → ( 2nd ‘ 𝑥 ) = 𝑛 )
11	3 10	sylbi	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑛 ⟩ → ( 2nd ‘ 𝑥 ) = 𝑛 )
12	9 11	oveq12d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑛 ⟩ → ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑥 ) ) ) +o ( 2nd ‘ 𝑥 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ) +o 𝑛 ) )
13	12	mpt3mpt	⊢ ( 𝑥 ∈ ( ( On × On ) × 9o ) ↦ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑥 ) ) ) +o ( 2nd ‘ 𝑥 ) ) ) = ( 𝑦 ∈ On , 𝑧 ∈ On , 𝑛 ∈ 9o ↦ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ) +o 𝑛 ) )
14	1 13	eqtr4i	⊢ 𝐽 = ( 𝑥 ∈ ( ( On × On ) × 9o ) ↦ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑥 ) ) ) +o ( 2nd ‘ 𝑥 ) ) )