Description: Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fnoe | |- ^o Fn ( On X. On ) |
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 ) |