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∈dom⁡rec⁡FA→rec⁡FA↾B∈V

Proof

Step Hyp Ref Expression
1 df-rdg ⊢rec⁡FA=recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
2 1 reseq1i ⊢rec⁡FA↾B=recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g↾B
3 rdglem1 ⊢w|∃y∈OnwFny∧∀v∈yw⁡v=g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡w↾v=f|∃x∈OnfFnx∧∀y∈xf⁡y=g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y
4 3 tfrlem9a ⊢B∈dom⁡recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g→recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g↾B∈V
5 1 dmeqi ⊢dom⁡rec⁡FA=dom⁡recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
6 4 5 eleq2s ⊢B∈dom⁡rec⁡FA→recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g↾B∈V
7 2 6 eqeltrid ⊢B∈dom⁡rec⁡FA→rec⁡FA↾B∈V