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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝐶 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝐶 ) ) )

Proof

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