Metamath Proof Explorer


Theorem oeword

Description: Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oeword AOnBOnCOn2𝑜ABC𝑜AC𝑜B

Proof

Step Hyp Ref Expression
1 oeord AOnBOnCOn2𝑜ABC𝑜AC𝑜B
2 oecan COn2𝑜AOnBOnC𝑜A=C𝑜BA=B
3 2 3coml AOnBOnCOn2𝑜C𝑜A=C𝑜BA=B
4 3 bicomd AOnBOnCOn2𝑜A=BC𝑜A=C𝑜B
5 1 4 orbi12d AOnBOnCOn2𝑜ABA=BC𝑜AC𝑜BC𝑜A=C𝑜B
6 onsseleq AOnBOnABABA=B
7 6 3adant3 AOnBOnCOn2𝑜ABABA=B
8 eldifi COn2𝑜COn
9 id AOnBOnAOnBOn
10 oecl COnAOnC𝑜AOn
11 oecl COnBOnC𝑜BOn
12 10 11 anim12dan COnAOnBOnC𝑜AOnC𝑜BOn
13 onsseleq C𝑜AOnC𝑜BOnC𝑜AC𝑜BC𝑜AC𝑜BC𝑜A=C𝑜B
14 12 13 syl COnAOnBOnC𝑜AC𝑜BC𝑜AC𝑜BC𝑜A=C𝑜B
15 8 9 14 syl2anr AOnBOnCOn2𝑜C𝑜AC𝑜BC𝑜AC𝑜BC𝑜A=C𝑜B
16 15 3impa AOnBOnCOn2𝑜C𝑜AC𝑜BC𝑜AC𝑜BC𝑜A=C𝑜B
17 5 7 16 3bitr4d AOnBOnCOn2𝑜ABC𝑜AC𝑜B