Metamath Proof Explorer

Theorem j0le

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

Ref Expression
Assertion j0le Could not format assertion : No typesetting found for |- ( A e. On -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ A ) with typecode |-

Proof

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