Metamath Proof Explorer

Theorem dfrdg3

Description: Generalization of dfrdg2 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dfrdg3 ⊢rec⁡FI=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y

Proof

Step Hyp Ref Expression
1 dfrdg2 ⊢I∈V→rec⁡FI=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
2 iftrue ⊢I∈V→ifI∈VI∅=I
3 2 ifeq1d ⊢I∈V→ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
4 3 eqeq2d ⊢I∈V→f⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y↔f⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
5 4 ralbidv ⊢I∈V→∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y↔∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
6 5 anbi2d ⊢I∈V→fFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y↔fFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
7 6 rexbidv ⊢I∈V→∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y↔∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
8 7 abbidv ⊢I∈V→f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y=f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
9 8 unieqd ⊢I∈V→⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
10 1 9 eqtr4d ⊢I∈V→rec⁡FI=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y
11 0ex ⊢∅∈V
12 dfrdg2 ⊢∅∈V→rec⁡F∅=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅∅ifLim⁡y⋃fyF⁡f⁡⋃y
13 11 12 ax-mp ⊢rec⁡F∅=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅∅ifLim⁡y⋃fyF⁡f⁡⋃y
14 rdgprc ⊢¬I∈V→rec⁡FI=rec⁡F∅
15 iffalse ⊢¬I∈V→ifI∈VI∅=∅
16 15 ifeq1d ⊢¬I∈V→ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y=ify=∅∅ifLim⁡y⋃fyF⁡f⁡⋃y
17 16 eqeq2d ⊢¬I∈V→f⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y↔f⁡y=ify=∅∅ifLim⁡y⋃fyF⁡f⁡⋃y
18 17 ralbidv ⊢¬I∈V→∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y↔∀y∈xf⁡y=ify=∅∅ifLim⁡y⋃fyF⁡f⁡⋃y
19 18 anbi2d ⊢¬I∈V→fFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y↔fFnx∧∀y∈xf⁡y=ify=∅∅ifLim⁡y⋃fyF⁡f⁡⋃y
20 19 rexbidv ⊢¬I∈V→∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y↔∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅∅ifLim⁡y⋃fyF⁡f⁡⋃y
21 20 abbidv ⊢¬I∈V→f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y=f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅∅ifLim⁡y⋃fyF⁡f⁡⋃y
22 21 unieqd ⊢¬I∈V→⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅∅ifLim⁡y⋃fyF⁡f⁡⋃y
23 13 14 22 3eqtr4a ⊢¬I∈V→rec⁡FI=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y
24 10 23 pm2.61i ⊢rec⁡FI=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅ifI∈VI∅ifLim⁡y⋃fyF⁡f⁡⋃y