Metamath Proof Explorer

Theorem oecl

Description: Closure law for ordinal exponentiation. (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 syl5ibr ⊢ ( 𝐴 = ∅ → ( 𝐵 ∈ 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 syl5ibr ⊢ ( ( 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 )