Metamath Proof Explorer

Theorem omlimcl2

Description: The product of a limit ordinal with any nonzero ordinal is a limit ordinal. (Contributed by RP, 8-Jan-2025)

Ref Expression
Assertion omlimcl2 
|- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Lim ( B .o A ) )

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( A e. On -> Ord A )
2 1 ad2antrr 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Ord A )
3 ne0i 
 |-  ( (/) e. A -> A =/= (/) )
4 3 adantl 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> A =/= (/) )
5 id 
 |-  ( A = U. A -> A = U. A )
6 df-lim 
 |-  ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
7 6 biimpri 
 |-  ( ( Ord A /\ A =/= (/) /\ A = U. A ) -> Lim A )
8 2 4 5 7 syl2an3an 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = U. A ) -> Lim A )
9 8 ex 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A = U. A -> Lim A ) )
10 limelon 
 |-  ( ( B e. C /\ Lim B ) -> B e. On )
11 10 ad3antlr 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ Lim A ) -> B e. On )
12 simpll 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> A e. On )
13 12 anim1i 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ Lim A ) -> ( A e. On /\ Lim A ) )
14 0ellim 
 |-  ( Lim B -> (/) e. B )
15 14 adantl 
 |-  ( ( B e. C /\ Lim B ) -> (/) e. B )
16 15 ad3antlr 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ Lim A ) -> (/) e. B )
17 omlimcl 
 |-  ( ( ( B e. On /\ ( A e. On /\ Lim A ) ) /\ (/) e. B ) -> Lim ( B .o A ) )
18 11 13 16 17 syl21anc 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ Lim A ) -> Lim ( B .o A ) )
19 18 ex 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( Lim A -> Lim ( B .o A ) ) )
20 9 19 syld 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A = U. A -> Lim ( B .o A ) ) )
21 onuni 
 |-  ( A e. On -> U. A e. On )
22 21 10 anim12ci 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( B e. On /\ U. A e. On ) )
23 omcl 
 |-  ( ( B e. On /\ U. A e. On ) -> ( B .o U. A ) e. On )
24 22 23 syl 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( B .o U. A ) e. On )
25 simpr 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( B e. C /\ Lim B ) )
26 24 25 jca 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( ( B .o U. A ) e. On /\ ( B e. C /\ Lim B ) ) )
27 26 ad2antrr 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = suc U. A ) -> ( ( B .o U. A ) e. On /\ ( B e. C /\ Lim B ) ) )
28 oalimcl 
 |-  ( ( ( B .o U. A ) e. On /\ ( B e. C /\ Lim B ) ) -> Lim ( ( B .o U. A ) +o B ) )
29 27 28 syl 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = suc U. A ) -> Lim ( ( B .o U. A ) +o B ) )
30 simpr 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = suc U. A ) -> A = suc U. A )
31 30 oveq2d 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = suc U. A ) -> ( B .o A ) = ( B .o suc U. A ) )
32 22 ad2antrr 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = suc U. A ) -> ( B e. On /\ U. A e. On ) )
33 omsuc 
 |-  ( ( B e. On /\ U. A e. On ) -> ( B .o suc U. A ) = ( ( B .o U. A ) +o B ) )
34 32 33 syl 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = suc U. A ) -> ( B .o suc U. A ) = ( ( B .o U. A ) +o B ) )
35 31 34 eqtrd 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = suc U. A ) -> ( B .o A ) = ( ( B .o U. A ) +o B ) )
36 limeq 
 |-  ( ( B .o A ) = ( ( B .o U. A ) +o B ) -> ( Lim ( B .o A ) <-> Lim ( ( B .o U. A ) +o B ) ) )
37 35 36 syl 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = suc U. A ) -> ( Lim ( B .o A ) <-> Lim ( ( B .o U. A ) +o B ) ) )
38 29 37 mpbird 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ A = suc U. A ) -> Lim ( B .o A ) )
39 38 ex 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A = suc U. A -> Lim ( B .o A ) ) )
40 orduniorsuc 
 |-  ( Ord A -> ( A = U. A \/ A = suc U. A ) )
41 2 40 syl 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A = U. A \/ A = suc U. A ) )
42 20 39 41 mpjaod 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Lim ( B .o A ) )