Metamath Proof Explorer


Theorem omord

Description: Ordering property of ordinal multiplication. Proposition 8.19 of TakeutiZaring p. 63. (Contributed by NM, 14-Dec-2004)

Ref Expression
Assertion omord A On B On C On A B C 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 1 ex A On B On C On C A B C 𝑜 A C 𝑜 B
3 2 pm5.32rd A On B On C On A B C C 𝑜 A C 𝑜 B C
4 simpl C 𝑜 A C 𝑜 B C C 𝑜 A C 𝑜 B
5 ne0i C 𝑜 A C 𝑜 B C 𝑜 B
6 om0r B On 𝑜 B =
7 oveq1 C = C 𝑜 B = 𝑜 B
8 7 eqeq1d C = C 𝑜 B = 𝑜 B =
9 6 8 syl5ibrcom B On C = C 𝑜 B =
10 9 necon3d B On C 𝑜 B C
11 5 10 syl5 B On C 𝑜 A C 𝑜 B C
12 11 adantr B On C On C 𝑜 A C 𝑜 B C
13 on0eln0 C On C C
14 13 adantl B On C On C C
15 12 14 sylibrd B On C On C 𝑜 A C 𝑜 B C
16 15 3adant1 A On B On C On C 𝑜 A C 𝑜 B C
17 16 ancld A On B On C On C 𝑜 A C 𝑜 B C 𝑜 A C 𝑜 B C
18 4 17 impbid2 A On B On C On C 𝑜 A C 𝑜 B C C 𝑜 A C 𝑜 B
19 3 18 bitrd A On B On C On A B C C 𝑜 A C 𝑜 B