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	Could not format assertion : No typesetting found for |- _K3 = { <. z , n >. | ( n e. 9o /\ E. x e. On E. y e. On z = ( _J ` <. x , y , n >. ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ck3	Could not format _K3 : No typesetting found for class _K3 with typecode class
1		vz	$$setvarz$$
2		vn	$$setvarn$$
3	2	cv	$$setvarn$$
4		c9o	Could not format 9o : No typesetting found for class 9o with typecode class
5	3 4	wcel	Could not format n e. 9o : No typesetting found for wff n e. 9o with typecode wff
6		vx	$$setvarx$$
7		con0	$$class\mathrm{On}$$
8		vy	$$setvary$$
9	1	cv	$$setvarz$$
10		cj	Could not format _J : No typesetting found for class _J with typecode class
11	6	cv	$$setvarx$$
12	8	cv	$$setvary$$
13	11 12 3	cotp	$$class⟨x,y,n⟩$$
14	13 10	cfv	Could not format ( _J ` <. x , y , n >. ) : No typesetting found for class ( _J ` <. x , y , n >. ) with typecode class
15	9 14	wceq	Could not format z = ( _J ` <. x , y , n >. ) : No typesetting found for wff z = ( _J ` <. x , y , n >. ) with typecode wff
16	15 8 7	wrex	Could not format E. y e. On z = ( _J ` <. x , y , n >. ) : No typesetting found for wff E. y e. On z = ( _J ` <. x , y , n >. ) with typecode wff
17	16 6 7	wrex	Could not format E. x e. On E. y e. On z = ( _J ` <. x , y , n >. ) : No typesetting found for wff E. x e. On E. y e. On z = ( _J ` <. x , y , n >. ) with typecode wff
18	5 17	wa	Could not format ( n e. 9o /\ E. x e. On E. y e. On z = ( _J ` <. x , y , n >. ) ) : No typesetting found for wff ( n e. 9o /\ E. x e. On E. y e. On z = ( _J ` <. x , y , n >. ) ) with typecode wff
19	18 1 2	copab	Could not format { <. z , n >. | ( n e. 9o /\ E. x e. On E. y e. On z = ( _J ` <. x , y , n >. ) ) } : No typesetting found for class { <. z , n >. | ( n e. 9o /\ E. x e. On E. y e. On z = ( _J ` <. x , y , n >. ) ) } with typecode class
20	0 19	wceq	Could not format _K3 = { <. z , n >. | ( n e. 9o /\ E. x e. On E. y e. On z = ( _J ` <. x , y , n >. ) ) } : No typesetting found for wff _K3 = { <. z , n >. | ( n e. 9o /\ E. x e. On E. y e. On z = ( _J ` <. x , y , n >. ) ) } with typecode wff