Metamath Proof Explorer

Theorem nnmwordi

Description: Weak ordering property of multiplication. (Contributed by Mario Carneiro, 17-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 nnmword ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → A ⊆ B ↔ C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
2 1 biimpd ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
3 2 ex ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → ∅ ∈ C → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
4 nnord ⊢ C ∈ ω → Ord ⁡ C
5 ord0eln0 ⊢ Ord ⁡ C → ∅ ∈ C ↔ C ≠ ∅
6 5 necon2bbid ⊢ Ord ⁡ C → C = ∅ ↔ ¬ ∅ ∈ C
7 4 6 syl ⊢ C ∈ ω → C = ∅ ↔ ¬ ∅ ∈ C
8 7 3ad2ant3 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → C = ∅ ↔ ¬ ∅ ∈ C
9 ssid ⊢ ∅ ⊆ ∅
10 nnm0r ⊢ A ∈ ω → ∅ ⋅ 𝑜 A = ∅
11 10 adantr ⊢ A ∈ ω ∧ B ∈ ω → ∅ ⋅ 𝑜 A = ∅
12 nnm0r ⊢ B ∈ ω → ∅ ⋅ 𝑜 B = ∅
13 12 adantl ⊢ A ∈ ω ∧ B ∈ ω → ∅ ⋅ 𝑜 B = ∅
14 11 13 sseq12d ⊢ A ∈ ω ∧ B ∈ ω → ∅ ⋅ 𝑜 A ⊆ ∅ ⋅ 𝑜 B ↔ ∅ ⊆ ∅
15 9 14 mpbiri ⊢ A ∈ ω ∧ B ∈ ω → ∅ ⋅ 𝑜 A ⊆ ∅ ⋅ 𝑜 B
16 oveq1 ⊢ C = ∅ → C ⋅ 𝑜 A = ∅ ⋅ 𝑜 A
17 oveq1 ⊢ C = ∅ → C ⋅ 𝑜 B = ∅ ⋅ 𝑜 B
18 16 17 sseq12d ⊢ C = ∅ → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B ↔ ∅ ⋅ 𝑜 A ⊆ ∅ ⋅ 𝑜 B
19 15 18 syl5ibrcom ⊢ A ∈ ω ∧ B ∈ ω → C = ∅ → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
20 19 3adant3 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → C = ∅ → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
21 8 20 sylbird ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → ¬ ∅ ∈ C → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
22 21 a1dd ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → ¬ ∅ ∈ C → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
23 3 22 pm2.61d ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B