Theorem alephlim

Description: Value of the aleph function at a limit ordinal. Definition 12(iii) of Suppes p. 91. (Contributed by NM, 21-Oct-2003) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Assertion	alephlim	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( ℵ ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		rdglim2a	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ( rec ( har , ω ) ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( rec ( har , ω ) ‘ 𝑥 ) )
2		df-aleph	⊢ ℵ = rec ( har , ω )
3	2	fveq1i	⊢ ( ℵ ‘ 𝐴 ) = ( rec ( har , ω ) ‘ 𝐴 )
4	2	fveq1i	⊢ ( ℵ ‘ 𝑥 ) = ( rec ( har , ω ) ‘ 𝑥 )
5	4	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( ℵ ‘ 𝑥 ) = ( rec ( har , ω ) ‘ 𝑥 ) )
6	5	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 ( ℵ ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝐴 ( rec ( har , ω ) ‘ 𝑥 )
7	1 3 6	3eqtr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( ℵ ‘ 𝑥 ) )