Metamath Proof Explorer

Theorem oelim

Description: Ordinal exponentiation with a limit exponent and nonzero base. Definition 8.30 of TakeutiZaring p. 67. (Contributed by NM, 1-Jan-2005) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oelim 
|- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ x e. B ( A ^o x ) )

Proof

Step Hyp Ref Expression
1 limelon 
 |-  ( ( B e. C /\ Lim B ) -> B e. On )
2 simpr 
 |-  ( ( B e. C /\ Lim B ) -> Lim B )
3 1 2 jca 
 |-  ( ( B e. C /\ Lim B ) -> ( B e. On /\ Lim B ) )
4 rdglim2a 
 |-  ( ( B e. On /\ Lim B ) -> ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) )
5 4 ad2antlr 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ (/) e. A ) -> ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) )
6 oevn0 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( A ^o B ) = ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` B ) )
7 onelon 
 |-  ( ( B e. On /\ x e. B ) -> x e. On )
8 oevn0 
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( A ^o x ) = ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) )
9 7 8 sylanl2 
 |-  ( ( ( A e. On /\ ( B e. On /\ x e. B ) ) /\ (/) e. A ) -> ( A ^o x ) = ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) )
10 9 exp42 
 |-  ( A e. On -> ( B e. On -> ( x e. B -> ( (/) e. A -> ( A ^o x ) = ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) ) ) ) )
11 10 com34 
 |-  ( A e. On -> ( B e. On -> ( (/) e. A -> ( x e. B -> ( A ^o x ) = ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) ) ) ) )
12 11 imp41 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) /\ x e. B ) -> ( A ^o x ) = ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) )
13 12 iuneq2dv 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> U_ x e. B ( A ^o x ) = U_ x e. B ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) )
14 6 13 eqeq12d 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( ( A ^o B ) = U_ x e. B ( A ^o x ) <-> ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) ) )
15 14 adantlrr 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ (/) e. A ) -> ( ( A ^o B ) = U_ x e. B ( A ^o x ) <-> ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> ( y .o A ) ) , 1o ) ` x ) ) )
16 5 15 mpbird 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ x e. B ( A ^o x ) )
17 3 16 sylanl2 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ x e. B ( A ^o x ) )