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