Metamath Proof Explorer

Theorem omge1

Description: Any nonzero ordinal product is greater-than-or-equal to the term on the left. Lemma 3.11 of Schloeder p. 8. See omword1 . (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion omge1 ⊢ A ∈ On ∧ B ∈ On ∧ B ≠ ∅ → A ⊆ A ⋅ 𝑜 B

Proof

Step Hyp Ref Expression
1 3simpa ⊢ A ∈ On ∧ B ∈ On ∧ B ≠ ∅ → A ∈ On ∧ B ∈ On
2 on0eln0 ⊢ B ∈ On → ∅ ∈ B ↔ B ≠ ∅
3 2 biimpar ⊢ B ∈ On ∧ B ≠ ∅ → ∅ ∈ B
4 3 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ B ≠ ∅ → ∅ ∈ B
5 omword1 ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ B → A ⊆ A ⋅ 𝑜 B
6 1 4 5 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ B ≠ ∅ → A ⊆ A ⋅ 𝑜 B