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