Description: Value of the aleph function at a successor ordinal. Definition 12(ii) of Suppes p. 91. Here we express the successor aleph in terms of the Hartogs function df-har , which gives the smallest ordinal that strictly dominates its argument (or the supremum of all ordinals that are dominated by the argument). (Contributed by Mario Carneiro, 13-Sep-2013) (Revised by Mario Carneiro, 15-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | alephsuc | |- ( A e. On -> ( aleph ` suc A ) = ( har ` ( aleph ` A ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rdgsuc | |- ( A e. On -> ( rec ( har , _om ) ` suc A ) = ( har ` ( rec ( har , _om ) ` A ) ) ) |
|
| 2 | df-aleph | |- aleph = rec ( har , _om ) |
|
| 3 | 2 | fveq1i | |- ( aleph ` suc A ) = ( rec ( har , _om ) ` suc A ) |
| 4 | 2 | fveq1i | |- ( aleph ` A ) = ( rec ( har , _om ) ` A ) |
| 5 | 4 | fveq2i | |- ( har ` ( aleph ` A ) ) = ( har ` ( rec ( har , _om ) ` A ) ) |
| 6 | 1 3 5 | 3eqtr4g | |- ( A e. On -> ( aleph ` suc A ) = ( har ` ( aleph ` A ) ) ) |