Metamath Proof Explorer

Theorem fnom

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 )

Proof

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 )