Metamath Proof Explorer

Theorem nnmword

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

Ref Expression
Assertion nnmword ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→A⊆B↔C⋅𝑜A⊆C⋅𝑜B

Proof

Step Hyp Ref Expression
1 iba ⊢∅∈C→B∈A↔B∈A∧∅∈C
2 nnmord ⊢B∈ω∧A∈ω∧C∈ω→B∈A∧∅∈C↔C⋅𝑜B∈C⋅𝑜A
3 2 3com12 ⊢A∈ω∧B∈ω∧C∈ω→B∈A∧∅∈C↔C⋅𝑜B∈C⋅𝑜A
4 1 3 sylan9bbr ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→B∈A↔C⋅𝑜B∈C⋅𝑜A
5 4 notbid ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→¬B∈A↔¬C⋅𝑜B∈C⋅𝑜A
6 simpl1 ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→A∈ω
7 nnon ⊢A∈ω→A∈On
8 6 7 syl ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→A∈On
9 simpl2 ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→B∈ω
10 nnon ⊢B∈ω→B∈On
11 9 10 syl ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→B∈On
12 ontri1 ⊢A∈On∧B∈On→A⊆B↔¬B∈A
13 8 11 12 syl2anc ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→A⊆B↔¬B∈A
14 simpl3 ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→C∈ω
15 nnmcl ⊢C∈ω∧A∈ω→C⋅𝑜A∈ω
16 14 6 15 syl2anc ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→C⋅𝑜A∈ω
17 nnon ⊢C⋅𝑜A∈ω→C⋅𝑜A∈On
18 16 17 syl ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→C⋅𝑜A∈On
19 nnmcl ⊢C∈ω∧B∈ω→C⋅𝑜B∈ω
20 14 9 19 syl2anc ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→C⋅𝑜B∈ω
21 nnon ⊢C⋅𝑜B∈ω→C⋅𝑜B∈On
22 20 21 syl ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→C⋅𝑜B∈On
23 ontri1 ⊢C⋅𝑜A∈On∧C⋅𝑜B∈On→C⋅𝑜A⊆C⋅𝑜B↔¬C⋅𝑜B∈C⋅𝑜A
24 18 22 23 syl2anc ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→C⋅𝑜A⊆C⋅𝑜B↔¬C⋅𝑜B∈C⋅𝑜A
25 5 13 24 3bitr4d ⊢A∈ω∧B∈ω∧C∈ω∧∅∈C→A⊆B↔C⋅𝑜A⊆C⋅𝑜B