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