Metamath Proof Explorer

Theorem omord2lim

Description: Given a limit ordinal, the product of any non-zero ordinal with an ordinal less than that limit ordinal is less than the product of the non-zero ordinal with the limit ordinal . Lemma 3.14 of Schloeder p. 9. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion omord2lim ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V→B∈C→A⋅𝑜B∈A⋅𝑜C

Proof

Step Hyp Ref Expression
1 limord ⊢Lim⁡C→Ord⁡C
2 1 ad2antrl ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V→Ord⁡C
3 ordelon ⊢Ord⁡C∧B∈C→B∈On
4 2 3 sylan ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V∧B∈C→B∈On
5 elex ⊢C∈V→C∈V
6 1 5 anim12i ⊢Lim⁡C∧C∈V→Ord⁡C∧C∈V
7 6 ad2antlr ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V∧B∈C→Ord⁡C∧C∈V
8 elon2 ⊢C∈On↔Ord⁡C∧C∈V
9 7 8 sylibr ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V∧B∈C→C∈On
10 simplll ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V∧B∈C→A∈On
11 simpr ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V∧B∈C→B∈C
12 on0eln0 ⊢A∈On→∅∈A↔A≠∅
13 12 biimpar ⊢A∈On∧A≠∅→∅∈A
14 13 ad2antrr ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V∧B∈C→∅∈A
15 omord ⊢B∈On∧C∈On∧A∈On→B∈C∧∅∈A↔A⋅𝑜B∈A⋅𝑜C
16 15 biimpa ⊢B∈On∧C∈On∧A∈On∧B∈C∧∅∈A→A⋅𝑜B∈A⋅𝑜C
17 4 9 10 11 14 16 syl32anc ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V∧B∈C→A⋅𝑜B∈A⋅𝑜C
18 17 ex ⊢A∈On∧A≠∅∧Lim⁡C∧C∈V→B∈C→A⋅𝑜B∈A⋅𝑜C