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 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 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 ⊢ C ∈ On → 1 𝑜 ↑ 𝑜 C = 1 𝑜
6 4 5 sylan9eqr ⊢ C ∈ On ∧ B = ∅ → ∅ ↑ 𝑜 B ↑ 𝑜 C = 1 𝑜
7 6 adantll ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ → ∅ ↑ 𝑜 B ↑ 𝑜 C = 1 𝑜
8 oveq2 ⊢ C = ∅ → ∅ ↑ 𝑜 B ↑ 𝑜 C = ∅ ↑ 𝑜 B ↑ 𝑜 ∅
9 0elon ⊢ ∅ ∈ On
10 oecl ⊢ ∅ ∈ On ∧ B ∈ On → ∅ ↑ 𝑜 B ∈ On
11 9 10 mpan ⊢ B ∈ On → ∅ ↑ 𝑜 B ∈ On
12 oe0 ⊢ ∅ ↑ 𝑜 B ∈ On → ∅ ↑ 𝑜 B ↑ 𝑜 ∅ = 1 𝑜
13 11 12 syl ⊢ B ∈ On → ∅ ↑ 𝑜 B ↑ 𝑜 ∅ = 1 𝑜
14 8 13 sylan9eqr ⊢ B ∈ On ∧ C = ∅ → ∅ ↑ 𝑜 B ↑ 𝑜 C = 1 𝑜
15 14 adantlr ⊢ B ∈ On ∧ C ∈ On ∧ C = ∅ → ∅ ↑ 𝑜 B ↑ 𝑜 C = 1 𝑜
16 7 15 jaodan ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ ∨ C = ∅ → ∅ ↑ 𝑜 B ↑ 𝑜 C = 1 𝑜
17 om00 ⊢ B ∈ On ∧ C ∈ On → B ⋅ 𝑜 C = ∅ ↔ B = ∅ ∨ C = ∅
18 17 biimpar ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ ∨ C = ∅ → B ⋅ 𝑜 C = ∅
19 18 oveq2d ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ ∨ C = ∅ → ∅ ↑ 𝑜 B ⋅ 𝑜 C = ∅ ↑ 𝑜 ∅
20 19 2 eqtrdi ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ ∨ C = ∅ → ∅ ↑ 𝑜 B ⋅ 𝑜 C = 1 𝑜
21 16 20 eqtr4d ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ ∨ C = ∅ → ∅ ↑ 𝑜 B ↑ 𝑜 C = ∅ ↑ 𝑜 B ⋅ 𝑜 C
22 on0eln0 ⊢ B ∈ On → ∅ ∈ B ↔ B ≠ ∅
23 on0eln0 ⊢ C ∈ On → ∅ ∈ C ↔ C ≠ ∅
24 22 23 bi2anan9 ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ∧ ∅ ∈ C ↔ B ≠ ∅ ∧ C ≠ ∅
25 neanior ⊢ B ≠ ∅ ∧ C ≠ ∅ ↔ ¬ B = ∅ ∨ C = ∅
26 24 25 bitrdi ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ∧ ∅ ∈ C ↔ ¬ B = ∅ ∨ C = ∅
27 oe0m1 ⊢ B ∈ On → ∅ ∈ B ↔ ∅ ↑ 𝑜 B = ∅
28 27 biimpa ⊢ B ∈ On ∧ ∅ ∈ B → ∅ ↑ 𝑜 B = ∅
29 28 oveq1d ⊢ B ∈ On ∧ ∅ ∈ B → ∅ ↑ 𝑜 B ↑ 𝑜 C = ∅ ↑ 𝑜 C
30 oe0m1 ⊢ C ∈ On → ∅ ∈ C ↔ ∅ ↑ 𝑜 C = ∅
31 30 biimpa ⊢ C ∈ On ∧ ∅ ∈ C → ∅ ↑ 𝑜 C = ∅
32 29 31 sylan9eq ⊢ B ∈ On ∧ ∅ ∈ B ∧ C ∈ On ∧ ∅ ∈ C → ∅ ↑ 𝑜 B ↑ 𝑜 C = ∅
33 32 an4s ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ B ∧ ∅ ∈ C → ∅ ↑ 𝑜 B ↑ 𝑜 C = ∅
34 om00el ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ⋅ 𝑜 C ↔ ∅ ∈ B ∧ ∅ ∈ C
35 omcl ⊢ B ∈ On ∧ C ∈ On → B ⋅ 𝑜 C ∈ On
36 oe0m1 ⊢ B ⋅ 𝑜 C ∈ On → ∅ ∈ B ⋅ 𝑜 C ↔ ∅ ↑ 𝑜 B ⋅ 𝑜 C = ∅
37 35 36 syl ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ⋅ 𝑜 C ↔ ∅ ↑ 𝑜 B ⋅ 𝑜 C = ∅
38 34 37 bitr3d ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ∧ ∅ ∈ C ↔ ∅ ↑ 𝑜 B ⋅ 𝑜 C = ∅
39 38 biimpa ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ B ∧ ∅ ∈ C → ∅ ↑ 𝑜 B ⋅ 𝑜 C = ∅
40 33 39 eqtr4d ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ B ∧ ∅ ∈ C → ∅ ↑ 𝑜 B ↑ 𝑜 C = ∅ ↑ 𝑜 B ⋅ 𝑜 C
41 40 ex ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ∧ ∅ ∈ C → ∅ ↑ 𝑜 B ↑ 𝑜 C = ∅ ↑ 𝑜 B ⋅ 𝑜 C
42 26 41 sylbird ⊢ B ∈ On ∧ C ∈ On → ¬ B = ∅ ∨ C = ∅ → ∅ ↑ 𝑜 B ↑ 𝑜 C = ∅ ↑ 𝑜 B ⋅ 𝑜 C
43 42 imp ⊢ B ∈ On ∧ C ∈ On ∧ ¬ B = ∅ ∨ C = ∅ → ∅ ↑ 𝑜 B ↑ 𝑜 C = ∅ ↑ 𝑜 B ⋅ 𝑜 C
44 21 43 pm2.61dan ⊢ B ∈ On ∧ C ∈ On → ∅ ↑ 𝑜 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 imbitrrid ⊢ A = ∅ → B ∈ On ∧ C ∈ On → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C
50 49 impcom ⊢ B ∈ On ∧ C ∈ On ∧ A = ∅ → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C
51 oveq1 ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ↑ 𝑜 B = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B
52 51 oveq1d ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ↑ 𝑜 B ↑ 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ↑ 𝑜 C
53 oveq1 ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ↑ 𝑜 B ⋅ 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 C
54 52 53 eqeq12d ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ↑ 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 C
55 54 imbi2d ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → B ∈ On ∧ C ∈ On → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C ↔ B ∈ On ∧ C ∈ On → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ↑ 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 C
56 eleq1 ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ∈ On ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On
57 eleq2 ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → ∅ ∈ A ↔ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
58 56 57 anbi12d ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ∈ On ∧ ∅ ∈ A ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On ∧ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
59 eleq1 ⊢ 1 𝑜 = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → 1 𝑜 ∈ On ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On
60 eleq2 ⊢ 1 𝑜 = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → ∅ ∈ 1 𝑜 ↔ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
61 59 60 anbi12d ⊢ 1 𝑜 = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → 1 𝑜 ∈ On ∧ ∅ ∈ 1 𝑜 ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On ∧ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
62 1on ⊢ 1 𝑜 ∈ On
63 0lt1o ⊢ ∅ ∈ 1 𝑜
64 62 63 pm3.2i ⊢ 1 𝑜 ∈ On ∧ ∅ ∈ 1 𝑜
65 58 61 64 elimhyp ⊢ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On ∧ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
66 65 simpli ⊢ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On
67 65 simpri ⊢ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
68 66 67 oeoelem ⊢ B ∈ On ∧ C ∈ On → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ↑ 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 C
69 55 68 dedth ⊢ A ∈ On ∧ ∅ ∈ A → B ∈ On ∧ C ∈ On → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C
70 69 imp ⊢ A ∈ On ∧ ∅ ∈ A ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C
71 70 an32s ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C
72 50 71 oe0lem ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C
73 72 3impb ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C