Definition df-k1 35801

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

Assertion

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

Distinct variable group:   𝑥,𝑛,𝑦,𝑧

Detailed syntax breakdown of Definition df-k1

Step	Hyp	Ref	Expression
1		ck1 35792	. 2 class 𝐾1
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1569	. . . . 5 class 𝑥
4		con0 6351	. . . . 5 class On
5	3, 4	wcel 2145	. . . 4 wff 𝑥 ∈ On
6		vz	. . . . . . . 8 setvar 𝑧
7	6	cv 1569	. . . . . . 7 class 𝑧
8		vy	. . . . . . . . . 10 setvar 𝑦
9	8	cv 1569	. . . . . . . . 9 class 𝑦
10		vn	. . . . . . . . . 10 setvar 𝑛
11	10	cv 1569	. . . . . . . . 9 class 𝑛
12	3, 9, 11	cotp 4591	. . . . . . . 8 class ⟨𝑥, 𝑦, 𝑛⟩
13		cj 35791	. . . . . . . 8 class 𝐽
14	12, 13	cfv 6527	. . . . . . 7 class (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
15	7, 14	wceq 1570	. . . . . 6 wff 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
16	15, 8, 4	wrex 3086	. . . . 5 wff ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩)
17		c9o 35690	. . . . 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 1570	1 wff 𝐾1 = {⟨𝑧, 𝑥⟩ ∣ (𝑥 ∈ On ∧ ∃𝑛 ∈ 9o ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))}

This definition is used by: (None)