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 A On B On A 𝑜 B On

Proof

Step Hyp Ref Expression
1 oveq2 B = 𝑜 B = 𝑜
2 oe0m0 𝑜 = 1 𝑜
3 1on 1 𝑜 On
4 2 3 eqeltri 𝑜 On
5 1 4 syl6eqel B = 𝑜 B On
6 5 adantl B On B = 𝑜 B On
7 oe0m1 B On B 𝑜 B =
8 7 biimpa B On B 𝑜 B =
9 0elon On
10 8 9 syl6eqel B On B 𝑜 B On
11 10 adantll B On B On B 𝑜 B On
12 6 11 oe0lem B On B On 𝑜 B On
13 12 anidms B On 𝑜 B On
14 oveq1 A = A 𝑜 B = 𝑜 B
15 14 eleq1d A = A 𝑜 B On 𝑜 B On
16 13 15 syl5ibr A = B On A 𝑜 B On
17 16 impcom B On A = A 𝑜 B On
18 oveq2 x = A 𝑜 x = A 𝑜
19 18 eleq1d x = A 𝑜 x On A 𝑜 On
20 oveq2 x = y A 𝑜 x = A 𝑜 y
21 20 eleq1d x = y A 𝑜 x On A 𝑜 y On
22 oveq2 x = suc y A 𝑜 x = A 𝑜 suc y
23 22 eleq1d x = suc y A 𝑜 x On A 𝑜 suc y On
24 oveq2 x = B A 𝑜 x = A 𝑜 B
25 24 eleq1d x = B A 𝑜 x On A 𝑜 B On
26 oe0 A On A 𝑜 = 1 𝑜
27 26 3 syl6eqel A On A 𝑜 On
28 27 adantr A On A A 𝑜 On
29 omcl A 𝑜 y On A On A 𝑜 y 𝑜 A On
30 29 expcom A On A 𝑜 y On A 𝑜 y 𝑜 A On
31 30 adantr A On y On A 𝑜 y On A 𝑜 y 𝑜 A On
32 oesuc A On y On A 𝑜 suc y = A 𝑜 y 𝑜 A
33 32 eleq1d A On y On A 𝑜 suc y On A 𝑜 y 𝑜 A On
34 31 33 sylibrd A On y On A 𝑜 y On A 𝑜 suc y On
35 34 expcom y On A On A 𝑜 y On A 𝑜 suc y On
36 35 adantrd y On A On A A 𝑜 y On A 𝑜 suc y On
37 vex x V
38 iunon x V y x A 𝑜 y On y x A 𝑜 y On
39 37 38 mpan y x A 𝑜 y On y x A 𝑜 y On
40 oelim A On x V Lim x A A 𝑜 x = y x A 𝑜 y
41 37 40 mpanlr1 A On Lim x A A 𝑜 x = y x A 𝑜 y
42 41 anasss A On Lim x A A 𝑜 x = y x A 𝑜 y
43 42 an12s Lim x A On A A 𝑜 x = y x A 𝑜 y
44 43 eleq1d Lim x A On A A 𝑜 x On y x A 𝑜 y On
45 39 44 syl5ibr Lim x A On A y x A 𝑜 y On A 𝑜 x On
46 45 ex Lim x A On A y x A 𝑜 y On A 𝑜 x On
47 19 21 23 25 28 36 46 tfinds3 B On A On A A 𝑜 B On
48 47 expd B On A On A A 𝑜 B On
49 48 com12 A On B On A A 𝑜 B On
50 49 imp31 A On B On A A 𝑜 B On
51 17 50 oe0lem A On B On A 𝑜 B On