Definition df-k2 35926

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

Assertion

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

Distinct variable group:   𝑥,𝑛,𝑦,𝑧

Detailed syntax breakdown of Definition df-k2

Step	Hyp	Ref	Expression
1		ck2 35917	. 2 class 𝐾2
2		vy	. . . . . 6 setvar 𝑦
3	2	cv 1568	. . . . 5 class 𝑦
4		con0 6362	. . . . 5 class On
5	3, 4	wcel 2144	. . . 4 wff 𝑦 ∈ On
6		vz	. . . . . . . 8 setvar 𝑧
7	6	cv 1568	. . . . . . 7 class 𝑧
8		vx	. . . . . . . . . 10 setvar 𝑥
9	8	cv 1568	. . . . . . . . 9 class 𝑥
10		vn	. . . . . . . . . 10 setvar 𝑛
11	10	cv 1568	. . . . . . . . 9 class 𝑛
12	9, 3, 11	cotp 4591	. . . . . . . 8 class ⟨𝑥, 𝑦, 𝑛⟩
13		cj 35915	. . . . . . . 8 class 𝐽
14	12, 13	cfv 6538	. . . . . . 7 class (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
15	7, 14	wceq 1569	. . . . . 6 wff 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
16	15, 8, 4	wrex 3086	. . . . 5 wff ∃𝑥 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
17		c9o 35814	. . . . 5 class 9o
18	16, 10, 17	wrex 3086	. . . 4 wff ∃𝑛 ∈ 9o ∃𝑥 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
19	5, 18	wa 401	. . 3 wff (𝑦 ∈ On ∧ ∃𝑛 ∈ 9o ∃𝑥 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))
20	19, 6, 2	copab 5166	. 2 class {⟨𝑧, 𝑦⟩ ∣ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9o ∃𝑥 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))}
21	1, 20	wceq 1569	1 wff 𝐾2 = {⟨𝑧, 𝑦⟩ ∣ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9o ∃𝑥 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))}

This definition is used by: (None)