Definition df-k2

Description: Define a function that takes an ordinal and returns the second argument of the ordered triple <. x , y , n >. such that the ordinal equals ( J<. x , y , n >. ) . Based on the second case of Definition 15.7 of TakeutiZaring p. 156. (Contributed by BTernaryTau, 2-Sep-2026)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ck2	⊢ 𝐾2
1		vz	⊢ 𝑧
2		vy	⊢ 𝑦
3	2	cv	⊢ 𝑦
4		con0	⊢ On
5	3 4	wcel	⊢ 𝑦 ∈ On
6		vn	⊢ 𝑛
7		c9o	⊢ 9o
8		vx	⊢ 𝑥
9	1	cv	⊢ 𝑧
10		cj	⊢ 𝐽
11	8	cv	⊢ 𝑥
12	6	cv	⊢ 𝑛
13	11 3 12	cotp	⊢ ⟨ 𝑥 , 𝑦 , 𝑛 ⟩
14	13 10	cfv	⊢ ( 𝐽 ‘ ⟨ 𝑥 , 𝑦 , 𝑛 ⟩ )
15	9 14	wceq	⊢ 𝑧 = ( 𝐽 ‘ ⟨ 𝑥 , 𝑦 , 𝑛 ⟩ )
16	15 8 4	wrex	⊢ ∃ 𝑥 ∈ On 𝑧 = ( 𝐽 ‘ ⟨ 𝑥 , 𝑦 , 𝑛 ⟩ )
17	16 6 7	wrex	⊢ ∃ 𝑛 ∈ 9o ∃ 𝑥 ∈ On 𝑧 = ( 𝐽 ‘ ⟨ 𝑥 , 𝑦 , 𝑛 ⟩ )
18	5 17	wa	⊢ ( 𝑦 ∈ On ∧ ∃ 𝑛 ∈ 9o ∃ 𝑥 ∈ On 𝑧 = ( 𝐽 ‘ ⟨ 𝑥 , 𝑦 , 𝑛 ⟩ ) )
19	18 1 2	copab	⊢ { ⟨ 𝑧 , 𝑦 ⟩ ∣ ( 𝑦 ∈ On ∧ ∃ 𝑛 ∈ 9o ∃ 𝑥 ∈ On 𝑧 = ( 𝐽 ‘ ⟨ 𝑥 , 𝑦 , 𝑛 ⟩ ) ) }
20	0 19	wceq	⊢ 𝐾2 = { ⟨ 𝑧 , 𝑦 ⟩ ∣ ( 𝑦 ∈ On ∧ ∃ 𝑛 ∈ 9o ∃ 𝑥 ∈ On 𝑧 = ( 𝐽 ‘ ⟨ 𝑥 , 𝑦 , 𝑛 ⟩ ) ) }