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 ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → Lim ( 𝐴 ↑o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eldifi ⊢ ( 𝐴 ∈ ( On ∖ 2o ) → 𝐴 ∈ On )
2 limelon ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On )
3 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
5 eloni ⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ On → Ord ( 𝐴 ↑o 𝐵 ) )
6 4 5 syl ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → Ord ( 𝐴 ↑o 𝐵 ) )
7 1 adantr ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → 𝐴 ∈ On )
8 2 adantl ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → 𝐵 ∈ On )
9 dif20el ⊢ ( 𝐴 ∈ ( On ∖ 2o ) → ∅ ∈ 𝐴 )
10 9 adantr ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ∅ ∈ 𝐴 )
11 oen0 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴 ↑o 𝐵 ) )
12 7 8 10 11 syl21anc ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ∅ ∈ ( 𝐴 ↑o 𝐵 ) )
13 oelim2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑦 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) )
14 1 13 sylan ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑦 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) )
15 14 eleq2d ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) ↔ 𝑥 ∈ ∪ 𝑦 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ) )
16 eliun ⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ↔ ∃ 𝑦 ∈ ( 𝐵 ∖ 1o ) 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) )
17 eldifi ⊢ ( 𝑦 ∈ ( 𝐵 ∖ 1o ) → 𝑦 ∈ 𝐵 )
18 7 adantr ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → 𝐴 ∈ On )
19 8 adantr ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → 𝐵 ∈ On )
20 simprl ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → 𝑦 ∈ 𝐵 )
21 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ On )
22 19 20 21 syl2anc ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → 𝑦 ∈ On )
23 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
24 18 22 23 syl2anc ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
25 eloni ⊢ ( ( 𝐴 ↑o 𝑦 ) ∈ On → Ord ( 𝐴 ↑o 𝑦 ) )
26 24 25 syl ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → Ord ( 𝐴 ↑o 𝑦 ) )
27 simprr ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) )
28 ordsucss ⊢ ( Ord ( 𝐴 ↑o 𝑦 ) → ( 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) → suc 𝑥 ⊆ ( 𝐴 ↑o 𝑦 ) ) )
29 26 27 28 sylc ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → suc 𝑥 ⊆ ( 𝐴 ↑o 𝑦 ) )
30 simpll ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → 𝐴 ∈ ( On ∖ 2o ) )
31 oeordi ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝑦 ∈ 𝐵 → ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o 𝐵 ) ) )
32 19 30 31 syl2anc ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → ( 𝑦 ∈ 𝐵 → ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o 𝐵 ) ) )
33 20 32 mpd ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o 𝐵 ) )
34 onelon ⊢ ( ( ( 𝐴 ↑o 𝑦 ) ∈ On ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) → 𝑥 ∈ On )
35 24 27 34 syl2anc ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → 𝑥 ∈ On )
36 suceloni ⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On )
37 35 36 syl ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → suc 𝑥 ∈ On )
38 4 adantr ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
39 ontr2 ⊢ ( ( suc 𝑥 ∈ On ∧ ( 𝐴 ↑o 𝐵 ) ∈ On ) → ( ( suc 𝑥 ⊆ ( 𝐴 ↑o 𝑦 ) ∧ ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o 𝐵 ) ) → suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) ) )
40 37 38 39 syl2anc ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → ( ( suc 𝑥 ⊆ ( 𝐴 ↑o 𝑦 ) ∧ ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o 𝐵 ) ) → suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) ) )
41 29 33 40 mp2and ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) ) ) → suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) )
42 41 expr ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) → suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) ) )
43 17 42 sylan2 ⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 1o ) ) → ( 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) → suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) ) )
44 43 rexlimdva ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( ∃ 𝑦 ∈ ( 𝐵 ∖ 1o ) 𝑥 ∈ ( 𝐴 ↑o 𝑦 ) → suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) ) )
45 16 44 syl5bi ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝑥 ∈ ∪ 𝑦 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) → suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) ) )
46 15 45 sylbid ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) → suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) ) )
47 46 ralrimiv ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ∀ 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) )
48 dflim4 ⊢ ( Lim ( 𝐴 ↑o 𝐵 ) ↔ ( Ord ( 𝐴 ↑o 𝐵 ) ∧ ∅ ∈ ( 𝐴 ↑o 𝐵 ) ∧ ∀ 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) suc 𝑥 ∈ ( 𝐴 ↑o 𝐵 ) ) )
49 6 12 47 48 syl3anbrc ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → Lim ( 𝐴 ↑o 𝐵 ) )