Metamath Proof Explorer

Theorem omord2lim

Description: Given a limit ordinal, the product of any nonzero ordinal with an ordinal less than that limit ordinal is less than the product of the nonzero 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