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. (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Assertion oeoa ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝐶 ) ) )

Proof

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