Metamath Proof Explorer

Theorem fnoa

Description: Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion fnoa 
|- +o Fn ( On X. On )

Proof

Step Hyp Ref Expression
1 df-oadd 
 |-  +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
2 fvex 
 |-  ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) e. _V
3 1 2 fnmpoi 
 |-  +o Fn ( On X. On )