Theorem fnoe

Description: Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015)

	Ref	Expression
Assertion	fnoe	|- ^o Fn ( On X. On )

Proof

Step	Hyp	Ref	Expression
1		df-oexp	|- ^o = ( x e. On , y e. On |-> if ( x = (/) , ( 1o \ y ) , ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) ) )
2		1on	|- 1o e. On
3		difexg	|- ( 1o e. On -> ( 1o \ y ) e. _V )
4	2 3	ax-mp	|- ( 1o \ y ) e. _V
5		fvex	|- ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) e. _V
6	4 5	ifex	|- if ( x = (/) , ( 1o \ y ) , ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) ) e. _V
7	1 6	fnmpoi	|- ^o Fn ( On X. On )