Metamath Proof Explorer

Theorem k39o

Description: Values of the _K3 function are ordinals less than 9. (Contributed by BTernaryTau, 11-Oct-2026)

Ref Expression
Assertion k39o 
|- ( _K3 ` A ) e. 9o

Proof

Step Hyp Ref Expression
1 2fveq3 
 |-  ( x = A -> ( 2nd ` ( `' _J ` x ) ) = ( 2nd ` ( `' _J ` A ) ) )
2 dfk32 
 |-  _K3 = ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) )
3 fvex 
 |-  ( 2nd ` ( `' _J ` A ) ) e. _V
4 1 2 3 fvmpt 
 |-  ( A e. On -> ( _K3 ` A ) = ( 2nd ` ( `' _J ` A ) ) )
5 jf1o 
 |-  _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On
6 f1ocnvdm 
 |-  ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ A e. On ) -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) )
7 5 6 mpan 
 |-  ( A e. On -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) )
8 xp2nd 
 |-  ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) -> ( 2nd ` ( `' _J ` A ) ) e. 9o )
9 7 8 syl 
 |-  ( A e. On -> ( 2nd ` ( `' _J ` A ) ) e. 9o )
10 4 9 eqeltrd 
 |-  ( A e. On -> ( _K3 ` A ) e. 9o )
11 2 fvmptndm 
 |-  ( -. A e. On -> ( _K3 ` A ) = (/) )
12 df-9o 
 |-  9o = suc 8o
13 nsuceq0 
 |-  suc 8o =/= (/)
14 12 13 eqnetri 
 |-  9o =/= (/)
15 9on 
 |-  9o e. On
16 on0eln0 
 |-  ( 9o e. On -> ( (/) e. 9o <-> 9o =/= (/) ) )
17 15 16 ax-mp 
 |-  ( (/) e. 9o <-> 9o =/= (/) )
18 14 17 mpbir 
 |-  (/) e. 9o
19 11 18 eqeltrdi 
 |-  ( -. A e. On -> ( _K3 ` A ) e. 9o )
20 10 19 pm2.61i 
 |-  ( _K3 ` A ) e. 9o