Metamath Proof Explorer

Theorem rdgseg

Description: The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion rdgseg 
|- ( B e. dom rec ( F , A ) -> ( rec ( F , A ) |` B ) e. _V )

Proof

Step Hyp Ref Expression
1 df-rdg 
 |-  rec ( F , A ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
2 1 reseq1i 
 |-  ( rec ( F , A ) |` B ) = ( recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) |` B )
3 rdglem1 
 |-  { w | E. y e. On ( w Fn y /\ A. v e. y ( w ` v ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( w |` v ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) ) }
4 3 tfrlem9a 
 |-  ( B e. dom recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) -> ( recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) |` B ) e. _V )
5 1 dmeqi 
 |-  dom rec ( F , A ) = dom recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
6 4 5 eleq2s 
 |-  ( B e. dom rec ( F , A ) -> ( recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) |` B ) e. _V )
7 2 6 eqeltrid 
 |-  ( B e. dom rec ( F , A ) -> ( rec ( F , A ) |` B ) e. _V )