Metamath Proof Explorer


Theorem oev

Description: Value of ordinal exponentiation. (Contributed by NM, 30-Dec-2004) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion oev
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) = if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1
 |-  ( y = A -> ( y = (/) <-> A = (/) ) )
2 oveq2
 |-  ( y = A -> ( x .o y ) = ( x .o A ) )
3 2 mpteq2dv
 |-  ( y = A -> ( x e. _V |-> ( x .o y ) ) = ( x e. _V |-> ( x .o A ) ) )
4 rdgeq1
 |-  ( ( x e. _V |-> ( x .o y ) ) = ( x e. _V |-> ( x .o A ) ) -> rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) = rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) )
5 3 4 syl
 |-  ( y = A -> rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) = rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) )
6 5 fveq1d
 |-  ( y = A -> ( rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) ` z ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` z ) )
7 1 6 ifbieq2d
 |-  ( y = A -> if ( y = (/) , ( 1o \ z ) , ( rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) ` z ) ) = if ( A = (/) , ( 1o \ z ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` z ) ) )
8 difeq2
 |-  ( z = B -> ( 1o \ z ) = ( 1o \ B ) )
9 fveq2
 |-  ( z = B -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` z ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )
10 8 9 ifeq12d
 |-  ( z = B -> if ( A = (/) , ( 1o \ z ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` z ) ) = if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
11 df-oexp
 |-  ^o = ( y e. On , z e. On |-> if ( y = (/) , ( 1o \ z ) , ( rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) ` z ) ) )
12 1oex
 |-  1o e. _V
13 12 difexi
 |-  ( 1o \ B ) e. _V
14 fvex
 |-  ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) e. _V
15 13 14 ifex
 |-  if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) e. _V
16 7 10 11 15 ovmpo
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) = if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )