Metamath Proof Explorer


Theorem oe1m

Description: Ordinal exponentiation with a base of 1. Proposition 8.31(3) of TakeutiZaring p. 67. (Contributed by NM, 2-Jan-2005)

Ref Expression
Assertion oe1m A On 1 𝑜 𝑜 A = 1 𝑜

Proof

Step Hyp Ref Expression
1 oveq2 x = 1 𝑜 𝑜 x = 1 𝑜 𝑜
2 1 eqeq1d x = 1 𝑜 𝑜 x = 1 𝑜 1 𝑜 𝑜 = 1 𝑜
3 oveq2 x = y 1 𝑜 𝑜 x = 1 𝑜 𝑜 y
4 3 eqeq1d x = y 1 𝑜 𝑜 x = 1 𝑜 1 𝑜 𝑜 y = 1 𝑜
5 oveq2 x = suc y 1 𝑜 𝑜 x = 1 𝑜 𝑜 suc y
6 5 eqeq1d x = suc y 1 𝑜 𝑜 x = 1 𝑜 1 𝑜 𝑜 suc y = 1 𝑜
7 oveq2 x = A 1 𝑜 𝑜 x = 1 𝑜 𝑜 A
8 7 eqeq1d x = A 1 𝑜 𝑜 x = 1 𝑜 1 𝑜 𝑜 A = 1 𝑜
9 1on 1 𝑜 On
10 oe0 1 𝑜 On 1 𝑜 𝑜 = 1 𝑜
11 9 10 ax-mp 1 𝑜 𝑜 = 1 𝑜
12 oesuc 1 𝑜 On y On 1 𝑜 𝑜 suc y = 1 𝑜 𝑜 y 𝑜 1 𝑜
13 9 12 mpan y On 1 𝑜 𝑜 suc y = 1 𝑜 𝑜 y 𝑜 1 𝑜
14 oveq1 1 𝑜 𝑜 y = 1 𝑜 1 𝑜 𝑜 y 𝑜 1 𝑜 = 1 𝑜 𝑜 1 𝑜
15 om1 1 𝑜 On 1 𝑜 𝑜 1 𝑜 = 1 𝑜
16 9 15 ax-mp 1 𝑜 𝑜 1 𝑜 = 1 𝑜
17 14 16 eqtrdi 1 𝑜 𝑜 y = 1 𝑜 1 𝑜 𝑜 y 𝑜 1 𝑜 = 1 𝑜
18 13 17 sylan9eq y On 1 𝑜 𝑜 y = 1 𝑜 1 𝑜 𝑜 suc y = 1 𝑜
19 18 ex y On 1 𝑜 𝑜 y = 1 𝑜 1 𝑜 𝑜 suc y = 1 𝑜
20 iuneq2 y x 1 𝑜 𝑜 y = 1 𝑜 y x 1 𝑜 𝑜 y = y x 1 𝑜
21 vex x V
22 0lt1o 1 𝑜
23 oelim 1 𝑜 On x V Lim x 1 𝑜 1 𝑜 𝑜 x = y x 1 𝑜 𝑜 y
24 22 23 mpan2 1 𝑜 On x V Lim x 1 𝑜 𝑜 x = y x 1 𝑜 𝑜 y
25 9 24 mpan x V Lim x 1 𝑜 𝑜 x = y x 1 𝑜 𝑜 y
26 21 25 mpan Lim x 1 𝑜 𝑜 x = y x 1 𝑜 𝑜 y
27 26 eqeq1d Lim x 1 𝑜 𝑜 x = 1 𝑜 y x 1 𝑜 𝑜 y = 1 𝑜
28 0ellim Lim x x
29 ne0i x x
30 iunconst x y x 1 𝑜 = 1 𝑜
31 28 29 30 3syl Lim x y x 1 𝑜 = 1 𝑜
32 31 eqeq2d Lim x y x 1 𝑜 𝑜 y = y x 1 𝑜 y x 1 𝑜 𝑜 y = 1 𝑜
33 27 32 bitr4d Lim x 1 𝑜 𝑜 x = 1 𝑜 y x 1 𝑜 𝑜 y = y x 1 𝑜
34 20 33 syl5ibr Lim x y x 1 𝑜 𝑜 y = 1 𝑜 1 𝑜 𝑜 x = 1 𝑜
35 2 4 6 8 11 19 34 tfinds A On 1 𝑜 𝑜 A = 1 𝑜