Metamath Proof Explorer

Theorem rdgellim

Description: Elementhood in a recursive definition at a limit ordinal. (Contributed by ML, 30-Mar-2022)

Ref Expression
Assertion rdgellim 
|- ( ( ( B e. On /\ Lim B ) /\ C e. B ) -> ( X e. ( rec ( F , A ) ` C ) -> X e. ( rec ( F , A ) ` B ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( y = C -> ( rec ( F , A ) ` y ) = ( rec ( F , A ) ` C ) )
2 1 eleq2d 
 |-  ( y = C -> ( X e. ( rec ( F , A ) ` y ) <-> X e. ( rec ( F , A ) ` C ) ) )
3 2 rspcev 
 |-  ( ( C e. B /\ X e. ( rec ( F , A ) ` C ) ) -> E. y e. B X e. ( rec ( F , A ) ` y ) )
4 3 ex 
 |-  ( C e. B -> ( X e. ( rec ( F , A ) ` C ) -> E. y e. B X e. ( rec ( F , A ) ` y ) ) )
5 eliun 
 |-  ( X e. U_ y e. B ( rec ( F , A ) ` y ) <-> E. y e. B X e. ( rec ( F , A ) ` y ) )
6 4 5 syl6ibr 
 |-  ( C e. B -> ( X e. ( rec ( F , A ) ` C ) -> X e. U_ y e. B ( rec ( F , A ) ` y ) ) )
7 6 adantl 
 |-  ( ( ( B e. On /\ Lim B ) /\ C e. B ) -> ( X e. ( rec ( F , A ) ` C ) -> X e. U_ y e. B ( rec ( F , A ) ` y ) ) )
8 rdglim2a 
 |-  ( ( B e. On /\ Lim B ) -> ( rec ( F , A ) ` B ) = U_ y e. B ( rec ( F , A ) ` y ) )
9 8 eleq2d 
 |-  ( ( B e. On /\ Lim B ) -> ( X e. ( rec ( F , A ) ` B ) <-> X e. U_ y e. B ( rec ( F , A ) ` y ) ) )
10 9 adantr 
 |-  ( ( ( B e. On /\ Lim B ) /\ C e. B ) -> ( X e. ( rec ( F , A ) ` B ) <-> X e. U_ y e. B ( rec ( F , A ) ` y ) ) )
11 7 10 sylibrd 
 |-  ( ( ( B e. On /\ Lim B ) /\ C e. B ) -> ( X e. ( rec ( F , A ) ` C ) -> X e. ( rec ( F , A ) ` B ) ) )