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 e. V /\ Lim A ) -> ( aleph ` A ) = U_ x e. A ( aleph ` x ) )

Proof

Step Hyp Ref Expression
1 rdglim2a 
 |-  ( ( A e. V /\ Lim A ) -> ( rec ( har , _om ) ` A ) = U_ x e. A ( rec ( har , _om ) ` x ) )
2 df-aleph 
 |-  aleph = rec ( har , _om )
3 2 fveq1i 
 |-  ( aleph ` A ) = ( rec ( har , _om ) ` A )
4 2 fveq1i 
 |-  ( aleph ` x ) = ( rec ( har , _om ) ` x )
5 4 a1i 
 |-  ( x e. A -> ( aleph ` x ) = ( rec ( har , _om ) ` x ) )
6 5 iuneq2i 
 |-  U_ x e. A ( aleph ` x ) = U_ x e. A ( rec ( har , _om ) ` x )
7 1 3 6 3eqtr4g 
 |-  ( ( A e. V /\ Lim A ) -> ( aleph ` A ) = U_ x e. A ( aleph ` x ) )