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 
|- ( ( A e. On /\ B e. On /\ N e. _om ) -> ( A e. ( _om ^o B ) -> ( A .o N ) e. ( _om ^o B ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = (/) -> ( A .o N ) = ( (/) .o N ) )
2 simp3 
 |-  ( ( A e. On /\ B e. On /\ N e. _om ) -> N e. _om )
3 nnon 
 |-  ( N e. _om -> N e. On )
4 om0r 
 |-  ( N e. On -> ( (/) .o N ) = (/) )
5 2 3 4 3syl 
 |-  ( ( A e. On /\ B e. On /\ N e. _om ) -> ( (/) .o N ) = (/) )
6 1 5 sylan9eqr 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ A = (/) ) -> ( A .o N ) = (/) )
7 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ A = (/) ) -> B e. On )
8 omelon 
 |-  _om e. On
9 7 8 jctil 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ A = (/) ) -> ( _om e. On /\ B e. On ) )
10 peano1 
 |-  (/) e. _om
11 oen0 
 |-  ( ( ( _om e. On /\ B e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o B ) )
12 9 10 11 sylancl 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ A = (/) ) -> (/) e. ( _om ^o B ) )
13 6 12 eqeltrd 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ A = (/) ) -> ( A .o N ) e. ( _om ^o B ) )
14 13 a1d 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ A = (/) ) -> ( A e. ( _om ^o B ) -> ( A .o N ) e. ( _om ^o B ) ) )
15 2 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ (/) e. A ) -> N e. _om )
16 simp1 
 |-  ( ( A e. On /\ B e. On /\ N e. _om ) -> A e. On )
17 16 anim1i 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ (/) e. A ) -> ( A e. On /\ (/) e. A ) )
18 ondif1 
 |-  ( A e. ( On \ 1o ) <-> ( A e. On /\ (/) e. A ) )
19 17 18 sylibr 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ (/) e. A ) -> A e. ( On \ 1o ) )
20 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ (/) e. A ) -> B e. On )
21 oveq2 
 |-  ( x = (/) -> ( A .o x ) = ( A .o (/) ) )
22 21 eleq1d 
 |-  ( x = (/) -> ( ( A .o x ) e. ( _om ^o B ) <-> ( A .o (/) ) e. ( _om ^o B ) ) )
23 22 imbi2d 
 |-  ( x = (/) -> ( ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o x ) e. ( _om ^o B ) ) <-> ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o (/) ) e. ( _om ^o B ) ) ) )
24 oveq2 
 |-  ( x = y -> ( A .o x ) = ( A .o y ) )
25 24 eleq1d 
 |-  ( x = y -> ( ( A .o x ) e. ( _om ^o B ) <-> ( A .o y ) e. ( _om ^o B ) ) )
26 25 imbi2d 
 |-  ( x = y -> ( ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o x ) e. ( _om ^o B ) ) <-> ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o y ) e. ( _om ^o B ) ) ) )
27 oveq2 
 |-  ( x = suc y -> ( A .o x ) = ( A .o suc y ) )
28 27 eleq1d 
 |-  ( x = suc y -> ( ( A .o x ) e. ( _om ^o B ) <-> ( A .o suc y ) e. ( _om ^o B ) ) )
29 28 imbi2d 
 |-  ( x = suc y -> ( ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o x ) e. ( _om ^o B ) ) <-> ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o suc y ) e. ( _om ^o B ) ) ) )
30 oveq2 
 |-  ( x = N -> ( A .o x ) = ( A .o N ) )
31 30 eleq1d 
 |-  ( x = N -> ( ( A .o x ) e. ( _om ^o B ) <-> ( A .o N ) e. ( _om ^o B ) ) )
32 31 imbi2d 
 |-  ( x = N -> ( ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o x ) e. ( _om ^o B ) ) <-> ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o N ) e. ( _om ^o B ) ) ) )
33 eldifi 
 |-  ( A e. ( On \ 1o ) -> A e. On )
34 om0 
 |-  ( A e. On -> ( A .o (/) ) = (/) )
35 33 34 syl 
 |-  ( A e. ( On \ 1o ) -> ( A .o (/) ) = (/) )
36 35 adantr 
 |-  ( ( A e. ( On \ 1o ) /\ B e. On ) -> ( A .o (/) ) = (/) )
37 8 jctl 
 |-  ( B e. On -> ( _om e. On /\ B e. On ) )
38 37 10 11 sylancl 
 |-  ( B e. On -> (/) e. ( _om ^o B ) )
39 38 adantl 
 |-  ( ( A e. ( On \ 1o ) /\ B e. On ) -> (/) e. ( _om ^o B ) )
40 36 39 eqeltrd 
 |-  ( ( A e. ( On \ 1o ) /\ B e. On ) -> ( A .o (/) ) e. ( _om ^o B ) )
41 40 adantr 
 |-  ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o (/) ) e. ( _om ^o B ) )
42 33 adantr 
 |-  ( ( A e. ( On \ 1o ) /\ B e. On ) -> A e. On )
43 42 ad2antrl 
 |-  ( ( y e. _om /\ ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) ) -> A e. On )
44 simpll 
 |-  ( ( ( y e. _om /\ ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) ) /\ ( A .o y ) e. ( _om ^o B ) ) -> y e. _om )
45 onmsuc 
 |-  ( ( A e. On /\ y e. _om ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
46 43 44 45 syl2an2r 
 |-  ( ( ( y e. _om /\ ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) ) /\ ( A .o y ) e. ( _om ^o B ) ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
47 simpr 
 |-  ( ( ( y e. _om /\ ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) ) /\ ( A .o y ) e. ( _om ^o B ) ) -> ( A .o y ) e. ( _om ^o B ) )
48 simplrr 
 |-  ( ( ( y e. _om /\ ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) ) /\ ( A .o y ) e. ( _om ^o B ) ) -> A e. ( _om ^o B ) )
49 eqid 
 |-  ( _om ^o B ) = ( _om ^o B )
50 49 jctl 
 |-  ( B e. On -> ( ( _om ^o B ) = ( _om ^o B ) /\ B e. On ) )
51 50 olcd 
 |-  ( B e. On -> ( ( _om ^o B ) = (/) \/ ( ( _om ^o B ) = ( _om ^o B ) /\ B e. On ) ) )
52 51 adantl 
 |-  ( ( A e. ( On \ 1o ) /\ B e. On ) -> ( ( _om ^o B ) = (/) \/ ( ( _om ^o B ) = ( _om ^o B ) /\ B e. On ) ) )
53 52 ad2antrl 
 |-  ( ( y e. _om /\ ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) ) -> ( ( _om ^o B ) = (/) \/ ( ( _om ^o B ) = ( _om ^o B ) /\ B e. On ) ) )
54 53 adantr 
 |-  ( ( ( y e. _om /\ ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) ) /\ ( A .o y ) e. ( _om ^o B ) ) -> ( ( _om ^o B ) = (/) \/ ( ( _om ^o B ) = ( _om ^o B ) /\ B e. On ) ) )
55 oacl2g 
 |-  ( ( ( ( A .o y ) e. ( _om ^o B ) /\ A e. ( _om ^o B ) ) /\ ( ( _om ^o B ) = (/) \/ ( ( _om ^o B ) = ( _om ^o B ) /\ B e. On ) ) ) -> ( ( A .o y ) +o A ) e. ( _om ^o B ) )
56 47 48 54 55 syl21anc 
 |-  ( ( ( y e. _om /\ ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) ) /\ ( A .o y ) e. ( _om ^o B ) ) -> ( ( A .o y ) +o A ) e. ( _om ^o B ) )
57 46 56 eqeltrd 
 |-  ( ( ( y e. _om /\ ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) ) /\ ( A .o y ) e. ( _om ^o B ) ) -> ( A .o suc y ) e. ( _om ^o B ) )
58 57 exp31 
 |-  ( y e. _om -> ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( ( A .o y ) e. ( _om ^o B ) -> ( A .o suc y ) e. ( _om ^o B ) ) ) )
59 58 a2d 
 |-  ( y e. _om -> ( ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o y ) e. ( _om ^o B ) ) -> ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o suc y ) e. ( _om ^o B ) ) ) )
60 23 26 29 32 41 59 finds 
 |-  ( N e. _om -> ( ( ( A e. ( On \ 1o ) /\ B e. On ) /\ A e. ( _om ^o B ) ) -> ( A .o N ) e. ( _om ^o B ) ) )
61 60 expdimp 
 |-  ( ( N e. _om /\ ( A e. ( On \ 1o ) /\ B e. On ) ) -> ( A e. ( _om ^o B ) -> ( A .o N ) e. ( _om ^o B ) ) )
62 15 19 20 61 syl12anc 
 |-  ( ( ( A e. On /\ B e. On /\ N e. _om ) /\ (/) e. A ) -> ( A e. ( _om ^o B ) -> ( A .o N ) e. ( _om ^o B ) ) )
63 on0eqel 
 |-  ( A e. On -> ( A = (/) \/ (/) e. A ) )
64 16 63 syl 
 |-  ( ( A e. On /\ B e. On /\ N e. _om ) -> ( A = (/) \/ (/) e. A ) )
65 14 62 64 mpjaodan 
 |-  ( ( A e. On /\ B e. On /\ N e. _om ) -> ( A e. ( _om ^o B ) -> ( A .o N ) e. ( _om ^o B ) ) )