Metamath Proof Explorer

Theorem oeoa

Description: Sum of exponents law for ordinal exponentiation. Theorem 8R of Enderton p. 238. Also Proposition 8.41 of TakeutiZaring p. 69. Theorem 4.7 of Schloeder p. 14. (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Assertion oeoa ⊢A∈On∧B∈On∧C∈On→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C

Proof

Step Hyp Ref Expression
1 oa00 ⊢B∈On∧C∈On→B+𝑜C=∅↔B=∅∧C=∅
2 1 biimpar ⊢B∈On∧C∈On∧B=∅∧C=∅→B+𝑜C=∅
3 2 oveq2d ⊢B∈On∧C∈On∧B=∅∧C=∅→∅↑𝑜B+𝑜C=∅↑𝑜∅
4 oveq2 ⊢B=∅→∅↑𝑜B=∅↑𝑜∅
5 oveq2 ⊢C=∅→∅↑𝑜C=∅↑𝑜∅
6 oe0m0 ⊢∅↑𝑜∅=1𝑜
7 5 6 eqtrdi ⊢C=∅→∅↑𝑜C=1𝑜
8 4 7 oveqan12d ⊢B=∅∧C=∅→∅↑𝑜B⋅𝑜∅↑𝑜C=∅↑𝑜∅⋅𝑜1𝑜
9 0elon ⊢∅∈On
10 oecl ⊢∅∈On∧∅∈On→∅↑𝑜∅∈On
11 9 9 10 mp2an ⊢∅↑𝑜∅∈On
12 om1 ⊢∅↑𝑜∅∈On→∅↑𝑜∅⋅𝑜1𝑜=∅↑𝑜∅
13 11 12 ax-mp ⊢∅↑𝑜∅⋅𝑜1𝑜=∅↑𝑜∅
14 8 13 eqtrdi ⊢B=∅∧C=∅→∅↑𝑜B⋅𝑜∅↑𝑜C=∅↑𝑜∅
15 14 adantl ⊢B∈On∧C∈On∧B=∅∧C=∅→∅↑𝑜B⋅𝑜∅↑𝑜C=∅↑𝑜∅
16 3 15 eqtr4d ⊢B∈On∧C∈On∧B=∅∧C=∅→∅↑𝑜B+𝑜C=∅↑𝑜B⋅𝑜∅↑𝑜C
17 oacl ⊢B∈On∧C∈On→B+𝑜C∈On
18 on0eln0 ⊢B+𝑜C∈On→∅∈B+𝑜C↔B+𝑜C≠∅
19 17 18 syl ⊢B∈On∧C∈On→∅∈B+𝑜C↔B+𝑜C≠∅
20 oe0m1 ⊢B+𝑜C∈On→∅∈B+𝑜C↔∅↑𝑜B+𝑜C=∅
21 17 20 syl ⊢B∈On∧C∈On→∅∈B+𝑜C↔∅↑𝑜B+𝑜C=∅
22 1 necon3abid ⊢B∈On∧C∈On→B+𝑜C≠∅↔¬B=∅∧C=∅
23 19 21 22 3bitr3d ⊢B∈On∧C∈On→∅↑𝑜B+𝑜C=∅↔¬B=∅∧C=∅
24 23 biimpar ⊢B∈On∧C∈On∧¬B=∅∧C=∅→∅↑𝑜B+𝑜C=∅
25 on0eln0 ⊢B∈On→∅∈B↔B≠∅
26 25 adantr ⊢B∈On∧C∈On→∅∈B↔B≠∅
27 on0eln0 ⊢C∈On→∅∈C↔C≠∅
28 27 adantl ⊢B∈On∧C∈On→∅∈C↔C≠∅
29 26 28 orbi12d ⊢B∈On∧C∈On→∅∈B∨∅∈C↔B≠∅∨C≠∅
30 neorian ⊢B≠∅∨C≠∅↔¬B=∅∧C=∅
31 29 30 bitrdi ⊢B∈On∧C∈On→∅∈B∨∅∈C↔¬B=∅∧C=∅
32 oe0m1 ⊢B∈On→∅∈B↔∅↑𝑜B=∅
33 32 biimpa ⊢B∈On∧∅∈B→∅↑𝑜B=∅
34 33 oveq1d ⊢B∈On∧∅∈B→∅↑𝑜B⋅𝑜∅↑𝑜C=∅⋅𝑜∅↑𝑜C
35 oecl ⊢∅∈On∧C∈On→∅↑𝑜C∈On
36 9 35 mpan ⊢C∈On→∅↑𝑜C∈On
37 om0r ⊢∅↑𝑜C∈On→∅⋅𝑜∅↑𝑜C=∅
38 36 37 syl ⊢C∈On→∅⋅𝑜∅↑𝑜C=∅
39 34 38 sylan9eq ⊢B∈On∧∅∈B∧C∈On→∅↑𝑜B⋅𝑜∅↑𝑜C=∅
40 39 an32s ⊢B∈On∧C∈On∧∅∈B→∅↑𝑜B⋅𝑜∅↑𝑜C=∅
41 oe0m1 ⊢C∈On→∅∈C↔∅↑𝑜C=∅
42 41 biimpa ⊢C∈On∧∅∈C→∅↑𝑜C=∅
43 42 oveq2d ⊢C∈On∧∅∈C→∅↑𝑜B⋅𝑜∅↑𝑜C=∅↑𝑜B⋅𝑜∅
44 oecl ⊢∅∈On∧B∈On→∅↑𝑜B∈On
45 9 44 mpan ⊢B∈On→∅↑𝑜B∈On
46 om0 ⊢∅↑𝑜B∈On→∅↑𝑜B⋅𝑜∅=∅
47 45 46 syl ⊢B∈On→∅↑𝑜B⋅𝑜∅=∅
48 43 47 sylan9eqr ⊢B∈On∧C∈On∧∅∈C→∅↑𝑜B⋅𝑜∅↑𝑜C=∅
49 48 anassrs ⊢B∈On∧C∈On∧∅∈C→∅↑𝑜B⋅𝑜∅↑𝑜C=∅
50 40 49 jaodan ⊢B∈On∧C∈On∧∅∈B∨∅∈C→∅↑𝑜B⋅𝑜∅↑𝑜C=∅
51 50 ex ⊢B∈On∧C∈On→∅∈B∨∅∈C→∅↑𝑜B⋅𝑜∅↑𝑜C=∅
52 31 51 sylbird ⊢B∈On∧C∈On→¬B=∅∧C=∅→∅↑𝑜B⋅𝑜∅↑𝑜C=∅
53 52 imp ⊢B∈On∧C∈On∧¬B=∅∧C=∅→∅↑𝑜B⋅𝑜∅↑𝑜C=∅
54 24 53 eqtr4d ⊢B∈On∧C∈On∧¬B=∅∧C=∅→∅↑𝑜B+𝑜C=∅↑𝑜B⋅𝑜∅↑𝑜C
55 16 54 pm2.61dan ⊢B∈On∧C∈On→∅↑𝑜B+𝑜C=∅↑𝑜B⋅𝑜∅↑𝑜C
56 oveq1 ⊢A=∅→A↑𝑜B+𝑜C=∅↑𝑜B+𝑜C
57 oveq1 ⊢A=∅→A↑𝑜B=∅↑𝑜B
58 oveq1 ⊢A=∅→A↑𝑜C=∅↑𝑜C
59 57 58 oveq12d ⊢A=∅→A↑𝑜B⋅𝑜A↑𝑜C=∅↑𝑜B⋅𝑜∅↑𝑜C
60 56 59 eqeq12d ⊢A=∅→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C↔∅↑𝑜B+𝑜C=∅↑𝑜B⋅𝑜∅↑𝑜C
61 55 60 imbitrrid ⊢A=∅→B∈On∧C∈On→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C
62 61 impcom ⊢B∈On∧C∈On∧A=∅→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C
63 oveq1 ⊢A=ifA∈On∧∅∈AA1𝑜→A↑𝑜B+𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜B+𝑜C
64 oveq1 ⊢A=ifA∈On∧∅∈AA1𝑜→A↑𝑜B=ifA∈On∧∅∈AA1𝑜↑𝑜B
65 oveq1 ⊢A=ifA∈On∧∅∈AA1𝑜→A↑𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜C
66 64 65 oveq12d ⊢A=ifA∈On∧∅∈AA1𝑜→A↑𝑜B⋅𝑜A↑𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜B⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C
67 63 66 eqeq12d ⊢A=ifA∈On∧∅∈AA1𝑜→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C↔ifA∈On∧∅∈AA1𝑜↑𝑜B+𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜B⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C
68 67 imbi2d ⊢A=ifA∈On∧∅∈AA1𝑜→C∈On→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C↔C∈On→ifA∈On∧∅∈AA1𝑜↑𝑜B+𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜B⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C
69 oveq1 ⊢B=ifB∈OnB1𝑜→B+𝑜C=ifB∈OnB1𝑜+𝑜C
70 69 oveq2d ⊢B=ifB∈OnB1𝑜→ifA∈On∧∅∈AA1𝑜↑𝑜B+𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜ifB∈OnB1𝑜+𝑜C
71 oveq2 ⊢B=ifB∈OnB1𝑜→ifA∈On∧∅∈AA1𝑜↑𝑜B=ifA∈On∧∅∈AA1𝑜↑𝑜ifB∈OnB1𝑜
72 71 oveq1d ⊢B=ifB∈OnB1𝑜→ifA∈On∧∅∈AA1𝑜↑𝑜B⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜ifB∈OnB1𝑜⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C
73 70 72 eqeq12d ⊢B=ifB∈OnB1𝑜→ifA∈On∧∅∈AA1𝑜↑𝑜B+𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜B⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C↔ifA∈On∧∅∈AA1𝑜↑𝑜ifB∈OnB1𝑜+𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜ifB∈OnB1𝑜⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C
74 73 imbi2d ⊢B=ifB∈OnB1𝑜→C∈On→ifA∈On∧∅∈AA1𝑜↑𝑜B+𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜B⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C↔C∈On→ifA∈On∧∅∈AA1𝑜↑𝑜ifB∈OnB1𝑜+𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜ifB∈OnB1𝑜⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C
75 eleq1 ⊢A=ifA∈On∧∅∈AA1𝑜→A∈On↔ifA∈On∧∅∈AA1𝑜∈On
76 eleq2 ⊢A=ifA∈On∧∅∈AA1𝑜→∅∈A↔∅∈ifA∈On∧∅∈AA1𝑜
77 75 76 anbi12d ⊢A=ifA∈On∧∅∈AA1𝑜→A∈On∧∅∈A↔ifA∈On∧∅∈AA1𝑜∈On∧∅∈ifA∈On∧∅∈AA1𝑜
78 eleq1 ⊢1𝑜=ifA∈On∧∅∈AA1𝑜→1𝑜∈On↔ifA∈On∧∅∈AA1𝑜∈On
79 eleq2 ⊢1𝑜=ifA∈On∧∅∈AA1𝑜→∅∈1𝑜↔∅∈ifA∈On∧∅∈AA1𝑜
80 78 79 anbi12d ⊢1𝑜=ifA∈On∧∅∈AA1𝑜→1𝑜∈On∧∅∈1𝑜↔ifA∈On∧∅∈AA1𝑜∈On∧∅∈ifA∈On∧∅∈AA1𝑜
81 1on ⊢1𝑜∈On
82 0lt1o ⊢∅∈1𝑜
83 81 82 pm3.2i ⊢1𝑜∈On∧∅∈1𝑜
84 77 80 83 elimhyp ⊢ifA∈On∧∅∈AA1𝑜∈On∧∅∈ifA∈On∧∅∈AA1𝑜
85 84 simpli ⊢ifA∈On∧∅∈AA1𝑜∈On
86 84 simpri ⊢∅∈ifA∈On∧∅∈AA1𝑜
87 81 elimel ⊢ifB∈OnB1𝑜∈On
88 85 86 87 oeoalem ⊢C∈On→ifA∈On∧∅∈AA1𝑜↑𝑜ifB∈OnB1𝑜+𝑜C=ifA∈On∧∅∈AA1𝑜↑𝑜ifB∈OnB1𝑜⋅𝑜ifA∈On∧∅∈AA1𝑜↑𝑜C
89 68 74 88 dedth2h ⊢A∈On∧∅∈A∧B∈On→C∈On→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C
90 89 impr ⊢A∈On∧∅∈A∧B∈On∧C∈On→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C
91 90 an32s ⊢A∈On∧B∈On∧C∈On∧∅∈A→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C
92 62 91 oe0lem ⊢A∈On∧B∈On∧C∈On→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C
93 92 3impb ⊢A∈On∧B∈On∧C∈On→A↑𝑜B+𝑜C=A↑𝑜B⋅𝑜A↑𝑜C