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	Could not format assertion : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		9on	Could not format 9o e. On : No typesetting found for |- 9o e. On with typecode |-
2		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 |-
3		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 |-
4		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 |-
5	2 3 4	mp2b	Could not format _J0 : ( On X. On ) --> On : No typesetting found for |- _J0 : ( On X. On ) --> On with typecode |-
6		0elon	$$⊢\varnothing \in \mathrm{On}$$
7	5 6	f0cli	Could not format ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. On : No typesetting found for |- ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. On with typecode |-
8		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 |-
9	1 7 8	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 |-
10		k39o	Could not format ( _K3 ` A ) e. 9o : No typesetting found for |- ( _K3 ` A ) e. 9o with typecode |-
11		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 |-
12	1 10 11	mp2an	Could not format ( _K3 ` A ) e. On : No typesetting found for |- ( _K3 ` A ) e. On with typecode |-
13		oaord1	Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
14	9 12 13	mp2an	Could not format ( (/) e. ( _K3 ` A ) <-> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) ) : No typesetting found for |- ( (/) e. ( _K3 ` A ) <-> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) ) with typecode |-
15	14	bilani	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) ) with typecode |-
16		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 |-
17		k1on	Could not format ( _K1 ` A ) e. On : No typesetting found for |- ( _K1 ` A ) e. On with typecode |-
18	17	a1i	Could not format ( A e. On -> ( _K1 ` A ) e. On ) : No typesetting found for |- ( A e. On -> ( _K1 ` A ) e. On ) with typecode |-
19		k2on	Could not format ( _K2 ` A ) e. On : No typesetting found for |- ( _K2 ` A ) e. On with typecode |-
20	19	a1i	Could not format ( A e. On -> ( _K2 ` A ) e. On ) : No typesetting found for |- ( A e. On -> ( _K2 ` A ) e. On ) with typecode |-
21	10	a1i	Could not format ( A e. On -> ( _K3 ` A ) e. 9o ) : No typesetting found for |- ( A e. On -> ( _K3 ` A ) e. 9o ) with typecode |-
22		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 |-
23		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 |-
24	23	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 |-
25	24	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 |-
26	25	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 |-
27	26	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 |-
28		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 |-
29	28	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 |-
30	29	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 |-
31	30	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 |-
32	31	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 |-
33		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 |-
34	33	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 |-
35		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 |-
36	18 20 21 22 27 32 34 35	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 |-
37	16 36	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 |-
38	37	adantr	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> A = ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> A = ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) +o ( _K3 ` A ) ) ) with typecode |-
39	15 38	eleqtrrd	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. A ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. A ) with typecode |-
40	10	ne0ii	Could not format 9o =/= (/) : No typesetting found for |- 9o =/= (/) with typecode |-
41		on0eln0	Could not format ( 9o e. On -> ( (/) e. 9o <-> 9o =/= (/) ) ) : No typesetting found for |- ( 9o e. On -> ( (/) e. 9o <-> 9o =/= (/) ) ) with typecode |-
42	1 41	ax-mp	Could not format ( (/) e. 9o <-> 9o =/= (/) ) : No typesetting found for |- ( (/) e. 9o <-> 9o =/= (/) ) with typecode |-
43	40 42	mpbir	Could not format (/) e. 9o : No typesetting found for |- (/) e. 9o with typecode |-
44		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 |-
45	43 44	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 |-
46	7 1 45	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 |-
47		ontr2	Could not format ( ( ( _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 ) ) : No typesetting found for |- ( ( ( _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 ) ) with typecode |-
48	7 47	mpan	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
49	48	adantr	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
50	46 49	mpani	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. A -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( 9o .o ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) e. A -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) ) with typecode |-
51	39 50	mpd	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) with typecode |-