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