Theorem alephsuc

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\in \mathrm{On}\to \aleph \left(\mathrm{suc}A\right)=\mathrm{har}\left(\aleph \left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rdgsuc	$$⊢A\in \mathrm{On}\to \mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(\mathrm{suc}A\right)=\mathrm{har}\left(\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(A\right)\right)$$
2		df-aleph	$$⊢\aleph =\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)$$
3	2	fveq1i	$$⊢\aleph \left(\mathrm{suc}A\right)=\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(\mathrm{suc}A\right)$$
4	2	fveq1i	$$⊢\aleph \left(A\right)=\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(A\right)$$
5	4	fveq2i	$$⊢\mathrm{har}\left(\aleph \left(A\right)\right)=\mathrm{har}\left(\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(A\right)\right)$$
6	1 3 5	3eqtr4g	$$⊢A\in \mathrm{On}\to \aleph \left(\mathrm{suc}A\right)=\mathrm{har}\left(\aleph \left(A\right)\right)$$