Definition df-j 35992

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 35983	. 2 class 𝐽
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		vn	. . 3 setvar 𝑛
5		con0 6380	. . 3 class On
6		c9o 35857	. . 3 class 9o
7	2	cv 1569	. . . . . . 7 class 𝑥
8	3	cv 1569	. . . . . . 7 class 𝑦
9	7, 8	cop 4838	. . . . . 6 class ⟨𝑥, 𝑦⟩
10		ccj0 35982	. . . . . 6 class 𝐽0
11	9, 10	cfv 6558	. . . . 5 class (𝐽0‘⟨𝑥, 𝑦⟩)
12		comu 8502	. . . . 5 class ·o
13	6, 11, 12	co 7443	. . . 4 class (9o ·o (𝐽0‘⟨𝑥, 𝑦⟩))
14	4	cv 1569	. . . 4 class 𝑛
15		coa 8501	. . . 4 class +o
16	13, 14, 15	co 7443	. . 3 class ((9o ·o (𝐽0‘⟨𝑥, 𝑦⟩)) +o 𝑛)
17	2, 3, 4, 5, 5, 6, 16	cmpt3 7707	. 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:  dfj2  36009  j0le  36019  k3n0j0lt  36020  jltaleph  36026