# Metamath Proof Explorer

## 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)$