Theorem jltalephlem

Description: Lemma for jltaleph . (Contributed by BTernaryTau, 16-Oct-2026)

	Ref	Expression
Assertion	jltalephlem	⊢ ( ( 𝐶 ∈ 9o ∧ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )

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 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On
8		omxpen	⊢ ( ( 9o ∈ On ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On ) → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( 9o × ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
9	1 7 8	mp2an	⊢ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( 9o × ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
10		9onn	⊢ 9o ∈ ω
11	10	elexi	⊢ 9o ∈ V
12		fvex	⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V
13	11 12	xpcomen	⊢ ( 9o × ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) × 9o )
14	9 13	entri	⊢ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) × 9o )
15		nnfi	⊢ ( 9o ∈ ω → 9o ∈ Fin )
16		fict	⊢ ( 9o ∈ Fin → 9o ≼ ω )
17	10 15 16	mp2b	⊢ 9o ≼ ω
18		domtr	⊢ ( ( 9o ≼ ω ∧ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → 9o ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
19	17 18	mpan	⊢ ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → 9o ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
20		df-9o	⊢ 9o = suc 8o
21		nsuceq0	⊢ suc 8o ≠ ∅
22	20 21	eqnetri	⊢ 9o ≠ ∅
23		onenon	⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ dom card )
24	7 23	ax-mp	⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ dom card
25		infxpabs	⊢ ( ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ dom card ∧ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 9o ≠ ∅ ∧ 9o ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) × 9o ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
26	24 25	mpanl1	⊢ ( ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 9o ≠ ∅ ∧ 9o ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) × 9o ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
27	22 26	mpanr1	⊢ ( ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∧ 9o ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) × 9o ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
28	19 27	mpdan	⊢ ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) × 9o ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
29		entr	⊢ ( ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) × 9o ) ∧ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) × 9o ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
30	14 28 29	sylancr	⊢ ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
31		ensym	⊢ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≈ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
32		domentr	⊢ ( ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≈ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
33	31 32	sylan2	⊢ ( ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
34	30 33	mpdan	⊢ ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
35		omcl	⊢ ( ( 9o ∈ On ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On ) → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ On )
36	1 7 35	mp2an	⊢ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ On
37	1	oneli	⊢ ( 𝐶 ∈ 9o → 𝐶 ∈ On )
38		onadju	⊢ ( ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ On ∧ 𝐶 ∈ On ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ⊔ 𝐶 ) )
39	36 37 38	sylancr	⊢ ( 𝐶 ∈ 9o → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ⊔ 𝐶 ) )
40		onenon	⊢ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ On → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ dom card )
41	36 40	ax-mp	⊢ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ dom card
42		simpr	⊢ ( ( 𝐶 ∈ 9o ∧ ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
43		elnn	⊢ ( ( 𝐶 ∈ 9o ∧ 9o ∈ ω ) → 𝐶 ∈ ω )
44	10 43	mpan2	⊢ ( 𝐶 ∈ 9o → 𝐶 ∈ ω )
45		nnfi	⊢ ( 𝐶 ∈ ω → 𝐶 ∈ Fin )
46		fict	⊢ ( 𝐶 ∈ Fin → 𝐶 ≼ ω )
47	44 45 46	3syl	⊢ ( 𝐶 ∈ 9o → 𝐶 ≼ ω )
48		domtr	⊢ ( ( 𝐶 ≼ ω ∧ ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝐶 ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
49	47 48	sylan	⊢ ( ( 𝐶 ∈ 9o ∧ ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝐶 ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
50		infdjuabs	⊢ ( ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ dom card ∧ ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ 𝐶 ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ⊔ 𝐶 ) ≈ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
51	41 42 49 50	mp3an2i	⊢ ( ( 𝐶 ∈ 9o ∧ ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ⊔ 𝐶 ) ≈ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
52		entr	⊢ ( ( ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ⊔ 𝐶 ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ⊔ 𝐶 ) ≈ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
53	39 51 52	syl2an2r	⊢ ( ( 𝐶 ∈ 9o ∧ ω ≼ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
54	34 53	sylan2	⊢ ( ( 𝐶 ∈ 9o ∧ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
55	30	adantl	⊢ ( ( 𝐶 ∈ 9o ∧ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
56		entr	⊢ ( ( ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
57	54 55 56	syl2anc	⊢ ( ( 𝐶 ∈ 9o ∧ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )