Description: Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 8-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | fnom | |- .o Fn ( On X. On ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-omul | |- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) ) |
|
2 | fvex | |- ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) e. _V |
|
3 | 1 2 | fnmpoi | |- .o Fn ( On X. On ) |