Metamath Proof Explorer


Theorem omord2

Description: Ordering property of ordinal multiplication. (Contributed by NM, 25-Dec-2004)

Ref Expression
Assertion omord2 A On B On C On C A B C 𝑜 A C 𝑜 B

Proof

Step Hyp Ref Expression
1 omordi B On C On C A B C 𝑜 A C 𝑜 B
2 1 3adantl1 A On B On C On C A B C 𝑜 A C 𝑜 B
3 oveq2 A = B C 𝑜 A = C 𝑜 B
4 3 a1i A On B On C On C A = B C 𝑜 A = C 𝑜 B
5 omordi A On C On C B A C 𝑜 B C 𝑜 A
6 5 3adantl2 A On B On C On C B A C 𝑜 B C 𝑜 A
7 4 6 orim12d A On B On C On C A = B B A C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
8 7 con3d A On B On C On C ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A ¬ A = B B A
9 omcl C On A On C 𝑜 A On
10 omcl C On B On C 𝑜 B On
11 eloni C 𝑜 A On Ord C 𝑜 A
12 eloni C 𝑜 B On Ord C 𝑜 B
13 ordtri2 Ord C 𝑜 A Ord C 𝑜 B C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
14 11 12 13 syl2an C 𝑜 A On C 𝑜 B On C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
15 9 10 14 syl2an C On A On C On B On C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
16 15 anandis C On A On B On C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
17 16 ancoms A On B On C On C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
18 17 3impa A On B On C On C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
19 18 adantr A On B On C On C C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
20 eloni A On Ord A
21 eloni B On Ord B
22 ordtri2 Ord A Ord B A B ¬ A = B B A
23 20 21 22 syl2an A On B On A B ¬ A = B B A
24 23 3adant3 A On B On C On A B ¬ A = B B A
25 24 adantr A On B On C On C A B ¬ A = B B A
26 8 19 25 3imtr4d A On B On C On C C 𝑜 A C 𝑜 B A B
27 2 26 impbid A On B On C On C A B C 𝑜 A C 𝑜 B