Metamath Proof Explorer


Theorem oelimcl

Description: The ordinal exponential with a limit ordinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion oelimcl A On 2 𝑜 B C Lim B Lim A 𝑜 B

Proof

Step Hyp Ref Expression
1 eldifi A On 2 𝑜 A On
2 limelon B C Lim B B On
3 oecl A On B On A 𝑜 B On
4 1 2 3 syl2an A On 2 𝑜 B C Lim B A 𝑜 B On
5 eloni A 𝑜 B On Ord A 𝑜 B
6 4 5 syl A On 2 𝑜 B C Lim B Ord A 𝑜 B
7 1 adantr A On 2 𝑜 B C Lim B A On
8 2 adantl A On 2 𝑜 B C Lim B B On
9 dif20el A On 2 𝑜 A
10 9 adantr A On 2 𝑜 B C Lim B A
11 oen0 A On B On A A 𝑜 B
12 7 8 10 11 syl21anc A On 2 𝑜 B C Lim B A 𝑜 B
13 oelim2 A On B C Lim B A 𝑜 B = y B 1 𝑜 A 𝑜 y
14 1 13 sylan A On 2 𝑜 B C Lim B A 𝑜 B = y B 1 𝑜 A 𝑜 y
15 14 eleq2d A On 2 𝑜 B C Lim B x A 𝑜 B x y B 1 𝑜 A 𝑜 y
16 eliun x y B 1 𝑜 A 𝑜 y y B 1 𝑜 x A 𝑜 y
17 eldifi y B 1 𝑜 y B
18 7 adantr A On 2 𝑜 B C Lim B y B x A 𝑜 y A On
19 8 adantr A On 2 𝑜 B C Lim B y B x A 𝑜 y B On
20 simprl A On 2 𝑜 B C Lim B y B x A 𝑜 y y B
21 onelon B On y B y On
22 19 20 21 syl2anc A On 2 𝑜 B C Lim B y B x A 𝑜 y y On
23 oecl A On y On A 𝑜 y On
24 18 22 23 syl2anc A On 2 𝑜 B C Lim B y B x A 𝑜 y A 𝑜 y On
25 eloni A 𝑜 y On Ord A 𝑜 y
26 24 25 syl A On 2 𝑜 B C Lim B y B x A 𝑜 y Ord A 𝑜 y
27 simprr A On 2 𝑜 B C Lim B y B x A 𝑜 y x A 𝑜 y
28 ordsucss Ord A 𝑜 y x A 𝑜 y suc x A 𝑜 y
29 26 27 28 sylc A On 2 𝑜 B C Lim B y B x A 𝑜 y suc x A 𝑜 y
30 simpll A On 2 𝑜 B C Lim B y B x A 𝑜 y A On 2 𝑜
31 oeordi B On A On 2 𝑜 y B A 𝑜 y A 𝑜 B
32 19 30 31 syl2anc A On 2 𝑜 B C Lim B y B x A 𝑜 y y B A 𝑜 y A 𝑜 B
33 20 32 mpd A On 2 𝑜 B C Lim B y B x A 𝑜 y A 𝑜 y A 𝑜 B
34 onelon A 𝑜 y On x A 𝑜 y x On
35 24 27 34 syl2anc A On 2 𝑜 B C Lim B y B x A 𝑜 y x On
36 suceloni x On suc x On
37 35 36 syl A On 2 𝑜 B C Lim B y B x A 𝑜 y suc x On
38 4 adantr A On 2 𝑜 B C Lim B y B x A 𝑜 y A 𝑜 B On
39 ontr2 suc x On A 𝑜 B On suc x A 𝑜 y A 𝑜 y A 𝑜 B suc x A 𝑜 B
40 37 38 39 syl2anc A On 2 𝑜 B C Lim B y B x A 𝑜 y suc x A 𝑜 y A 𝑜 y A 𝑜 B suc x A 𝑜 B
41 29 33 40 mp2and A On 2 𝑜 B C Lim B y B x A 𝑜 y suc x A 𝑜 B
42 41 expr A On 2 𝑜 B C Lim B y B x A 𝑜 y suc x A 𝑜 B
43 17 42 sylan2 A On 2 𝑜 B C Lim B y B 1 𝑜 x A 𝑜 y suc x A 𝑜 B
44 43 rexlimdva A On 2 𝑜 B C Lim B y B 1 𝑜 x A 𝑜 y suc x A 𝑜 B
45 16 44 syl5bi A On 2 𝑜 B C Lim B x y B 1 𝑜 A 𝑜 y suc x A 𝑜 B
46 15 45 sylbid A On 2 𝑜 B C Lim B x A 𝑜 B suc x A 𝑜 B
47 46 ralrimiv A On 2 𝑜 B C Lim B x A 𝑜 B suc x A 𝑜 B
48 dflim4 Lim A 𝑜 B Ord A 𝑜 B A 𝑜 B x A 𝑜 B suc x A 𝑜 B
49 6 12 47 48 syl3anbrc A On 2 𝑜 B C Lim B Lim A 𝑜 B