Metamath Proof Explorer


Theorem alephfnon

Description: The aleph function is a function on the class of ordinal numbers. (Contributed by NM, 21-Oct-2003) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Assertion alephfnon
|- aleph Fn On

Proof

Step Hyp Ref Expression
1 rdgfnon
 |-  rec ( har , _om ) Fn On
2 df-aleph
 |-  aleph = rec ( har , _om )
3 2 fneq1i
 |-  ( aleph Fn On <-> rec ( har , _om ) Fn On )
4 1 3 mpbir
 |-  aleph Fn On