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 e. On -> ( 1o ^o A ) = 1o )

Proof

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