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	⊢ 𝐽 = ( 𝑥 ∈ On , 𝑦 ∈ On , 𝑛 ∈ 9o ↦ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cj	⊢ 𝐽
1		vx	⊢ 𝑥
2		con0	⊢ On
3		vy	⊢ 𝑦
4		vn	⊢ 𝑛
5		c9o	⊢ 9o
6		comu	⊢ ·o
7		ccj0	⊢ 𝐽0
8	1	cv	⊢ 𝑥
9	3	cv	⊢ 𝑦
10	8 9	cop	⊢ ⟨ 𝑥 , 𝑦 ⟩
11	10 7	cfv	⊢ ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
12	5 11 6	co	⊢ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
13		coa	⊢ +o
14	4	cv	⊢ 𝑛
15	12 14 13	co	⊢ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 )
16	1 3 4 2 2 5 15	cmpt3	⊢ ( 𝑥 ∈ On , 𝑦 ∈ On , 𝑛 ∈ 9o ↦ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 ) )
17	0 16	wceq	⊢ 𝐽 = ( 𝑥 ∈ On , 𝑦 ∈ On , 𝑛 ∈ 9o ↦ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 ) )