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