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 |
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 |