Metamath Proof Explorer

Theorem nnmwordri

Description: Weak ordering property of ordinal multiplication. Proposition 8.21 of TakeutiZaring p. 63, limited to natural numbers. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion nnmwordri ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⊆ B → A ⋅ 𝑜 C ⊆ B ⋅ 𝑜 C

Proof

Step Hyp Ref Expression
1 nnmwordi ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
2 nnmcom ⊢ A ∈ ω ∧ C ∈ ω → A ⋅ 𝑜 C = C ⋅ 𝑜 A
3 2 3adant2 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⋅ 𝑜 C = C ⋅ 𝑜 A
4 nnmcom ⊢ B ∈ ω ∧ C ∈ ω → B ⋅ 𝑜 C = C ⋅ 𝑜 B
5 4 3adant1 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → B ⋅ 𝑜 C = C ⋅ 𝑜 B
6 3 5 sseq12d ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⋅ 𝑜 C ⊆ B ⋅ 𝑜 C ↔ C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
7 1 6 sylibrd ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⊆ B → A ⋅ 𝑜 C ⊆ B ⋅ 𝑜 C