Metamath Proof Explorer

Theorem rdgeq1

Description: Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion rdgeq1 ⊢F=G→rec⁡FA=rec⁡GA

Proof

Step Hyp Ref Expression
1 fveq1 ⊢F=G→F⁡g⁡⋃dom⁡g=G⁡g⁡⋃dom⁡g
2 1 ifeq2d ⊢F=G→ifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=ifLim⁡dom⁡g⋃ran⁡gG⁡g⁡⋃dom⁡g
3 2 ifeq2d ⊢F=G→ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=ifg=∅AifLim⁡dom⁡g⋃ran⁡gG⁡g⁡⋃dom⁡g
4 3 mpteq2dv ⊢F=G→g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gG⁡g⁡⋃dom⁡g
5 recseq ⊢g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gG⁡g⁡⋃dom⁡g→recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gG⁡g⁡⋃dom⁡g
6 4 5 syl ⊢F=G→recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gG⁡g⁡⋃dom⁡g
7 df-rdg ⊢rec⁡FA=recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
8 df-rdg ⊢rec⁡GA=recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gG⁡g⁡⋃dom⁡g
9 6 7 8 3eqtr4g ⊢F=G→rec⁡FA=rec⁡GA