Theorem k2on

Description: Values of the _K2 function are ordinals. (Contributed by BTernaryTau, 11-Oct-2026)

	Ref	Expression
Assertion	k2on	Could not format assertion : No typesetting found for |- ( _K2 ` A ) e. On with typecode |-

Proof

Step	Hyp	Ref	Expression
1		2fveq3	Could not format ( x = A -> ( 1st ` ( `' _J ` x ) ) = ( 1st ` ( `' _J ` A ) ) ) : No typesetting found for |- ( x = A -> ( 1st ` ( `' _J ` x ) ) = ( 1st ` ( `' _J ` A ) ) ) with typecode |-
2	1	fveq2d	Could not format ( x = A -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) ) : No typesetting found for |- ( x = A -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) ) with typecode |-
3		dfk22	Could not format _K2 = ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) : No typesetting found for |- _K2 = ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) with typecode |-
4		fvex	Could not format ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) e. _V : No typesetting found for |- ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) e. _V with typecode |-
5	2 3 4	fvmpt	Could not format ( A e. On -> ( _K2 ` A ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) ) : No typesetting found for |- ( A e. On -> ( _K2 ` A ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) ) with typecode |-
6		jf1o	Could not format _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On : No typesetting found for |- _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On with typecode |-
7		f1ocnvdm	Could not format ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ A e. On ) -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) ) : No typesetting found for |- ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ A e. On ) -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) ) with typecode |-
8	6 7	mpan	Could not format ( A e. On -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) ) : No typesetting found for |- ( A e. On -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) ) with typecode |-
9		xp1st	Could not format ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) -> ( 1st ` ( `' _J ` A ) ) e. ( On X. On ) ) : No typesetting found for |- ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) -> ( 1st ` ( `' _J ` A ) ) e. ( On X. On ) ) with typecode |-
10		xp2nd	Could not format ( ( 1st ` ( `' _J ` A ) ) e. ( On X. On ) -> ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) e. On ) : No typesetting found for |- ( ( 1st ` ( `' _J ` A ) ) e. ( On X. On ) -> ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) e. On ) with typecode |-
11	8 9 10	3syl	Could not format ( A e. On -> ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) e. On ) : No typesetting found for |- ( A e. On -> ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) e. On ) with typecode |-
12	5 11	eqeltrd	Could not format ( A e. On -> ( _K2 ` A ) e. On ) : No typesetting found for |- ( A e. On -> ( _K2 ` A ) e. On ) with typecode |-
13	3	fvmptndm	Could not format ( -. A e. On -> ( _K2 ` A ) = (/) ) : No typesetting found for |- ( -. A e. On -> ( _K2 ` A ) = (/) ) with typecode |-
14		0elon	$$⊢\varnothing \in \mathrm{On}$$
15	13 14	eqeltrdi	Could not format ( -. A e. On -> ( _K2 ` A ) e. On ) : No typesetting found for |- ( -. A e. On -> ( _K2 ` A ) e. On ) with typecode |-
16	12 15	pm2.61i	Could not format ( _K2 ` A ) e. On : No typesetting found for |- ( _K2 ` A ) e. On with typecode |-