Metamath Proof Explorer

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 𝐵 ) ) )