Definition df-k3 35995

Description: Define a function that takes an ordinal and returns the third argument of the ordered triple ⟨𝑥, 𝑦, 𝑛⟩ such that the ordinal equals (𝐽‘⟨𝑥, 𝑦, 𝑛⟩). Based on the third case of Definition 15.7 of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 2-Sep-2026.)

Assertion

Ref	Expression
df-k3	⊢ 𝐾3 = {⟨𝑧, 𝑛⟩ ∣ (𝑛 ∈ 9o ∧ ∃𝑥 ∈ On ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))}

Distinct variable group:   𝑥,𝑛,𝑦,𝑧

Detailed syntax breakdown of Definition df-k3

Step	Hyp	Ref	Expression
1		ck3 35986	. 2 class 𝐾3
2		vn	. . . . . 6 setvar 𝑛
3	2	cv 1569	. . . . 5 class 𝑛
4		c9o 35857	. . . . 5 class 9o
5	3, 4	wcel 2147	. . . 4 wff 𝑛 ∈ 9o
6		vz	. . . . . . . 8 setvar 𝑧
7	6	cv 1569	. . . . . . 7 class 𝑧
8		vx	. . . . . . . . . 10 setvar 𝑥
9	8	cv 1569	. . . . . . . . 9 class 𝑥
10		vy	. . . . . . . . . 10 setvar 𝑦
11	10	cv 1569	. . . . . . . . 9 class 𝑦
12	9, 11, 3	cotp 4861	. . . . . . . 8 class ⟨𝑥, 𝑦, 𝑛⟩
13		cj 35983	. . . . . . . 8 class 𝐽
14	12, 13	cfv 6558	. . . . . . 7 class (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
15	7, 14	wceq 1570	. . . . . 6 wff 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
16		con0 6380	. . . . . 6 class On
17	15, 10, 16	wrex 3090	. . . . 5 wff ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
18	17, 8, 16	wrex 3090	. . . 4 wff ∃𝑥 ∈ On ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
19	5, 18	wa 401	. . 3 wff (𝑛 ∈ 9o ∧ ∃𝑥 ∈ On ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))
20	19, 6, 2	copab 5170	. 2 class {⟨𝑧, 𝑛⟩ ∣ (𝑛 ∈ 9o ∧ ∃𝑥 ∈ On ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))}
21	1, 20	wceq 1570	1 wff 𝐾3 = {⟨𝑧, 𝑛⟩ ∣ (𝑛 ∈ 9o ∧ ∃𝑥 ∈ On ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))}

This definition is used by:  dfk32  36014