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 e. On /\ B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )

Proof

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