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 ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → Lim ( 𝐵 ·o 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
2 1 ad2antrr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → Ord 𝐴 )
3 ne0i ⊢ ( ∅ ∈ 𝐴 → 𝐴 ≠ ∅ )
4 3 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → 𝐴 ≠ ∅ )
5 id ⊢ ( 𝐴 = ∪ 𝐴 → 𝐴 = ∪ 𝐴 )
6 df-lim ⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) )
7 6 biimpri ⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) → Lim 𝐴 )
8 2 4 5 7 syl2an3an ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = ∪ 𝐴 ) → Lim 𝐴 )
9 8 ex ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 = ∪ 𝐴 → Lim 𝐴 ) )
10 limelon ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On )
11 10 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ Lim 𝐴 ) → 𝐵 ∈ On )
12 simpll ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → 𝐴 ∈ On )
13 12 anim1i ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ Lim 𝐴 ) → ( 𝐴 ∈ On ∧ Lim 𝐴 ) )
14 0ellim ⊢ ( Lim 𝐵 → ∅ ∈ 𝐵 )
15 14 adantl ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ∅ ∈ 𝐵 )
16 15 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ Lim 𝐴 ) → ∅ ∈ 𝐵 )
17 omlimcl ⊢ ( ( ( 𝐵 ∈ On ∧ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) ∧ ∅ ∈ 𝐵 ) → Lim ( 𝐵 ·o 𝐴 ) )
18 11 13 16 17 syl21anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ Lim 𝐴 ) → Lim ( 𝐵 ·o 𝐴 ) )
19 18 ex ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( Lim 𝐴 → Lim ( 𝐵 ·o 𝐴 ) ) )
20 9 19 syld ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 = ∪ 𝐴 → Lim ( 𝐵 ·o 𝐴 ) ) )
21 onuni ⊢ ( 𝐴 ∈ On → ∪ 𝐴 ∈ On )
22 21 10 anim12ci ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐵 ∈ On ∧ ∪ 𝐴 ∈ On ) )
23 omcl ⊢ ( ( 𝐵 ∈ On ∧ ∪ 𝐴 ∈ On ) → ( 𝐵 ·o ∪ 𝐴 ) ∈ On )
24 22 23 syl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐵 ·o ∪ 𝐴 ) ∈ On )
25 simpr ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) )
26 24 25 jca ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( ( 𝐵 ·o ∪ 𝐴 ) ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) )
27 26 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = suc ∪ 𝐴 ) → ( ( 𝐵 ·o ∪ 𝐴 ) ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) )
28 oalimcl ⊢ ( ( ( 𝐵 ·o ∪ 𝐴 ) ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → Lim ( ( 𝐵 ·o ∪ 𝐴 ) +o 𝐵 ) )
29 27 28 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = suc ∪ 𝐴 ) → Lim ( ( 𝐵 ·o ∪ 𝐴 ) +o 𝐵 ) )
30 simpr ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = suc ∪ 𝐴 ) → 𝐴 = suc ∪ 𝐴 )
31 30 oveq2d ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = suc ∪ 𝐴 ) → ( 𝐵 ·o 𝐴 ) = ( 𝐵 ·o suc ∪ 𝐴 ) )
32 22 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = suc ∪ 𝐴 ) → ( 𝐵 ∈ On ∧ ∪ 𝐴 ∈ On ) )
33 omsuc ⊢ ( ( 𝐵 ∈ On ∧ ∪ 𝐴 ∈ On ) → ( 𝐵 ·o suc ∪ 𝐴 ) = ( ( 𝐵 ·o ∪ 𝐴 ) +o 𝐵 ) )
34 32 33 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = suc ∪ 𝐴 ) → ( 𝐵 ·o suc ∪ 𝐴 ) = ( ( 𝐵 ·o ∪ 𝐴 ) +o 𝐵 ) )
35 31 34 eqtrd ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = suc ∪ 𝐴 ) → ( 𝐵 ·o 𝐴 ) = ( ( 𝐵 ·o ∪ 𝐴 ) +o 𝐵 ) )
36 limeq ⊢ ( ( 𝐵 ·o 𝐴 ) = ( ( 𝐵 ·o ∪ 𝐴 ) +o 𝐵 ) → ( Lim ( 𝐵 ·o 𝐴 ) ↔ Lim ( ( 𝐵 ·o ∪ 𝐴 ) +o 𝐵 ) ) )
37 35 36 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = suc ∪ 𝐴 ) → ( Lim ( 𝐵 ·o 𝐴 ) ↔ Lim ( ( 𝐵 ·o ∪ 𝐴 ) +o 𝐵 ) ) )
38 29 37 mpbird ⊢ ( ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐴 = suc ∪ 𝐴 ) → Lim ( 𝐵 ·o 𝐴 ) )
39 38 ex ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 = suc ∪ 𝐴 → Lim ( 𝐵 ·o 𝐴 ) ) )
40 orduniorsuc ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 ) )
41 2 40 syl ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 ) )
42 20 39 41 mpjaod ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → Lim ( 𝐵 ·o 𝐴 ) )