Theorem oeoe 7300

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.)

Assertion

Ref	Expression
oeoe	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )

Proof of Theorem oeoe

Step	Hyp	Ref	Expression
1		oveq2 6298	. . . . . . . . . . . 12 |- ( B = (/) -> ( (/) ^o B ) = ( (/) ^o (/) ) )
2		oe0m0 7222	. . . . . . . . . . . 12 |- ( (/) ^o (/) ) = 1o
3	1, 2	syl6eq 2501	. . . . . . . . . . 11 |- ( B = (/) -> ( (/) ^o B ) = 1o )
4	3	oveq1d 6305	. . . . . . . . . 10 |- ( B = (/) -> ( ( (/) ^o B ) ^o C ) = ( 1o ^o C ) )
5		oe1m 7246	. . . . . . . . . 10 |- ( C e. On -> ( 1o ^o C ) = 1o )
6	4, 5	sylan9eqr 2507	. . . . . . . . 9 |- ( ( C e. On /\ B = (/) ) -> ( ( (/) ^o B ) ^o C ) = 1o )
7	6	adantll 720	. . . . . . . 8 |- ( ( ( B e. On /\ C e. On ) /\ B = (/) ) -> ( ( (/) ^o B ) ^o C ) = 1o )
8		oveq2 6298	. . . . . . . . . 10 |- ( C = (/) -> ( ( (/) ^o B ) ^o C ) = ( ( (/) ^o B ) ^o (/) ) )
9		0elon 5476	. . . . . . . . . . . 12 |- (/) e. On
10		oecl 7239	. . . . . . . . . . . 12 |- ( ( (/) e. On /\ B e. On ) -> ( (/) ^o B ) e. On )
11	9, 10	mpan 676	. . . . . . . . . . 11 |- ( B e. On -> ( (/) ^o B ) e. On )
12		oe0 7224	. . . . . . . . . . 11 |- ( ( (/) ^o B ) e. On -> ( ( (/) ^o B ) ^o (/) ) = 1o )
13	11, 12	syl 17	. . . . . . . . . 10 |- ( B e. On -> ( ( (/) ^o B ) ^o (/) ) = 1o )
14	8, 13	sylan9eqr 2507	. . . . . . . . 9 |- ( ( B e. On /\ C = (/) ) -> ( ( (/) ^o B ) ^o C ) = 1o )
15	14	adantlr 721	. . . . . . . 8 |- ( ( ( B e. On /\ C e. On ) /\ C = (/) ) -> ( ( (/) ^o B ) ^o C ) = 1o )
16	7, 15	jaodan 794	. . . . . . 7 |- ( ( ( B e. On /\ C e. On ) /\ ( B = (/) \/ C = (/) ) ) -> ( ( (/) ^o B ) ^o C ) = 1o )
17		om00 7276	. . . . . . . . . 10 |- ( ( B e. On /\ C e. On ) -> ( ( B .o C ) = (/) <-> ( B = (/) \/ C = (/) ) ) )
18	17	biimpar 488	. . . . . . . . 9 |- ( ( ( B e. On /\ C e. On ) /\ ( B = (/) \/ C = (/) ) ) -> ( B .o C ) = (/) )
19	18	oveq2d 6306	. . . . . . . 8 |- ( ( ( B e. On /\ C e. On ) /\ ( B = (/) \/ C = (/) ) ) -> ( (/) ^o ( B .o C ) ) = ( (/) ^o (/) ) )
20	19, 2	syl6eq 2501	. . . . . . 7 |- ( ( ( B e. On /\ C e. On ) /\ ( B = (/) \/ C = (/) ) ) -> ( (/) ^o ( B .o C ) ) = 1o )
21	16, 20	eqtr4d 2488	. . . . . 6 |- ( ( ( B e. On /\ C e. On ) /\ ( B = (/) \/ C = (/) ) ) -> ( ( (/) ^o B ) ^o C ) = ( (/) ^o ( B .o C ) ) )
22		on0eln0 5478	. . . . . . . . . 10 |- ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
23		on0eln0 5478	. . . . . . . . . 10 |- ( C e. On -> ( (/) e. C <-> C =/= (/) ) )
24	22, 23	bi2anan9 884	. . . . . . . . 9 |- ( ( B e. On /\ C e. On ) -> ( ( (/) e. B /\ (/) e. C ) <-> ( B =/= (/) /\ C =/= (/) ) ) )
25		neanior 2716	. . . . . . . . 9 |- ( ( B =/= (/) /\ C =/= (/) ) <-> -. ( B = (/) \/ C = (/) ) )
26	24, 25	syl6bb 265	. . . . . . . 8 |- ( ( B e. On /\ C e. On ) -> ( ( (/) e. B /\ (/) e. C ) <-> -. ( B = (/) \/ C = (/) ) ) )
27		oe0m1 7223	. . . . . . . . . . . . . 14 |- ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
28	27	biimpa 487	. . . . . . . . . . . . 13 |- ( ( B e. On /\ (/) e. B ) -> ( (/) ^o B ) = (/) )
29	28	oveq1d 6305	. . . . . . . . . . . 12 |- ( ( B e. On /\ (/) e. B ) -> ( ( (/) ^o B ) ^o C ) = ( (/) ^o C ) )
30		oe0m1 7223	. . . . . . . . . . . . 13 |- ( C e. On -> ( (/) e. C <-> ( (/) ^o C ) = (/) ) )
31	30	biimpa 487	. . . . . . . . . . . 12 |- ( ( C e. On /\ (/) e. C ) -> ( (/) ^o C ) = (/) )
32	29, 31	sylan9eq 2505	. . . . . . . . . . 11 |- ( ( ( B e. On /\ (/) e. B ) /\ ( C e. On /\ (/) e. C ) ) -> ( ( (/) ^o B ) ^o C ) = (/) )
33	32	an4s 835	. . . . . . . . . 10 |- ( ( ( B e. On /\ C e. On ) /\ ( (/) e. B /\ (/) e. C ) ) -> ( ( (/) ^o B ) ^o C ) = (/) )
34		om00el 7277	. . . . . . . . . . . 12 |- ( ( B e. On /\ C e. On ) -> ( (/) e. ( B .o C ) <-> ( (/) e. B /\ (/) e. C ) ) )
35		omcl 7238	. . . . . . . . . . . . 13 |- ( ( B e. On /\ C e. On ) -> ( B .o C ) e. On )
36		oe0m1 7223	. . . . . . . . . . . . 13 |- ( ( B .o C ) e. On -> ( (/) e. ( B .o C ) <-> ( (/) ^o ( B .o C ) ) = (/) ) )
37	35, 36	syl 17	. . . . . . . . . . . 12 |- ( ( B e. On /\ C e. On ) -> ( (/) e. ( B .o C ) <-> ( (/) ^o ( B .o C ) ) = (/) ) )
38	34, 37	bitr3d 259	. . . . . . . . . . 11 |- ( ( B e. On /\ C e. On ) -> ( ( (/) e. B /\ (/) e. C ) <-> ( (/) ^o ( B .o C ) ) = (/) ) )
39	38	biimpa 487	. . . . . . . . . 10 |- ( ( ( B e. On /\ C e. On ) /\ ( (/) e. B /\ (/) e. C ) ) -> ( (/) ^o ( B .o C ) ) = (/) )
40	33, 39	eqtr4d 2488	. . . . . . . . 9 |- ( ( ( B e. On /\ C e. On ) /\ ( (/) e. B /\ (/) e. C ) ) -> ( ( (/) ^o B ) ^o C ) = ( (/) ^o ( B .o C ) ) )
41	40	ex 436	. . . . . . . 8 |- ( ( B e. On /\ C e. On ) -> ( ( (/) e. B /\ (/) e. C ) -> ( ( (/) ^o B ) ^o C ) = ( (/) ^o ( B .o C ) ) ) )
42	26, 41	sylbird 239	. . . . . . 7 |- ( ( B e. On /\ C e. On ) -> ( -. ( B = (/) \/ C = (/) ) -> ( ( (/) ^o B ) ^o C ) = ( (/) ^o ( B .o C ) ) ) )
43	42	imp 431	. . . . . 6 |- ( ( ( B e. On /\ C e. On ) /\ -. ( B = (/) \/ C = (/) ) ) -> ( ( (/) ^o B ) ^o C ) = ( (/) ^o ( B .o C ) ) )
44	21, 43	pm2.61dan 800	. . . . 5 |- ( ( B e. On /\ C e. On ) -> ( ( (/) ^o B ) ^o C ) = ( (/) ^o ( B .o C ) ) )
45		oveq1 6297	. . . . . . 7 |- ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
46	45	oveq1d 6305	. . . . . 6 |- ( A = (/) -> ( ( A ^o B ) ^o C ) = ( ( (/) ^o B ) ^o C ) )
47		oveq1 6297	. . . . . 6 |- ( A = (/) -> ( A ^o ( B .o C ) ) = ( (/) ^o ( B .o C ) ) )
48	46, 47	eqeq12d 2466	. . . . 5 |- ( A = (/) -> ( ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) <-> ( ( (/) ^o B ) ^o C ) = ( (/) ^o ( B .o C ) ) ) )
49	44, 48	syl5ibr 225	. . . 4 |- ( A = (/) -> ( ( B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) ) )
50	49	impcom 432	. . 3 |- ( ( ( B e. On /\ C e. On ) /\ A = (/) ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )
51		oveq1 6297	. . . . . . . . 9 |- ( 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 6305	. . . . . . . 8 |- ( 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 6297	. . . . . . . 8 |- ( 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 2466	. . . . . . 7 |- ( 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 318	. . . . . 6 |- ( 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 2517	. . . . . . . . . 10 |- ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( A e. On <-> if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On ) )
57		eleq2 2518	. . . . . . . . . 10 |- ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( (/) e. A <-> (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o ) ) )
58	56, 57	anbi12d 717	. . . . . . . . 9 |- ( 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 2517	. . . . . . . . . 10 |- ( 1o = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( 1o e. On <-> if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On ) )
60		eleq2 2518	. . . . . . . . . 10 |- ( 1o = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( (/) e. 1o <-> (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o ) ) )
61	59, 60	anbi12d 717	. . . . . . . . 9 |- ( 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 7189	. . . . . . . . . 10 |- 1o e. On
63		0lt1o 7206	. . . . . . . . . 10 |- (/) e. 1o
64	62, 63	pm3.2i 457	. . . . . . . . 9 |- ( 1o e. On /\ (/) e. 1o )
65	58, 61, 64	elimhyp 3939	. . . . . . . 8 |- ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On /\ (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o ) )
66	65	simpli 460	. . . . . . 7 |- if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On
67	65	simpri 464	. . . . . . 7 |- (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o )
68	66, 67	oeoelem 7299	. . . . . 6 |- ( ( 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 3932	. . . . 5 |- ( ( A e. On /\ (/) e. A ) -> ( ( B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) ) )
70	69	imp 431	. . . 4 |- ( ( ( A e. On /\ (/) e. A ) /\ ( B e. On /\ C e. On ) ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )
71	70	an32s 813	. . 3 |- ( ( ( 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 7215	. 2 |- ( ( A e. On /\ ( B e. On /\ C e. On ) ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )
73	72	3impb 1204	1 |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   =/= wne 2622   (/)c0 3731   ifcif 3881   Oncon0 5423  (class class class)co 6290   1oc1o 7175   .o comu 7180   ^o coe 7181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-omul 7187  df-oexp 7188

This theorem is referenced by:  infxpenc  8449