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 e. ( On \ 2o ) /\ ( B e. C /\ Lim B ) ) -> Lim ( A ^o B ) )

Proof

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