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	imbitrrid	⊢ ( 𝐴 = ∅ → ( ( 𝐵 ∈ 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 𝐶 ) ) )