Theorem rdgseg

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

	Ref	Expression
Assertion	rdgseg	⊢ ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ↾ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-rdg	⊢ rec ( 𝐹 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
2	1	reseq1i	⊢ ( rec ( 𝐹 , 𝐴 ) ↾ 𝐵 ) = ( recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) ↾ 𝐵 )
3		rdglem1	⊢ { 𝑤 ∣ ∃ 𝑦 ∈ On ( 𝑤 Fn 𝑦 ∧ ∀ 𝑣 ∈ 𝑦 ( 𝑤 ‘ 𝑣 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑤 ↾ 𝑣 ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
4	3	tfrlem9a	⊢ ( 𝐵 ∈ dom recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) → ( recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) ↾ 𝐵 ) ∈ V )
5	1	dmeqi	⊢ dom rec ( 𝐹 , 𝐴 ) = dom recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
6	4 5	eleq2s	⊢ ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) ↾ 𝐵 ) ∈ V )
7	2 6	eqeltrid	⊢ ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ↾ 𝐵 ) ∈ V )