This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )