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	$$⊢\left(A\in V\wedge \mathrm{Lim}A\right)\to \aleph \left(A\right)=\bigcup _{x\in A}\aleph \left(x\right)$$

Proof

Step	Hyp	Ref	Expression
1		rdglim2a	$$⊢\left(A\in V\wedge \mathrm{Lim}A\right)\to \mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(A\right)=\bigcup _{x\in A}\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(x\right)$$
2		df-aleph	$$⊢\aleph =\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)$$
3	2	fveq1i	$$⊢\aleph \left(A\right)=\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(A\right)$$
4	2	fveq1i	$$⊢\aleph \left(x\right)=\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(x\right)$$
5	4	a1i	$$⊢x\in A\to \aleph \left(x\right)=\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(x\right)$$
6	5	iuneq2i	$$⊢\bigcup _{x\in A}\aleph \left(x\right)=\bigcup _{x\in A}\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(x\right)$$
7	1 3 6	3eqtr4g	$$⊢\left(A\in V\wedge \mathrm{Lim}A\right)\to \aleph \left(A\right)=\bigcup _{x\in A}\aleph \left(x\right)$$