Metamath Proof Explorer

Theorem oe1m

Description: Ordinal exponentiation with a mantissa 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 )