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	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		9on	⊢ 9o ∈ On
2		j0iso	⊢ 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On )
3		isof1o	⊢ ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) → 𝐽0 : ( On × On ) –1-1-onto→ On )
4		f1of	⊢ ( 𝐽0 : ( On × On ) –1-1-onto→ On → 𝐽0 : ( On × On ) ⟶ On )
5	2 3 4	mp2b	⊢ 𝐽0 : ( On × On ) ⟶ On
6		0elon	⊢ ∅ ∈ On
7	5 6	f0cli	⊢ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ On
8		omcl	⊢ ( ( 9o ∈ On ∧ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ On ) → ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ On )
9	1 7 8	mp2an	⊢ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ On
10		k39o	⊢ ( 𝐾3 ‘ 𝐴 ) ∈ 9o
11		onelon	⊢ ( ( 9o ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ∈ 9o ) → ( 𝐾3 ‘ 𝐴 ) ∈ On )
12	1 10 11	mp2an	⊢ ( 𝐾3 ‘ 𝐴 ) ∈ On
13		oaord1	⊢ ( ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ∈ On ) → ( ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ↔ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o ( 𝐾3 ‘ 𝐴 ) ) ) )
14	9 12 13	mp2an	⊢ ( ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ↔ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o ( 𝐾3 ‘ 𝐴 ) ) )
15	14	bilani	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o ( 𝐾3 ‘ 𝐴 ) ) )
16		jk1k2k3	⊢ ( 𝐴 ∈ On → 𝐴 = ( 𝐽 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) )
17		k1on	⊢ ( 𝐾1 ‘ 𝐴 ) ∈ On
18	17	a1i	⊢ ( 𝐴 ∈ On → ( 𝐾1 ‘ 𝐴 ) ∈ On )
19		k2on	⊢ ( 𝐾2 ‘ 𝐴 ) ∈ On
20	19	a1i	⊢ ( 𝐴 ∈ On → ( 𝐾2 ‘ 𝐴 ) ∈ On )
21	10	a1i	⊢ ( 𝐴 ∈ On → ( 𝐾3 ‘ 𝐴 ) ∈ 9o )
22		ovexd	⊢ ( 𝐴 ∈ On → ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o ( 𝐾3 ‘ 𝐴 ) ) ∈ V )
23		opeq1	⊢ ( ( 𝐾1 ‘ 𝐴 ) = 𝑥 → ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
24	23	fveq2d	⊢ ( ( 𝐾1 ‘ 𝐴 ) = 𝑥 → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ ) = ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
25	24	oveq2d	⊢ ( ( 𝐾1 ‘ 𝐴 ) = 𝑥 → ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ ) ) = ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
26	25	oveq1d	⊢ ( ( 𝐾1 ‘ 𝐴 ) = 𝑥 → ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ ) ) +o 𝑛 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 ) )
27	26	adantl	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾1 ‘ 𝐴 ) = 𝑥 ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ ) ) +o 𝑛 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 ) )
28		opeq2	⊢ ( ( 𝐾2 ‘ 𝐴 ) = 𝑦 → ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ = ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ )
29	28	fveq2d	⊢ ( ( 𝐾2 ‘ 𝐴 ) = 𝑦 → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) = ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ ) )
30	29	oveq2d	⊢ ( ( 𝐾2 ‘ 𝐴 ) = 𝑦 → ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) = ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ ) ) )
31	30	oveq1d	⊢ ( ( 𝐾2 ‘ 𝐴 ) = 𝑦 → ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o 𝑛 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ ) ) +o 𝑛 ) )
32	31	adantl	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾2 ‘ 𝐴 ) = 𝑦 ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o 𝑛 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , 𝑦 ⟩ ) ) +o 𝑛 ) )
33		oveq2	⊢ ( ( 𝐾3 ‘ 𝐴 ) = 𝑛 → ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o ( 𝐾3 ‘ 𝐴 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o 𝑛 ) )
34	33	adantl	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = 𝑛 ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o ( 𝐾3 ‘ 𝐴 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o 𝑛 ) )
35		df-j	⊢ 𝐽 = ( 𝑥 ∈ On , 𝑦 ∈ On , 𝑛 ∈ 9o ↦ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 ) )
36	18 20 21 22 27 32 34 35	mpt3fvot2d	⊢ ( 𝐴 ∈ On → ( 𝐽 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o ( 𝐾3 ‘ 𝐴 ) ) )
37	16 36	eqtrd	⊢ ( 𝐴 ∈ On → 𝐴 = ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o ( 𝐾3 ‘ 𝐴 ) ) )
38	37	adantr	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → 𝐴 = ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) +o ( 𝐾3 ‘ 𝐴 ) ) )
39	15 38	eleqtrrd	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ 𝐴 )
40	10	ne0ii	⊢ 9o ≠ ∅
41		on0eln0	⊢ ( 9o ∈ On → ( ∅ ∈ 9o ↔ 9o ≠ ∅ ) )
42	1 41	ax-mp	⊢ ( ∅ ∈ 9o ↔ 9o ≠ ∅ )
43	40 42	mpbir	⊢ ∅ ∈ 9o
44		omword2	⊢ ( ( ( ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ On ∧ 9o ∈ On ) ∧ ∅ ∈ 9o ) → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ⊆ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) )
45	43 44	mpan2	⊢ ( ( ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ On ∧ 9o ∈ On ) → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ⊆ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) )
46	7 1 45	mp2an	⊢ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ⊆ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) )
47		ontr2	⊢ ( ( ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ On ∧ 𝐴 ∈ On ) → ( ( ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ⊆ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∧ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ 𝐴 ) → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 ) )
48	7 47	mpan	⊢ ( 𝐴 ∈ On → ( ( ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ⊆ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∧ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ 𝐴 ) → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 ) )
49	48	adantr	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( ( ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ⊆ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∧ ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ 𝐴 ) → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 ) )
50	46 49	mpani	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ) ∈ 𝐴 → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 ) )
51	39 50	mpd	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 )