Theorem j0le

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

	Ref	Expression
Assertion	j0le	⊢ ( 𝐴 ∈ On → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ⊆ 𝐴 )

Proof

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