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