Metamath Proof Explorer


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 )