Metamath Proof Explorer

Theorem k1on

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

Ref Expression
Assertion k1on 
|- ( _K1 ` A ) e. On

Proof

Step Hyp Ref Expression
1 2fveq3 
 |-  ( x = A -> ( 1st ` ( `' _J ` x ) ) = ( 1st ` ( `' _J ` A ) ) )
2 1 fveq2d 
 |-  ( x = A -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) = ( 1st ` ( 1st ` ( `' _J ` A ) ) ) )
3 dfk12 
 |-  _K1 = ( x e. On |-> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) )
4 fvex 
 |-  ( 1st ` ( 1st ` ( `' _J ` A ) ) ) e. _V
5 2 3 4 fvmpt 
 |-  ( A e. On -> ( _K1 ` A ) = ( 1st ` ( 1st ` ( `' _J ` A ) ) ) )
6 jf1o 
 |-  _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On
7 f1ocnvdm 
 |-  ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ A e. On ) -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) )
8 6 7 mpan 
 |-  ( A e. On -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) )
9 xp1st 
 |-  ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) -> ( 1st ` ( `' _J ` A ) ) e. ( On X. On ) )
10 xp1st 
 |-  ( ( 1st ` ( `' _J ` A ) ) e. ( On X. On ) -> ( 1st ` ( 1st ` ( `' _J ` A ) ) ) e. On )
11 8 9 10 3syl 
 |-  ( A e. On -> ( 1st ` ( 1st ` ( `' _J ` A ) ) ) e. On )
12 5 11 eqeltrd 
 |-  ( A e. On -> ( _K1 ` A ) e. On )
13 3 fvmptndm 
 |-  ( -. A e. On -> ( _K1 ` A ) = (/) )
14 0elon 
 |-  (/) e. On
15 13 14 eqeltrdi 
 |-  ( -. A e. On -> ( _K1 ` A ) e. On )
16 12 15 pm2.61i 
 |-  ( _K1 ` A ) e. On