This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A = ⋃ x ∈ A ℵ ⁡ x

Proof

Step Hyp Ref Expression
1 rdglim2a ⊢ A ∈ V ∧ Lim ⁡ A → rec ⁡ har ω ⁡ A = ⋃ x ∈ A rec ⁡ har ω ⁡ x
2 df-aleph ⊢ ℵ = rec ⁡ har ω
3 2 fveq1i ⊢ ℵ ⁡ A = rec ⁡ har ω ⁡ A
4 2 fveq1i ⊢ ℵ ⁡ x = rec ⁡ har ω ⁡ x
5 4 a1i ⊢ x ∈ A → ℵ ⁡ x = rec ⁡ har ω ⁡ x
6 5 iuneq2i ⊢ ⋃ x ∈ A ℵ ⁡ x = ⋃ x ∈ A rec ⁡ har ω ⁡ x
7 1 3 6 3eqtr4g ⊢ A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A = ⋃ x ∈ A ℵ ⁡ x