Metamath Proof Explorer


Theorem oelim2

Description: Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of Mendelson p. 250. (Contributed by NM, 6-Jan-2005)

Ref Expression
Assertion oelim2 ( ( 𝐴 ∈ On ∧ ( 𝐵𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴o 𝐵 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) )

Proof

Step Hyp Ref Expression
1 limelon ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On )
2 0ellim ( Lim 𝐵 → ∅ ∈ 𝐵 )
3 2 adantl ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → ∅ ∈ 𝐵 )
4 oe0m1 ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) )
5 4 biimpa ( ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ )
6 1 3 5 syl2anc ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ )
7 eldif ( 𝑥 ∈ ( 𝐵 ∖ 1o ) ↔ ( 𝑥𝐵 ∧ ¬ 𝑥 ∈ 1o ) )
8 limord ( Lim 𝐵 → Ord 𝐵 )
9 ordelon ( ( Ord 𝐵𝑥𝐵 ) → 𝑥 ∈ On )
10 8 9 sylan ( ( Lim 𝐵𝑥𝐵 ) → 𝑥 ∈ On )
11 on0eln0 ( 𝑥 ∈ On → ( ∅ ∈ 𝑥𝑥 ≠ ∅ ) )
12 el1o ( 𝑥 ∈ 1o𝑥 = ∅ )
13 12 necon3bbii ( ¬ 𝑥 ∈ 1o𝑥 ≠ ∅ )
14 11 13 bitr4di ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ ¬ 𝑥 ∈ 1o ) )
15 oe0m1 ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ ( ∅ ↑o 𝑥 ) = ∅ ) )
16 15 biimpd ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 → ( ∅ ↑o 𝑥 ) = ∅ ) )
17 14 16 sylbird ( 𝑥 ∈ On → ( ¬ 𝑥 ∈ 1o → ( ∅ ↑o 𝑥 ) = ∅ ) )
18 10 17 syl ( ( Lim 𝐵𝑥𝐵 ) → ( ¬ 𝑥 ∈ 1o → ( ∅ ↑o 𝑥 ) = ∅ ) )
19 18 impr ( ( Lim 𝐵 ∧ ( 𝑥𝐵 ∧ ¬ 𝑥 ∈ 1o ) ) → ( ∅ ↑o 𝑥 ) = ∅ )
20 7 19 sylan2b ( ( Lim 𝐵𝑥 ∈ ( 𝐵 ∖ 1o ) ) → ( ∅ ↑o 𝑥 ) = ∅ )
21 20 iuneq2dv ( Lim 𝐵 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ∅ )
22 df-1o 1o = suc ∅
23 limsuc ( Lim 𝐵 → ( ∅ ∈ 𝐵 ↔ suc ∅ ∈ 𝐵 ) )
24 2 23 mpbid ( Lim 𝐵 → suc ∅ ∈ 𝐵 )
25 22 24 eqeltrid ( Lim 𝐵 → 1o𝐵 )
26 1on 1o ∈ On
27 26 onirri ¬ 1o ∈ 1o
28 eldif ( 1o ∈ ( 𝐵 ∖ 1o ) ↔ ( 1o𝐵 ∧ ¬ 1o ∈ 1o ) )
29 25 27 28 sylanblrc ( Lim 𝐵 → 1o ∈ ( 𝐵 ∖ 1o ) )
30 ne0i ( 1o ∈ ( 𝐵 ∖ 1o ) → ( 𝐵 ∖ 1o ) ≠ ∅ )
31 iunconst ( ( 𝐵 ∖ 1o ) ≠ ∅ → 𝑥 ∈ ( 𝐵 ∖ 1o ) ∅ = ∅ )
32 29 30 31 3syl ( Lim 𝐵 𝑥 ∈ ( 𝐵 ∖ 1o ) ∅ = ∅ )
33 21 32 eqtrd ( Lim 𝐵 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) = ∅ )
34 33 adantl ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) = ∅ )
35 6 34 eqtr4d ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → ( ∅ ↑o 𝐵 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) )
36 oveq1 ( 𝐴 = ∅ → ( 𝐴o 𝐵 ) = ( ∅ ↑o 𝐵 ) )
37 oveq1 ( 𝐴 = ∅ → ( 𝐴o 𝑥 ) = ( ∅ ↑o 𝑥 ) )
38 37 iuneq2d ( 𝐴 = ∅ → 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) )
39 36 38 eqeq12d ( 𝐴 = ∅ → ( ( 𝐴o 𝐵 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) ↔ ( ∅ ↑o 𝐵 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) ) )
40 35 39 syl5ibr ( 𝐴 = ∅ → ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → ( 𝐴o 𝐵 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) ) )
41 40 impcom ( ( ( 𝐵𝐶 ∧ Lim 𝐵 ) ∧ 𝐴 = ∅ ) → ( 𝐴o 𝐵 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) )
42 oelim ( ( ( 𝐴 ∈ On ∧ ( 𝐵𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴o 𝐵 ) = 𝑦𝐵 ( 𝐴o 𝑦 ) )
43 limsuc ( Lim 𝐵 → ( 𝑦𝐵 ↔ suc 𝑦𝐵 ) )
44 43 biimpa ( ( Lim 𝐵𝑦𝐵 ) → suc 𝑦𝐵 )
45 nsuceq0 suc 𝑦 ≠ ∅
46 dif1o ( suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ↔ ( suc 𝑦𝐵 ∧ suc 𝑦 ≠ ∅ ) )
47 44 45 46 sylanblrc ( ( Lim 𝐵𝑦𝐵 ) → suc 𝑦 ∈ ( 𝐵 ∖ 1o ) )
48 47 ex ( Lim 𝐵 → ( 𝑦𝐵 → suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ) )
49 48 ad2antlr ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦𝐵 → suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ) )
50 sssucid 𝑦 ⊆ suc 𝑦
51 ordelon ( ( Ord 𝐵𝑦𝐵 ) → 𝑦 ∈ On )
52 8 51 sylan ( ( Lim 𝐵𝑦𝐵 ) → 𝑦 ∈ On )
53 suceloni ( 𝑦 ∈ On → suc 𝑦 ∈ On )
54 52 53 jccir ( ( Lim 𝐵𝑦𝐵 ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ) )
55 id ( ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
56 55 3expa ( ( ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ) ∧ 𝐴 ∈ On ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
57 56 ancoms ( ( 𝐴 ∈ On ∧ ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ) ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
58 54 57 sylan2 ( ( 𝐴 ∈ On ∧ ( Lim 𝐵𝑦𝐵 ) ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
59 58 anassrs ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ 𝑦𝐵 ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
60 oewordi ( ( ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ⊆ suc 𝑦 → ( 𝐴o 𝑦 ) ⊆ ( 𝐴o suc 𝑦 ) ) )
61 59 60 sylan ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ 𝑦𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ⊆ suc 𝑦 → ( 𝐴o 𝑦 ) ⊆ ( 𝐴o suc 𝑦 ) ) )
62 61 an32s ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑦𝐵 ) → ( 𝑦 ⊆ suc 𝑦 → ( 𝐴o 𝑦 ) ⊆ ( 𝐴o suc 𝑦 ) ) )
63 50 62 mpi ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑦𝐵 ) → ( 𝐴o 𝑦 ) ⊆ ( 𝐴o suc 𝑦 ) )
64 63 ex ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦𝐵 → ( 𝐴o 𝑦 ) ⊆ ( 𝐴o suc 𝑦 ) ) )
65 49 64 jcad ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦𝐵 → ( suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ∧ ( 𝐴o 𝑦 ) ⊆ ( 𝐴o suc 𝑦 ) ) ) )
66 oveq2 ( 𝑥 = suc 𝑦 → ( 𝐴o 𝑥 ) = ( 𝐴o suc 𝑦 ) )
67 66 sseq2d ( 𝑥 = suc 𝑦 → ( ( 𝐴o 𝑦 ) ⊆ ( 𝐴o 𝑥 ) ↔ ( 𝐴o 𝑦 ) ⊆ ( 𝐴o suc 𝑦 ) ) )
68 67 rspcev ( ( suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ∧ ( 𝐴o 𝑦 ) ⊆ ( 𝐴o suc 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑦 ) ⊆ ( 𝐴o 𝑥 ) )
69 65 68 syl6 ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦𝐵 → ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑦 ) ⊆ ( 𝐴o 𝑥 ) ) )
70 69 ralrimiv ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ∀ 𝑦𝐵𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑦 ) ⊆ ( 𝐴o 𝑥 ) )
71 iunss2 ( ∀ 𝑦𝐵𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑦 ) ⊆ ( 𝐴o 𝑥 ) → 𝑦𝐵 ( 𝐴o 𝑦 ) ⊆ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) )
72 70 71 syl ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → 𝑦𝐵 ( 𝐴o 𝑦 ) ⊆ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) )
73 difss ( 𝐵 ∖ 1o ) ⊆ 𝐵
74 iunss1 ( ( 𝐵 ∖ 1o ) ⊆ 𝐵 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) ⊆ 𝑥𝐵 ( 𝐴o 𝑥 ) )
75 73 74 ax-mp 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) ⊆ 𝑥𝐵 ( 𝐴o 𝑥 )
76 oveq2 ( 𝑥 = 𝑦 → ( 𝐴o 𝑥 ) = ( 𝐴o 𝑦 ) )
77 76 cbviunv 𝑥𝐵 ( 𝐴o 𝑥 ) = 𝑦𝐵 ( 𝐴o 𝑦 )
78 75 77 sseqtri 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) ⊆ 𝑦𝐵 ( 𝐴o 𝑦 )
79 78 a1i ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) ⊆ 𝑦𝐵 ( 𝐴o 𝑦 ) )
80 72 79 eqssd ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → 𝑦𝐵 ( 𝐴o 𝑦 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) )
81 80 adantlrl ( ( ( 𝐴 ∈ On ∧ ( 𝐵𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → 𝑦𝐵 ( 𝐴o 𝑦 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) )
82 42 81 eqtrd ( ( ( 𝐴 ∈ On ∧ ( 𝐵𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴o 𝐵 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) )
83 41 82 oe0lem ( ( 𝐴 ∈ On ∧ ( 𝐵𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴o 𝐵 ) = 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴o 𝑥 ) )