Theorem oecl

Description: Closure law for ordinal exponentiation. Remark 2.8 of Schloeder p. 5. (Contributed by NM, 1-Jan-2005) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Assertion	oecl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝐵 = ∅ → ( ∅ ↑o 𝐵 ) = ( ∅ ↑o ∅ ) )
2		oe0m0	⊢ ( ∅ ↑o ∅ ) = 1o
3		1on	⊢ 1o ∈ On
4	2 3	eqeltri	⊢ ( ∅ ↑o ∅ ) ∈ On
5	1 4	eqeltrdi	⊢ ( 𝐵 = ∅ → ( ∅ ↑o 𝐵 ) ∈ On )
6	5	adantl	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 = ∅ ) → ( ∅ ↑o 𝐵 ) ∈ On )
7		oe0m1	⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) )
8	7	biimpa	⊢ ( ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ )
9		0elon	⊢ ∅ ∈ On
10	8 9	eqeltrdi	⊢ ( ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) ∈ On )
11	10	adantll	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) ∈ On )
12	6 11	oe0lem	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ↑o 𝐵 ) ∈ On )
13	12	anidms	⊢ ( 𝐵 ∈ On → ( ∅ ↑o 𝐵 ) ∈ On )
14		oveq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ( ∅ ↑o 𝐵 ) )
15	14	eleq1d	⊢ ( 𝐴 = ∅ → ( ( 𝐴 ↑o 𝐵 ) ∈ On ↔ ( ∅ ↑o 𝐵 ) ∈ On ) )
16	13 15	imbitrrid	⊢ ( 𝐴 = ∅ → ( 𝐵 ∈ On → ( 𝐴 ↑o 𝐵 ) ∈ On ) )
17	16	impcom	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
18		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o ∅ ) )
19	18	eleq1d	⊢ ( 𝑥 = ∅ → ( ( 𝐴 ↑o 𝑥 ) ∈ On ↔ ( 𝐴 ↑o ∅ ) ∈ On ) )
20		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝑦 ) )
21	20	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑o 𝑥 ) ∈ On ↔ ( 𝐴 ↑o 𝑦 ) ∈ On ) )
22		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑦 ) )
23	22	eleq1d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ↑o 𝑥 ) ∈ On ↔ ( 𝐴 ↑o suc 𝑦 ) ∈ On ) )
24		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝐵 ) )
25	24	eleq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ↑o 𝑥 ) ∈ On ↔ ( 𝐴 ↑o 𝐵 ) ∈ On ) )
26		oe0	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) = 1o )
27	26 3	eqeltrdi	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) ∈ On )
28	27	adantr	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o ∅ ) ∈ On )
29		omcl	⊢ ( ( ( 𝐴 ↑o 𝑦 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ∈ On )
30	29	expcom	⊢ ( 𝐴 ∈ On → ( ( 𝐴 ↑o 𝑦 ) ∈ On → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ∈ On ) )
31	30	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ↑o 𝑦 ) ∈ On → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ∈ On ) )
32		oesuc	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o suc 𝑦 ) = ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) )
33	32	eleq1d	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ↑o suc 𝑦 ) ∈ On ↔ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ∈ On ) )
34	31 33	sylibrd	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ↑o 𝑦 ) ∈ On → ( 𝐴 ↑o suc 𝑦 ) ∈ On ) )
35	34	expcom	⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( ( 𝐴 ↑o 𝑦 ) ∈ On → ( 𝐴 ↑o suc 𝑦 ) ∈ On ) ) )
36	35	adantrd	⊢ ( 𝑦 ∈ On → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ↑o 𝑦 ) ∈ On → ( 𝐴 ↑o suc 𝑦 ) ∈ On ) ) )
37		vex	⊢ 𝑥 ∈ V
38		iunon	⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ∈ On ) → ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ∈ On )
39	37 38	mpan	⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ∈ On → ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ∈ On )
40		oelim	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
41	37 40	mpanlr1	⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
42	41	anasss	⊢ ( ( 𝐴 ∈ On ∧ ( Lim 𝑥 ∧ ∅ ∈ 𝐴 ) ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
43	42	an12s	⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
44	43	eleq1d	⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( ( 𝐴 ↑o 𝑥 ) ∈ On ↔ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ∈ On ) )
45	39 44	imbitrrid	⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ∈ On → ( 𝐴 ↑o 𝑥 ) ∈ On ) )
46	45	ex	⊢ ( Lim 𝑥 → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ∈ On → ( 𝐴 ↑o 𝑥 ) ∈ On ) ) )
47	19 21 23 25 28 36 46	tfinds3	⊢ ( 𝐵 ∈ On → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) ∈ On ) )
48	47	expd	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ( 𝐴 ↑o 𝐵 ) ∈ On ) ) )
49	48	com12	⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( ∅ ∈ 𝐴 → ( 𝐴 ↑o 𝐵 ) ∈ On ) ) )
50	49	imp31	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
51	17 50	oe0lem	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )