Metamath Proof Explorer

Theorem omword

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

Ref Expression
Assertion omword ⊢A∈On∧B∈On∧C∈On∧∅∈C→A⊆B↔C⋅𝑜A⊆C⋅𝑜B

Proof

Step Hyp Ref Expression
1 omord2 ⊢A∈On∧B∈On∧C∈On∧∅∈C→A∈B↔C⋅𝑜A∈C⋅𝑜B
2 3anrot ⊢C∈On∧A∈On∧B∈On↔A∈On∧B∈On∧C∈On
3 omcan ⊢C∈On∧A∈On∧B∈On∧∅∈C→C⋅𝑜A=C⋅𝑜B↔A=B
4 2 3 sylanbr ⊢A∈On∧B∈On∧C∈On∧∅∈C→C⋅𝑜A=C⋅𝑜B↔A=B
5 4 bicomd ⊢A∈On∧B∈On∧C∈On∧∅∈C→A=B↔C⋅𝑜A=C⋅𝑜B
6 1 5 orbi12d ⊢A∈On∧B∈On∧C∈On∧∅∈C→A∈B∨A=B↔C⋅𝑜A∈C⋅𝑜B∨C⋅𝑜A=C⋅𝑜B
7 onsseleq ⊢A∈On∧B∈On→A⊆B↔A∈B∨A=B
8 7 3adant3 ⊢A∈On∧B∈On∧C∈On→A⊆B↔A∈B∨A=B
9 8 adantr ⊢A∈On∧B∈On∧C∈On∧∅∈C→A⊆B↔A∈B∨A=B
10 omcl ⊢C∈On∧A∈On→C⋅𝑜A∈On
11 omcl ⊢C∈On∧B∈On→C⋅𝑜B∈On
12 10 11 anim12dan ⊢C∈On∧A∈On∧B∈On→C⋅𝑜A∈On∧C⋅𝑜B∈On
13 12 ancoms ⊢A∈On∧B∈On∧C∈On→C⋅𝑜A∈On∧C⋅𝑜B∈On
14 13 3impa ⊢A∈On∧B∈On∧C∈On→C⋅𝑜A∈On∧C⋅𝑜B∈On
15 onsseleq ⊢C⋅𝑜A∈On∧C⋅𝑜B∈On→C⋅𝑜A⊆C⋅𝑜B↔C⋅𝑜A∈C⋅𝑜B∨C⋅𝑜A=C⋅𝑜B
16 14 15 syl ⊢A∈On∧B∈On∧C∈On→C⋅𝑜A⊆C⋅𝑜B↔C⋅𝑜A∈C⋅𝑜B∨C⋅𝑜A=C⋅𝑜B
17 16 adantr ⊢A∈On∧B∈On∧C∈On∧∅∈C→C⋅𝑜A⊆C⋅𝑜B↔C⋅𝑜A∈C⋅𝑜B∨C⋅𝑜A=C⋅𝑜B
18 6 9 17 3bitr4d ⊢A∈On∧B∈On∧C∈On∧∅∈C→A⊆B↔C⋅𝑜A⊆C⋅𝑜B