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 AOnBCLimBA𝑜B=xB1𝑜A𝑜x

Proof

Step Hyp Ref Expression
1 limelon BCLimBBOn
2 0ellim LimBB
3 2 adantl BCLimBB
4 oe0m1 BOnB𝑜B=
5 4 biimpa BOnB𝑜B=
6 1 3 5 syl2anc BCLimB𝑜B=
7 eldif xB1𝑜xB¬x1𝑜
8 limord LimBOrdB
9 ordelon OrdBxBxOn
10 8 9 sylan LimBxBxOn
11 on0eln0 xOnxx
12 el1o x1𝑜x=
13 12 necon3bbii ¬x1𝑜x
14 11 13 bitr4di xOnx¬x1𝑜
15 oe0m1 xOnx𝑜x=
16 15 biimpd xOnx𝑜x=
17 14 16 sylbird xOn¬x1𝑜𝑜x=
18 10 17 syl LimBxB¬x1𝑜𝑜x=
19 18 impr LimBxB¬x1𝑜𝑜x=
20 7 19 sylan2b LimBxB1𝑜𝑜x=
21 20 iuneq2dv LimBxB1𝑜𝑜x=xB1𝑜
22 df-1o 1𝑜=suc
23 limsuc LimBBsucB
24 2 23 mpbid LimBsucB
25 22 24 eqeltrid LimB1𝑜B
26 1on 1𝑜On
27 26 onirri ¬1𝑜1𝑜
28 eldif 1𝑜B1𝑜1𝑜B¬1𝑜1𝑜
29 25 27 28 sylanblrc LimB1𝑜B1𝑜
30 ne0i 1𝑜B1𝑜B1𝑜
31 iunconst B1𝑜xB1𝑜=
32 29 30 31 3syl LimBxB1𝑜=
33 21 32 eqtrd LimBxB1𝑜𝑜x=
34 33 adantl BCLimBxB1𝑜𝑜x=
35 6 34 eqtr4d BCLimB𝑜B=xB1𝑜𝑜x
36 oveq1 A=A𝑜B=𝑜B
37 oveq1 A=A𝑜x=𝑜x
38 37 iuneq2d A=xB1𝑜A𝑜x=xB1𝑜𝑜x
39 36 38 eqeq12d A=A𝑜B=xB1𝑜A𝑜x𝑜B=xB1𝑜𝑜x
40 35 39 syl5ibr A=BCLimBA𝑜B=xB1𝑜A𝑜x
41 40 impcom BCLimBA=A𝑜B=xB1𝑜A𝑜x
42 oelim AOnBCLimBAA𝑜B=yBA𝑜y
43 limsuc LimByBsucyB
44 43 biimpa LimByBsucyB
45 nsuceq0 sucy
46 dif1o sucyB1𝑜sucyBsucy
47 44 45 46 sylanblrc LimByBsucyB1𝑜
48 47 ex LimByBsucyB1𝑜
49 48 ad2antlr AOnLimBAyBsucyB1𝑜
50 sssucid ysucy
51 ordelon OrdByByOn
52 8 51 sylan LimByByOn
53 suceloni yOnsucyOn
54 52 53 jccir LimByByOnsucyOn
55 id yOnsucyOnAOnyOnsucyOnAOn
56 55 3expa yOnsucyOnAOnyOnsucyOnAOn
57 56 ancoms AOnyOnsucyOnyOnsucyOnAOn
58 54 57 sylan2 AOnLimByByOnsucyOnAOn
59 58 anassrs AOnLimByByOnsucyOnAOn
60 oewordi yOnsucyOnAOnAysucyA𝑜yA𝑜sucy
61 59 60 sylan AOnLimByBAysucyA𝑜yA𝑜sucy
62 61 an32s AOnLimBAyBysucyA𝑜yA𝑜sucy
63 50 62 mpi AOnLimBAyBA𝑜yA𝑜sucy
64 63 ex AOnLimBAyBA𝑜yA𝑜sucy
65 49 64 jcad AOnLimBAyBsucyB1𝑜A𝑜yA𝑜sucy
66 oveq2 x=sucyA𝑜x=A𝑜sucy
67 66 sseq2d x=sucyA𝑜yA𝑜xA𝑜yA𝑜sucy
68 67 rspcev sucyB1𝑜A𝑜yA𝑜sucyxB1𝑜A𝑜yA𝑜x
69 65 68 syl6 AOnLimBAyBxB1𝑜A𝑜yA𝑜x
70 69 ralrimiv AOnLimBAyBxB1𝑜A𝑜yA𝑜x
71 iunss2 yBxB1𝑜A𝑜yA𝑜xyBA𝑜yxB1𝑜A𝑜x
72 70 71 syl AOnLimBAyBA𝑜yxB1𝑜A𝑜x
73 difss B1𝑜B
74 iunss1 B1𝑜BxB1𝑜A𝑜xxBA𝑜x
75 73 74 ax-mp xB1𝑜A𝑜xxBA𝑜x
76 oveq2 x=yA𝑜x=A𝑜y
77 76 cbviunv xBA𝑜x=yBA𝑜y
78 75 77 sseqtri xB1𝑜A𝑜xyBA𝑜y
79 78 a1i AOnLimBAxB1𝑜A𝑜xyBA𝑜y
80 72 79 eqssd AOnLimBAyBA𝑜y=xB1𝑜A𝑜x
81 80 adantlrl AOnBCLimBAyBA𝑜y=xB1𝑜A𝑜x
82 42 81 eqtrd AOnBCLimBAA𝑜B=xB1𝑜A𝑜x
83 41 82 oe0lem AOnBCLimBA𝑜B=xB1𝑜A𝑜x