Metamath Proof Explorer

Theorem omwordi

Description: Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004)

Ref Expression
Assertion omwordi ⊢A∈On∧B∈On∧C∈On→A⊆B→C⋅𝑜A⊆C⋅𝑜B

Proof

Step Hyp Ref Expression
1 omword ⊢A∈On∧B∈On∧C∈On∧∅∈C→A⊆B↔C⋅𝑜A⊆C⋅𝑜B
2 1 biimpd ⊢A∈On∧B∈On∧C∈On∧∅∈C→A⊆B→C⋅𝑜A⊆C⋅𝑜B
3 2 ex ⊢A∈On∧B∈On∧C∈On→∅∈C→A⊆B→C⋅𝑜A⊆C⋅𝑜B
4 eloni ⊢C∈On→Ord⁡C
5 ord0eln0 ⊢Ord⁡C→∅∈C↔C≠∅
6 5 necon2bbid ⊢Ord⁡C→C=∅↔¬∅∈C
7 4 6 syl ⊢C∈On→C=∅↔¬∅∈C
8 7 3ad2ant3 ⊢A∈On∧B∈On∧C∈On→C=∅↔¬∅∈C
9 ssid ⊢∅⊆∅
10 om0r ⊢A∈On→∅⋅𝑜A=∅
11 10 adantr ⊢A∈On∧B∈On→∅⋅𝑜A=∅
12 om0r ⊢B∈On→∅⋅𝑜B=∅
13 12 adantl ⊢A∈On∧B∈On→∅⋅𝑜B=∅
14 11 13 sseq12d ⊢A∈On∧B∈On→∅⋅𝑜A⊆∅⋅𝑜B↔∅⊆∅
15 9 14 mpbiri ⊢A∈On∧B∈On→∅⋅𝑜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∈On∧B∈On→C=∅→C⋅𝑜A⊆C⋅𝑜B
20 19 3adant3 ⊢A∈On∧B∈On∧C∈On→C=∅→C⋅𝑜A⊆C⋅𝑜B
21 8 20 sylbird ⊢A∈On∧B∈On∧C∈On→¬∅∈C→C⋅𝑜A⊆C⋅𝑜B
22 21 a1dd ⊢A∈On∧B∈On∧C∈On→¬∅∈C→A⊆B→C⋅𝑜A⊆C⋅𝑜B
23 3 22 pm2.61d ⊢A∈On∧B∈On∧C∈On→A⊆B→C⋅𝑜A⊆C⋅𝑜B