Metamath Proof Explorer


Theorem oeord

Description: Ordering property of ordinal exponentiation. Corollary 8.34 of TakeutiZaring p. 68 and its converse. (Contributed by NM, 6-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oeord A On B On C On 2 𝑜 A B C 𝑜 A C 𝑜 B

Proof

Step Hyp Ref Expression
1 oeordi B On C On 2 𝑜 A B C 𝑜 A C 𝑜 B
2 1 3adant1 A On B On C On 2 𝑜 A B C 𝑜 A C 𝑜 B
3 oveq2 A = B C 𝑜 A = C 𝑜 B
4 3 a1i A On B On C On 2 𝑜 A = B C 𝑜 A = C 𝑜 B
5 oeordi A On C On 2 𝑜 B A C 𝑜 B C 𝑜 A
6 5 3adant2 A On B On C On 2 𝑜 B A C 𝑜 B C 𝑜 A
7 4 6 orim12d A On B On C On 2 𝑜 A = B B A C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
8 7 con3d A On B On C On 2 𝑜 ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A ¬ A = B B A
9 eldifi C On 2 𝑜 C On
10 9 3ad2ant3 A On B On C On 2 𝑜 C On
11 simp1 A On B On C On 2 𝑜 A On
12 oecl C On A On C 𝑜 A On
13 10 11 12 syl2anc A On B On C On 2 𝑜 C 𝑜 A On
14 simp2 A On B On C On 2 𝑜 B On
15 oecl C On B On C 𝑜 B On
16 10 14 15 syl2anc A On B On C On 2 𝑜 C 𝑜 B On
17 eloni C 𝑜 A On Ord C 𝑜 A
18 eloni C 𝑜 B On Ord C 𝑜 B
19 ordtri2 Ord C 𝑜 A Ord C 𝑜 B C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
20 17 18 19 syl2an C 𝑜 A On C 𝑜 B On C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
21 13 16 20 syl2anc A On B On C On 2 𝑜 C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
22 eloni A On Ord A
23 eloni B On Ord B
24 ordtri2 Ord A Ord B A B ¬ A = B B A
25 22 23 24 syl2an A On B On A B ¬ A = B B A
26 25 3adant3 A On B On C On 2 𝑜 A B ¬ A = B B A
27 8 21 26 3imtr4d A On B On C On 2 𝑜 C 𝑜 A C 𝑜 B A B
28 2 27 impbid A On B On C On 2 𝑜 A B C 𝑜 A C 𝑜 B