Theorem onmcl

Description: If an ordinal is less than a power of omega, the product with a natural number is also less than that power of omega. (Contributed by RP, 19-Feb-2025)

	Ref	Expression
Assertion	onmcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) → ( 𝐴 ∈ ( ω ↑o 𝐵 ) → ( 𝐴 ·o 𝑁 ) ∈ ( ω ↑o 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ·o 𝑁 ) = ( ∅ ·o 𝑁 ) )
2		simp3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) → 𝑁 ∈ ω )
3		nnon	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ On )
4		om0r	⊢ ( 𝑁 ∈ On → ( ∅ ·o 𝑁 ) = ∅ )
5	2 3 4	3syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) → ( ∅ ·o 𝑁 ) = ∅ )
6	1 5	sylan9eqr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ 𝐴 = ∅ ) → ( 𝐴 ·o 𝑁 ) = ∅ )
7		simpl2	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ 𝐴 = ∅ ) → 𝐵 ∈ On )
8		omelon	⊢ ω ∈ On
9	7 8	jctil	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ 𝐴 = ∅ ) → ( ω ∈ On ∧ 𝐵 ∈ On ) )
10		peano1	⊢ ∅ ∈ ω
11		oen0	⊢ ( ( ( ω ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 𝐵 ) )
12	9 10 11	sylancl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ 𝐴 = ∅ ) → ∅ ∈ ( ω ↑o 𝐵 ) )
13	6 12	eqeltrd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ 𝐴 = ∅ ) → ( 𝐴 ·o 𝑁 ) ∈ ( ω ↑o 𝐵 ) )
14	13	a1d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ 𝐴 = ∅ ) → ( 𝐴 ∈ ( ω ↑o 𝐵 ) → ( 𝐴 ·o 𝑁 ) ∈ ( ω ↑o 𝐵 ) ) )
15	2	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ ∅ ∈ 𝐴 ) → 𝑁 ∈ ω )
16		simp1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) → 𝐴 ∈ On )
17	16	anim1i	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )
18		ondif1	⊢ ( 𝐴 ∈ ( On ∖ 1o ) ↔ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )
19	17 18	sylibr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ ∅ ∈ 𝐴 ) → 𝐴 ∈ ( On ∖ 1o ) )
20		simpl2	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ ∅ ∈ 𝐴 ) → 𝐵 ∈ On )
21		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o ∅ ) )
22	21	eleq1d	⊢ ( 𝑥 = ∅ → ( ( 𝐴 ·o 𝑥 ) ∈ ( ω ↑o 𝐵 ) ↔ ( 𝐴 ·o ∅ ) ∈ ( ω ↑o 𝐵 ) ) )
23	22	imbi2d	⊢ ( 𝑥 = ∅ → ( ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o 𝑥 ) ∈ ( ω ↑o 𝐵 ) ) ↔ ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o ∅ ) ∈ ( ω ↑o 𝐵 ) ) ) )
24		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝑦 ) )
25	24	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·o 𝑥 ) ∈ ( ω ↑o 𝐵 ) ↔ ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) )
26	25	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o 𝑥 ) ∈ ( ω ↑o 𝐵 ) ) ↔ ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) ) )
27		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o suc 𝑦 ) )
28	27	eleq1d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ·o 𝑥 ) ∈ ( ω ↑o 𝐵 ) ↔ ( 𝐴 ·o suc 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) )
29	28	imbi2d	⊢ ( 𝑥 = suc 𝑦 → ( ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o 𝑥 ) ∈ ( ω ↑o 𝐵 ) ) ↔ ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o suc 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) ) )
30		oveq2	⊢ ( 𝑥 = 𝑁 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝑁 ) )
31	30	eleq1d	⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 ·o 𝑥 ) ∈ ( ω ↑o 𝐵 ) ↔ ( 𝐴 ·o 𝑁 ) ∈ ( ω ↑o 𝐵 ) ) )
32	31	imbi2d	⊢ ( 𝑥 = 𝑁 → ( ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o 𝑥 ) ∈ ( ω ↑o 𝐵 ) ) ↔ ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o 𝑁 ) ∈ ( ω ↑o 𝐵 ) ) ) )
33		eldifi	⊢ ( 𝐴 ∈ ( On ∖ 1o ) → 𝐴 ∈ On )
34		om0	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ )
35	33 34	syl	⊢ ( 𝐴 ∈ ( On ∖ 1o ) → ( 𝐴 ·o ∅ ) = ∅ )
36	35	adantr	⊢ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) → ( 𝐴 ·o ∅ ) = ∅ )
37	8	jctl	⊢ ( 𝐵 ∈ On → ( ω ∈ On ∧ 𝐵 ∈ On ) )
38	37 10 11	sylancl	⊢ ( 𝐵 ∈ On → ∅ ∈ ( ω ↑o 𝐵 ) )
39	38	adantl	⊢ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) → ∅ ∈ ( ω ↑o 𝐵 ) )
40	36 39	eqeltrd	⊢ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) → ( 𝐴 ·o ∅ ) ∈ ( ω ↑o 𝐵 ) )
41	40	adantr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o ∅ ) ∈ ( ω ↑o 𝐵 ) )
42	33	adantr	⊢ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) → 𝐴 ∈ On )
43	42	ad2antrl	⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ) → 𝐴 ∈ On )
44		simpll	⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) → 𝑦 ∈ ω )
45		onmsuc	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ ω ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
46	43 44 45	syl2an2r	⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
47		simpr	⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) )
48		simplrr	⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) → 𝐴 ∈ ( ω ↑o 𝐵 ) )
49		eqid	⊢ ( ω ↑o 𝐵 ) = ( ω ↑o 𝐵 )
50	49	jctl	⊢ ( 𝐵 ∈ On → ( ( ω ↑o 𝐵 ) = ( ω ↑o 𝐵 ) ∧ 𝐵 ∈ On ) )
51	50	olcd	⊢ ( 𝐵 ∈ On → ( ( ω ↑o 𝐵 ) = ∅ ∨ ( ( ω ↑o 𝐵 ) = ( ω ↑o 𝐵 ) ∧ 𝐵 ∈ On ) ) )
52	51	adantl	⊢ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) → ( ( ω ↑o 𝐵 ) = ∅ ∨ ( ( ω ↑o 𝐵 ) = ( ω ↑o 𝐵 ) ∧ 𝐵 ∈ On ) ) )
53	52	ad2antrl	⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ) → ( ( ω ↑o 𝐵 ) = ∅ ∨ ( ( ω ↑o 𝐵 ) = ( ω ↑o 𝐵 ) ∧ 𝐵 ∈ On ) ) )
54	53	adantr	⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) → ( ( ω ↑o 𝐵 ) = ∅ ∨ ( ( ω ↑o 𝐵 ) = ( ω ↑o 𝐵 ) ∧ 𝐵 ∈ On ) ) )
55		oacl2g	⊢ ( ( ( ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ∧ ( ( ω ↑o 𝐵 ) = ∅ ∨ ( ( ω ↑o 𝐵 ) = ( ω ↑o 𝐵 ) ∧ 𝐵 ∈ On ) ) ) → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ ( ω ↑o 𝐵 ) )
56	47 48 54 55	syl21anc	⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ ( ω ↑o 𝐵 ) )
57	46 56	eqeltrd	⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o suc 𝑦 ) ∈ ( ω ↑o 𝐵 ) )
58	57	exp31	⊢ ( 𝑦 ∈ ω → ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) → ( 𝐴 ·o suc 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) ) )
59	58	a2d	⊢ ( 𝑦 ∈ ω → ( ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) → ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o suc 𝑦 ) ∈ ( ω ↑o 𝐵 ) ) ) )
60	23 26 29 32 41 59	finds	⊢ ( 𝑁 ∈ ω → ( ( ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ ( ω ↑o 𝐵 ) ) → ( 𝐴 ·o 𝑁 ) ∈ ( ω ↑o 𝐵 ) ) )
61	60	expdimp	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝐴 ∈ ( On ∖ 1o ) ∧ 𝐵 ∈ On ) ) → ( 𝐴 ∈ ( ω ↑o 𝐵 ) → ( 𝐴 ·o 𝑁 ) ∈ ( ω ↑o 𝐵 ) ) )
62	15 19 20 61	syl12anc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ∈ ( ω ↑o 𝐵 ) → ( 𝐴 ·o 𝑁 ) ∈ ( ω ↑o 𝐵 ) ) )
63		on0eqel	⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
64	16 63	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
65	14 62 64	mpjaodan	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω ) → ( 𝐴 ∈ ( ω ↑o 𝐵 ) → ( 𝐴 ·o 𝑁 ) ∈ ( ω ↑o 𝐵 ) ) )