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 ( 𝐴 ∈ On → ( 1oo 𝐴 ) = 1o )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑥 = ∅ → ( 1oo 𝑥 ) = ( 1oo ∅ ) )
2 1 eqeq1d ( 𝑥 = ∅ → ( ( 1oo 𝑥 ) = 1o ↔ ( 1oo ∅ ) = 1o ) )
3 oveq2 ( 𝑥 = 𝑦 → ( 1oo 𝑥 ) = ( 1oo 𝑦 ) )
4 3 eqeq1d ( 𝑥 = 𝑦 → ( ( 1oo 𝑥 ) = 1o ↔ ( 1oo 𝑦 ) = 1o ) )
5 oveq2 ( 𝑥 = suc 𝑦 → ( 1oo 𝑥 ) = ( 1oo suc 𝑦 ) )
6 5 eqeq1d ( 𝑥 = suc 𝑦 → ( ( 1oo 𝑥 ) = 1o ↔ ( 1oo suc 𝑦 ) = 1o ) )
7 oveq2 ( 𝑥 = 𝐴 → ( 1oo 𝑥 ) = ( 1oo 𝐴 ) )
8 7 eqeq1d ( 𝑥 = 𝐴 → ( ( 1oo 𝑥 ) = 1o ↔ ( 1oo 𝐴 ) = 1o ) )
9 1on 1o ∈ On
10 oe0 ( 1o ∈ On → ( 1oo ∅ ) = 1o )
11 9 10 ax-mp ( 1oo ∅ ) = 1o
12 oesuc ( ( 1o ∈ On ∧ 𝑦 ∈ On ) → ( 1oo suc 𝑦 ) = ( ( 1oo 𝑦 ) ·o 1o ) )
13 9 12 mpan ( 𝑦 ∈ On → ( 1oo suc 𝑦 ) = ( ( 1oo 𝑦 ) ·o 1o ) )
14 oveq1 ( ( 1oo 𝑦 ) = 1o → ( ( 1oo 𝑦 ) ·o 1o ) = ( 1o ·o 1o ) )
15 om1 ( 1o ∈ On → ( 1o ·o 1o ) = 1o )
16 9 15 ax-mp ( 1o ·o 1o ) = 1o
17 14 16 eqtrdi ( ( 1oo 𝑦 ) = 1o → ( ( 1oo 𝑦 ) ·o 1o ) = 1o )
18 13 17 sylan9eq ( ( 𝑦 ∈ On ∧ ( 1oo 𝑦 ) = 1o ) → ( 1oo suc 𝑦 ) = 1o )
19 18 ex ( 𝑦 ∈ On → ( ( 1oo 𝑦 ) = 1o → ( 1oo suc 𝑦 ) = 1o ) )
20 iuneq2 ( ∀ 𝑦𝑥 ( 1oo 𝑦 ) = 1o 𝑦𝑥 ( 1oo 𝑦 ) = 𝑦𝑥 1o )
21 vex 𝑥 ∈ V
22 0lt1o ∅ ∈ 1o
23 oelim ( ( ( 1o ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 1o ) → ( 1oo 𝑥 ) = 𝑦𝑥 ( 1oo 𝑦 ) )
24 22 23 mpan2 ( ( 1o ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 1oo 𝑥 ) = 𝑦𝑥 ( 1oo 𝑦 ) )
25 9 24 mpan ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( 1oo 𝑥 ) = 𝑦𝑥 ( 1oo 𝑦 ) )
26 21 25 mpan ( Lim 𝑥 → ( 1oo 𝑥 ) = 𝑦𝑥 ( 1oo 𝑦 ) )
27 26 eqeq1d ( Lim 𝑥 → ( ( 1oo 𝑥 ) = 1o 𝑦𝑥 ( 1oo 𝑦 ) = 1o ) )
28 0ellim ( Lim 𝑥 → ∅ ∈ 𝑥 )
29 ne0i ( ∅ ∈ 𝑥𝑥 ≠ ∅ )
30 iunconst ( 𝑥 ≠ ∅ → 𝑦𝑥 1o = 1o )
31 28 29 30 3syl ( Lim 𝑥 𝑦𝑥 1o = 1o )
32 31 eqeq2d ( Lim 𝑥 → ( 𝑦𝑥 ( 1oo 𝑦 ) = 𝑦𝑥 1o 𝑦𝑥 ( 1oo 𝑦 ) = 1o ) )
33 27 32 bitr4d ( Lim 𝑥 → ( ( 1oo 𝑥 ) = 1o 𝑦𝑥 ( 1oo 𝑦 ) = 𝑦𝑥 1o ) )
34 20 33 syl5ibr ( Lim 𝑥 → ( ∀ 𝑦𝑥 ( 1oo 𝑦 ) = 1o → ( 1oo 𝑥 ) = 1o ) )
35 2 4 6 8 11 19 34 tfinds ( 𝐴 ∈ On → ( 1oo 𝐴 ) = 1o )