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	⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) = ( har ‘ ( ℵ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rdgsuc	⊢ ( 𝐴 ∈ On → ( rec ( har , ω ) ‘ suc 𝐴 ) = ( har ‘ ( rec ( har , ω ) ‘ 𝐴 ) ) )
2		df-aleph	⊢ ℵ = rec ( har , ω )
3	2	fveq1i	⊢ ( ℵ ‘ suc 𝐴 ) = ( rec ( har , ω ) ‘ suc 𝐴 )
4	2	fveq1i	⊢ ( ℵ ‘ 𝐴 ) = ( rec ( har , ω ) ‘ 𝐴 )
5	4	fveq2i	⊢ ( har ‘ ( ℵ ‘ 𝐴 ) ) = ( har ‘ ( rec ( har , ω ) ‘ 𝐴 ) )
6	1 3 5	3eqtr4g	⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) = ( har ‘ ( ℵ ‘ 𝐴 ) ) )