Metamath Proof Explorer


Theorem oeoe

Description: Product of exponents law for ordinal exponentiation. Theorem 8S of Enderton p. 238. Also Proposition 8.42 of TakeutiZaring p. 70. (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Assertion oeoe AOnBOnCOnA𝑜B𝑜C=A𝑜B𝑜C

Proof

Step Hyp Ref Expression
1 oveq2 B=𝑜B=𝑜
2 oe0m0 𝑜=1𝑜
3 1 2 eqtrdi B=𝑜B=1𝑜
4 3 oveq1d B=𝑜B𝑜C=1𝑜𝑜C
5 oe1m COn1𝑜𝑜C=1𝑜
6 4 5 sylan9eqr COnB=𝑜B𝑜C=1𝑜
7 6 adantll BOnCOnB=𝑜B𝑜C=1𝑜
8 oveq2 C=𝑜B𝑜C=𝑜B𝑜
9 0elon On
10 oecl OnBOn𝑜BOn
11 9 10 mpan BOn𝑜BOn
12 oe0 𝑜BOn𝑜B𝑜=1𝑜
13 11 12 syl BOn𝑜B𝑜=1𝑜
14 8 13 sylan9eqr BOnC=𝑜B𝑜C=1𝑜
15 14 adantlr BOnCOnC=𝑜B𝑜C=1𝑜
16 7 15 jaodan BOnCOnB=C=𝑜B𝑜C=1𝑜
17 om00 BOnCOnB𝑜C=B=C=
18 17 biimpar BOnCOnB=C=B𝑜C=
19 18 oveq2d BOnCOnB=C=𝑜B𝑜C=𝑜
20 19 2 eqtrdi BOnCOnB=C=𝑜B𝑜C=1𝑜
21 16 20 eqtr4d BOnCOnB=C=𝑜B𝑜C=𝑜B𝑜C
22 on0eln0 BOnBB
23 on0eln0 COnCC
24 22 23 bi2anan9 BOnCOnBCBC
25 neanior BC¬B=C=
26 24 25 bitrdi BOnCOnBC¬B=C=
27 oe0m1 BOnB𝑜B=
28 27 biimpa BOnB𝑜B=
29 28 oveq1d BOnB𝑜B𝑜C=𝑜C
30 oe0m1 COnC𝑜C=
31 30 biimpa COnC𝑜C=
32 29 31 sylan9eq BOnBCOnC𝑜B𝑜C=
33 32 an4s BOnCOnBC𝑜B𝑜C=
34 om00el BOnCOnB𝑜CBC
35 omcl BOnCOnB𝑜COn
36 oe0m1 B𝑜COnB𝑜C𝑜B𝑜C=
37 35 36 syl BOnCOnB𝑜C𝑜B𝑜C=
38 34 37 bitr3d BOnCOnBC𝑜B𝑜C=
39 38 biimpa BOnCOnBC𝑜B𝑜C=
40 33 39 eqtr4d BOnCOnBC𝑜B𝑜C=𝑜B𝑜C
41 40 ex BOnCOnBC𝑜B𝑜C=𝑜B𝑜C
42 26 41 sylbird BOnCOn¬B=C=𝑜B𝑜C=𝑜B𝑜C
43 42 imp BOnCOn¬B=C=𝑜B𝑜C=𝑜B𝑜C
44 21 43 pm2.61dan BOnCOn𝑜B𝑜C=𝑜B𝑜C
45 oveq1 A=A𝑜B=𝑜B
46 45 oveq1d A=A𝑜B𝑜C=𝑜B𝑜C
47 oveq1 A=A𝑜B𝑜C=𝑜B𝑜C
48 46 47 eqeq12d A=A𝑜B𝑜C=A𝑜B𝑜C𝑜B𝑜C=𝑜B𝑜C
49 44 48 syl5ibr A=BOnCOnA𝑜B𝑜C=A𝑜B𝑜C
50 49 impcom BOnCOnA=A𝑜B𝑜C=A𝑜B𝑜C
51 oveq1 A=ifAOnAA1𝑜A𝑜B=ifAOnAA1𝑜𝑜B
52 51 oveq1d A=ifAOnAA1𝑜A𝑜B𝑜C=ifAOnAA1𝑜𝑜B𝑜C
53 oveq1 A=ifAOnAA1𝑜A𝑜B𝑜C=ifAOnAA1𝑜𝑜B𝑜C
54 52 53 eqeq12d A=ifAOnAA1𝑜A𝑜B𝑜C=A𝑜B𝑜CifAOnAA1𝑜𝑜B𝑜C=ifAOnAA1𝑜𝑜B𝑜C
55 54 imbi2d A=ifAOnAA1𝑜BOnCOnA𝑜B𝑜C=A𝑜B𝑜CBOnCOnifAOnAA1𝑜𝑜B𝑜C=ifAOnAA1𝑜𝑜B𝑜C
56 eleq1 A=ifAOnAA1𝑜AOnifAOnAA1𝑜On
57 eleq2 A=ifAOnAA1𝑜AifAOnAA1𝑜
58 56 57 anbi12d A=ifAOnAA1𝑜AOnAifAOnAA1𝑜OnifAOnAA1𝑜
59 eleq1 1𝑜=ifAOnAA1𝑜1𝑜OnifAOnAA1𝑜On
60 eleq2 1𝑜=ifAOnAA1𝑜1𝑜ifAOnAA1𝑜
61 59 60 anbi12d 1𝑜=ifAOnAA1𝑜1𝑜On1𝑜ifAOnAA1𝑜OnifAOnAA1𝑜
62 1on 1𝑜On
63 0lt1o 1𝑜
64 62 63 pm3.2i 1𝑜On1𝑜
65 58 61 64 elimhyp ifAOnAA1𝑜OnifAOnAA1𝑜
66 65 simpli ifAOnAA1𝑜On
67 65 simpri ifAOnAA1𝑜
68 66 67 oeoelem BOnCOnifAOnAA1𝑜𝑜B𝑜C=ifAOnAA1𝑜𝑜B𝑜C
69 55 68 dedth AOnABOnCOnA𝑜B𝑜C=A𝑜B𝑜C
70 69 imp AOnABOnCOnA𝑜B𝑜C=A𝑜B𝑜C
71 70 an32s AOnBOnCOnAA𝑜B𝑜C=A𝑜B𝑜C
72 50 71 oe0lem AOnBOnCOnA𝑜B𝑜C=A𝑜B𝑜C
73 72 3impb AOnBOnCOnA𝑜B𝑜C=A𝑜B𝑜C