Metamath Proof Explorer


Theorem oeworde

Description: Ordinal exponentiation compared to its exponent. Proposition 8.37 of TakeutiZaring p. 68. (Contributed by NM, 7-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oeworde A On 2 𝑜 B On B A 𝑜 B

Proof

Step Hyp Ref Expression
1 id x = x =
2 oveq2 x = A 𝑜 x = A 𝑜
3 1 2 sseq12d x = x A 𝑜 x A 𝑜
4 id x = y x = y
5 oveq2 x = y A 𝑜 x = A 𝑜 y
6 4 5 sseq12d x = y x A 𝑜 x y A 𝑜 y
7 id x = suc y x = suc y
8 oveq2 x = suc y A 𝑜 x = A 𝑜 suc y
9 7 8 sseq12d x = suc y x A 𝑜 x suc y A 𝑜 suc y
10 id x = B x = B
11 oveq2 x = B A 𝑜 x = A 𝑜 B
12 10 11 sseq12d x = B x A 𝑜 x B A 𝑜 B
13 0ss A 𝑜
14 13 a1i A On 2 𝑜 A 𝑜
15 eloni y On Ord y
16 eldifi A On 2 𝑜 A On
17 oecl A On y On A 𝑜 y On
18 16 17 sylan A On 2 𝑜 y On A 𝑜 y On
19 eloni A 𝑜 y On Ord A 𝑜 y
20 18 19 syl A On 2 𝑜 y On Ord A 𝑜 y
21 ordsucsssuc Ord y Ord A 𝑜 y y A 𝑜 y suc y suc A 𝑜 y
22 15 20 21 syl2an2 A On 2 𝑜 y On y A 𝑜 y suc y suc A 𝑜 y
23 suceloni y On suc y On
24 oecl A On suc y On A 𝑜 suc y On
25 16 23 24 syl2an A On 2 𝑜 y On A 𝑜 suc y On
26 eloni A 𝑜 suc y On Ord A 𝑜 suc y
27 25 26 syl A On 2 𝑜 y On Ord A 𝑜 suc y
28 id A On 2 𝑜 A On 2 𝑜
29 vex y V
30 29 sucid y suc y
31 oeordi suc y On A On 2 𝑜 y suc y A 𝑜 y A 𝑜 suc y
32 30 31 mpi suc y On A On 2 𝑜 A 𝑜 y A 𝑜 suc y
33 23 28 32 syl2anr A On 2 𝑜 y On A 𝑜 y A 𝑜 suc y
34 ordsucss Ord A 𝑜 suc y A 𝑜 y A 𝑜 suc y suc A 𝑜 y A 𝑜 suc y
35 27 33 34 sylc A On 2 𝑜 y On suc A 𝑜 y A 𝑜 suc y
36 sstr2 suc y suc A 𝑜 y suc A 𝑜 y A 𝑜 suc y suc y A 𝑜 suc y
37 35 36 syl5com A On 2 𝑜 y On suc y suc A 𝑜 y suc y A 𝑜 suc y
38 22 37 sylbid A On 2 𝑜 y On y A 𝑜 y suc y A 𝑜 suc y
39 38 expcom y On A On 2 𝑜 y A 𝑜 y suc y A 𝑜 suc y
40 dif20el A On 2 𝑜 A
41 16 40 jca A On 2 𝑜 A On A
42 ss2iun y x y A 𝑜 y y x y y x A 𝑜 y
43 limuni Lim x x = x
44 uniiun x = y x y
45 43 44 syl6eq Lim x x = y x y
46 45 adantr Lim x A On A x = y x y
47 vex x V
48 oelim A On x V Lim x A A 𝑜 x = y x A 𝑜 y
49 47 48 mpanlr1 A On Lim x A A 𝑜 x = y x A 𝑜 y
50 49 anasss A On Lim x A A 𝑜 x = y x A 𝑜 y
51 50 an12s Lim x A On A A 𝑜 x = y x A 𝑜 y
52 46 51 sseq12d Lim x A On A x A 𝑜 x y x y y x A 𝑜 y
53 42 52 syl5ibr Lim x A On A y x y A 𝑜 y x A 𝑜 x
54 53 ex Lim x A On A y x y A 𝑜 y x A 𝑜 x
55 41 54 syl5 Lim x A On 2 𝑜 y x y A 𝑜 y x A 𝑜 x
56 3 6 9 12 14 39 55 tfinds3 B On A On 2 𝑜 B A 𝑜 B
57 56 impcom A On 2 𝑜 B On B A 𝑜 B