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	|- _K2 = { <. z , y >. | ( y e. On /\ E. n e. 9o E. x e. On z = ( _J ` <. x , y , n >. ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ck2	|- _K2
1		vz	|- z
2		vy	|- y
3	2	cv	|- y
4		con0	|- On
5	3 4	wcel	|- y e. On
6		vn	|- n
7		c9o	|- 9o
8		vx	|- x
9	1	cv	|- z
10		cj	|- _J
11	8	cv	|- x
12	6	cv	|- n
13	11 3 12	cotp	|- <. x , y , n >.
14	13 10	cfv	|- ( _J ` <. x , y , n >. )
15	9 14	wceq	|- z = ( _J ` <. x , y , n >. )
16	15 8 4	wrex	|- E. x e. On z = ( _J ` <. x , y , n >. )
17	16 6 7	wrex	|- E. n e. 9o E. x e. On z = ( _J ` <. x , y , n >. )
18	5 17	wa	|- ( y e. On /\ E. n e. 9o E. x e. On z = ( _J ` <. x , y , n >. ) )
19	18 1 2	copab	|- { <. z , y >. | ( y e. On /\ E. n e. 9o E. x e. On z = ( _J ` <. x , y , n >. ) ) }
20	0 19	wceq	|- _K2 = { <. z , y >. | ( y e. On /\ E. n e. 9o E. x e. On z = ( _J ` <. x , y , n >. ) ) }