Metamath Proof Explorer

Theorem omge2

Description: Any nonzero ordinal product is greater-than-or-equal to the term on the right. Lemma 3.12 of Schloeder p. 9. See omword2 . (Contributed by RP, 29-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 ancom ⊢ A ∈ On ∧ B ∈ On ↔ B ∈ On ∧ A ∈ On
2 1 anbi1i ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ↔ B ∈ On ∧ A ∈ On ∧ A ≠ ∅
3 df-3an ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ↔ A ∈ On ∧ B ∈ On ∧ A ≠ ∅
4 on0eln0 ⊢ A ∈ On → ∅ ∈ A ↔ A ≠ ∅
5 4 adantl ⊢ B ∈ On ∧ A ∈ On → ∅ ∈ A ↔ A ≠ ∅
6 5 pm5.32i ⊢ B ∈ On ∧ A ∈ On ∧ ∅ ∈ A ↔ B ∈ On ∧ A ∈ On ∧ A ≠ ∅
7 2 3 6 3bitr4i ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ ↔ B ∈ On ∧ A ∈ On ∧ ∅ ∈ A
8 omword2 ⊢ B ∈ On ∧ A ∈ On ∧ ∅ ∈ A → B ⊆ A ⋅ 𝑜 B
9 7 8 sylbi ⊢ A ∈ On ∧ B ∈ On ∧ A ≠ ∅ → B ⊆ A ⋅ 𝑜 B