Metamath Proof Explorer

Theorem omord2i

Description: Ordinal multiplication of the same non-zero number on the left preserves the ordering of the numbers on the right. Lemma 3.15 of Schloeder p. 9. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion omord2i ⊢ A ∈ On ∧ A ≠ ∅ ∧ C ∈ On → B ∈ C → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 C

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ On ∧ A ≠ ∅ → A ∈ On
2 1 anim1ci ⊢ A ∈ On ∧ A ≠ ∅ ∧ C ∈ On → C ∈ On ∧ A ∈ On
3 on0eln0 ⊢ A ∈ On → ∅ ∈ A ↔ A ≠ ∅
4 3 biimpar ⊢ A ∈ On ∧ A ≠ ∅ → ∅ ∈ A
5 4 adantr ⊢ A ∈ On ∧ A ≠ ∅ ∧ C ∈ On → ∅ ∈ A
6 omordi ⊢ C ∈ On ∧ A ∈ On ∧ ∅ ∈ A → B ∈ C → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 C
7 2 5 6 syl2anc ⊢ A ∈ On ∧ A ≠ ∅ ∧ C ∈ On → B ∈ C → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 C