Definition df-k3

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

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

Detailed syntax breakdown

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