Definition df-j 35800

Description: Define an order isomorphism from (On × On) × 9_o to On. Based on Definition 15.2 of [TakeutiZaring] p. 155. (Contributed by BTernaryTau, 2-Sep-2026.)

Assertion

Ref	Expression
df-j	⊢ 𝐽 = (𝑥 ∈ On, 𝑦 ∈ On, 𝑛 ∈ 9o ↦ ((9o ·o (𝐽0‘⟨𝑥, 𝑦⟩)) +o 𝑛))

Distinct variable group:   𝑥,𝑛,𝑦

Detailed syntax breakdown of Definition df-j

Step	Hyp	Ref	Expression
1		cj 35791	. 2 class 𝐽
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		vn	. . 3 setvar 𝑛
5		con0 6351	. . 3 class On
6		c9o 35690	. . 3 class 9o
7	2	cv 1569	. . . . . . 7 class 𝑥
8	3	cv 1569	. . . . . . 7 class 𝑦
9	7, 8	cop 4589	. . . . . 6 class ⟨𝑥, 𝑦⟩
10		ccj0 35790	. . . . . 6 class 𝐽0
11	9, 10	cfv 6527	. . . . 5 class (𝐽0‘⟨𝑥, 𝑦⟩)
12		comu 8452	. . . . 5 class ·o
13	6, 11, 12	co 7408	. . . 4 class (9o ·o (𝐽0‘⟨𝑥, 𝑦⟩))
14	4	cv 1569	. . . 4 class 𝑛
15		coa 8451	. . . 4 class +o
16	13, 14, 15	co 7408	. . 3 class ((9o ·o (𝐽0‘⟨𝑥, 𝑦⟩)) +o 𝑛)
17	2, 3, 4, 5, 5, 6, 16	cmpt3 7671	. 2 class (𝑥 ∈ On, 𝑦 ∈ On, 𝑛 ∈ 9o ↦ ((9o ·o (𝐽0‘⟨𝑥, 𝑦⟩)) +o 𝑛))
18	1, 17	wceq 1570	1 wff 𝐽 = (𝑥 ∈ On, 𝑦 ∈ On, 𝑛 ∈ 9o ↦ ((9o ·o (𝐽0‘⟨𝑥, 𝑦⟩)) +o 𝑛))

This definition is used by: (None)