Metamath Proof Explorer

Theorem k3n0j0lt

Description: A strict upper bound on the value of _J0 for nonzero values of _K3 . (Contributed by BTernaryTau, 12-Oct-2026)

Ref Expression
Assertion k3n0j0lt 
|- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A )

Proof

Step Hyp Ref Expression
1 9on 
 |-  9o e. On
2 j0iso 
 |-  _J0 Isom _R0 , _E ( ( On X. On ) , On )
3 isof1o 
 |-  ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On )
4 f1of 
 |-  ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On )
5 2 3 4 mp2b 
 |-  _J0 : ( On X. On ) --> On
6 0elon 
 |-  (/) e. On
7 5 6 f0cli 
 |-  ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. On
8 omcl 
 |-  ( ( 9o e. On /\ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. On ) -> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. On )
9 1 7 8 mp2an 
 |-  ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. On
10 k39o 
 |-  ( _K3 ` A ) e. 9o
11 onelon 
 |-  ( ( 9o e. On /\ ( _K3 ` A ) e. 9o ) -> ( _K3 ` A ) e. On )
12 1 10 11 mp2an 
 |-  ( _K3 ` A ) e. On
13 oaord1 
 |-  ( ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. On /\ ( _K3 ` A ) e. On ) -> ( (/) e. ( _K3 ` A ) <-> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) ) )
14 9 12 13 mp2an 
 |-  ( (/) e. ( _K3 ` A ) <-> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) )
15 14 bilani 
 |-  ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) )
16 jk1k2k3 
 |-  ( A e. On -> A = ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) )
17 k1on 
 |-  ( _K1 ` A ) e. On
18 17 a1i 
 |-  ( A e. On -> ( _K1 ` A ) e. On )
19 k2on 
 |-  ( _K2 ` A ) e. On
20 19 a1i 
 |-  ( A e. On -> ( _K2 ` A ) e. On )
21 10 a1i 
 |-  ( A e. On -> ( _K3 ` A ) e. 9o )
22 ovexd 
 |-  ( A e. On -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) e. _V )
23 opeq1 
 |-  ( ( _K1 ` A ) = x -> <. ( _K1 ` A ) , y >. = <. x , y >. )
24 23 fveq2d 
 |-  ( ( _K1 ` A ) = x -> ( _J0 ` <. ( _K1 ` A ) , y >. ) = ( _J0 ` <. x , y >. ) )
25 24 oveq2d 
 |-  ( ( _K1 ` A ) = x -> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , y >. ) ) = ( 9o .o ( _J0 ` <. x , y >. ) ) )
26 25 oveq1d 
 |-  ( ( _K1 ` A ) = x -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , y >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) )
27 26 adantl 
 |-  ( ( A e. On /\ ( _K1 ` A ) = x ) -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , y >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) )
28 opeq2 
 |-  ( ( _K2 ` A ) = y -> <. ( _K1 ` A ) , ( _K2 ` A ) >. = <. ( _K1 ` A ) , y >. )
29 28 fveq2d 
 |-  ( ( _K2 ` A ) = y -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) = ( _J0 ` <. ( _K1 ` A ) , y >. ) )
30 29 oveq2d 
 |-  ( ( _K2 ` A ) = y -> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) = ( 9o .o ( _J0 ` <. ( _K1 ` A ) , y >. ) ) )
31 30 oveq1d 
 |-  ( ( _K2 ` A ) = y -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , y >. ) ) +o n ) )
32 31 adantl 
 |-  ( ( A e. On /\ ( _K2 ` A ) = y ) -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , y >. ) ) +o n ) )
33 oveq2 
 |-  ( ( _K3 ` A ) = n -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) = ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o n ) )
34 33 adantl 
 |-  ( ( A e. On /\ ( _K3 ` A ) = n ) -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) = ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o n ) )
35 df-j 
 |-  _J = ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) )
36 18 20 21 22 27 32 34 35 mpt3fvot2d 
 |-  ( A e. On -> ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) )
37 16 36 eqtrd 
 |-  ( A e. On -> A = ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) )
38 37 adantr 
 |-  ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> A = ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) )
39 15 38 eleqtrrd 
 |-  ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. A )
40 10 ne0ii 
 |-  9o =/= (/)
41 on0eln0 
 |-  ( 9o e. On -> ( (/) e. 9o <-> 9o =/= (/) ) )
42 1 41 ax-mp 
 |-  ( (/) e. 9o <-> 9o =/= (/) )
43 40 42 mpbir 
 |-  (/) e. 9o
44 omword2 
 |-  ( ( ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. On /\ 9o e. On ) /\ (/) e. 9o ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) )
45 43 44 mpan2 
 |-  ( ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. On /\ 9o e. On ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) )
46 7 1 45 mp2an 
 |-  ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) )
47 ontr2 
 |-  ( ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. On /\ A e. On ) -> ( ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) /\ ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. A ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) )
48 7 47 mpan 
 |-  ( A e. On -> ( ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) /\ ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. A ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) )
49 48 adantr 
 |-  ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) /\ ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. A ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) )
50 46 49 mpani 
 |-  ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. A -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) )
51 39 50 mpd 
 |-  ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A )