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\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		rdgfnon	$$⊢\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)Fn\mathrm{On}$$
2		df-aleph	$$⊢\aleph =\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)$$
3	2	fneq1i	$$⊢\aleph Fn\mathrm{On}\leftrightarrow \mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)Fn\mathrm{On}$$
4	1 3	mpbir	$$⊢\aleph Fn\mathrm{On}$$