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	⊢ ℵ Fn On

Proof

Step	Hyp	Ref	Expression
1		rdgfnon	⊢ rec ( har , ω ) Fn On
2		df-aleph	⊢ ℵ = rec ( har , ω )
3	2	fneq1i	⊢ ( ℵ Fn On ↔ rec ( har , ω ) Fn On )
4	1 3	mpbir	⊢ ℵ Fn On