Metamath Proof Explorer

Theorem j0le

Description: An upper bound on the value of _J0 . (Contributed by BTernaryTau, 12-Oct-2026)

Ref Expression
Assertion j0le 
|- ( A e. On -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ A )

Proof

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