Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  oeord Unicode version

Theorem oeord 6472
 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.)
Assertion
Ref Expression
oeord

Proof of Theorem oeord
StepHypRef Expression
1 oeordi 6471 . . 3
3 oveq2 5718 . . . . . 6
43a1i 12 . . . . 5
5 oeordi 6471 . . . . . 6
653adant2 979 . . . . 5
74, 6orim12d 814 . . . 4
87con3d 127 . . 3
9 eldifi 3215 . . . . . 6
1093ad2ant3 983 . . . . 5
11 simp1 960 . . . . 5
12 oecl 6422 . . . . 5
1310, 11, 12syl2anc 645 . . . 4
14 simp2 961 . . . . 5
15 oecl 6422 . . . . 5
1610, 14, 15syl2anc 645 . . . 4
17 eloni 4295 . . . . 5
18 eloni 4295 . . . . 5
19 ordtri2 4320 . . . . 5
2017, 18, 19syl2an 465 . . . 4
2113, 16, 20syl2anc 645 . . 3
22 eloni 4295 . . . . 5
23 eloni 4295 . . . . 5
24 ordtri2 4320 . . . . 5
2522, 23, 24syl2an 465 . . . 4