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

Theorem oecan 6824
 Description: Left cancellation law for ordinal exponentiation. (Contributed by NM, 6-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
Assertion
Ref Expression
oecan

Proof of Theorem oecan
StepHypRef Expression
1 oeordi 6822 . . . . . . 7
21ancoms 440 . . . . . 6
323adant2 976 . . . . 5
4 oeordi 6822 . . . . . . 7
54ancoms 440 . . . . . 6
653adant3 977 . . . . 5
73, 6orim12d 812 . . . 4
87con3d 127 . . 3
9 eldifi 3461 . . . . . 6
1093ad2ant1 978 . . . . 5
11 simp2 958 . . . . 5
12 oecl 6773 . . . . 5
1310, 11, 12syl2anc 643 . . . 4
14 simp3 959 . . . . 5
15 oecl 6773 . . . . 5
1610, 14, 15syl2anc 643 . . . 4
17 eloni 4583 . . . . 5
18 eloni 4583 . . . . 5
19 ordtri3 4609 . . . . 5
2017, 18, 19syl2an 464 . . . 4
2113, 16, 20syl2anc 643 . . 3
22 eloni 4583 . . . . 5
23 eloni 4583 . . . . 5
24 ordtri3 4609 . . . . 5
2522, 23, 24syl2an 464 . . . 4