Metamath Proof Explorer

Theorem rdgprc0

Description: The value of the recursive definition generator at (/) when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion rdgprc0 ⊢¬I∈V→rec⁡FI⁡∅=∅

Proof

Step Hyp Ref Expression
1 0elon ⊢∅∈On
2 rdgval ⊢∅∈On→rec⁡FI⁡∅=g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡rec⁡FI↾∅
3 1 2 ax-mp ⊢rec⁡FI⁡∅=g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡rec⁡FI↾∅
4 res0 ⊢rec⁡FI↾∅=∅
5 4 fveq2i ⊢g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡rec⁡FI↾∅=g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡∅
6 3 5 eqtri ⊢rec⁡FI⁡∅=g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡∅
7 eqeq1 ⊢g=∅→g=∅↔∅=∅
8 dmeq ⊢g=∅→dom⁡g=dom⁡∅
9 limeq ⊢dom⁡g=dom⁡∅→Lim⁡dom⁡g↔Lim⁡dom⁡∅
10 8 9 syl ⊢g=∅→Lim⁡dom⁡g↔Lim⁡dom⁡∅
11 rneq ⊢g=∅→ran⁡g=ran⁡∅
12 11 unieqd ⊢g=∅→⋃ran⁡g=⋃ran⁡∅
13 id ⊢g=∅→g=∅
14 8 unieqd ⊢g=∅→⋃dom⁡g=⋃dom⁡∅
15 13 14 fveq12d ⊢g=∅→g⁡⋃dom⁡g=∅⁡⋃dom⁡∅
16 15 fveq2d ⊢g=∅→F⁡g⁡⋃dom⁡g=F⁡∅⁡⋃dom⁡∅
17 10 12 16 ifbieq12d ⊢g=∅→ifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=ifLim⁡dom⁡∅⋃ran⁡∅F⁡∅⁡⋃dom⁡∅
18 7 17 ifbieq2d ⊢g=∅→ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=if∅=∅IifLim⁡dom⁡∅⋃ran⁡∅F⁡∅⁡⋃dom⁡∅
19 18 eleq1d ⊢g=∅→ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g∈V↔if∅=∅IifLim⁡dom⁡∅⋃ran⁡∅F⁡∅⁡⋃dom⁡∅∈V
20 eqid ⊢g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
21 20 dmmpt ⊢dom⁡g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=g∈V|ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g∈V
22 19 21 elrab2 ⊢∅∈dom⁡g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g↔∅∈V∧if∅=∅IifLim⁡dom⁡∅⋃ran⁡∅F⁡∅⁡⋃dom⁡∅∈V
23 eqid ⊢∅=∅
24 23 iftruei ⊢if∅=∅IifLim⁡dom⁡∅⋃ran⁡∅F⁡∅⁡⋃dom⁡∅=I
25 24 eleq1i ⊢if∅=∅IifLim⁡dom⁡∅⋃ran⁡∅F⁡∅⁡⋃dom⁡∅∈V↔I∈V
26 25 biimpi ⊢if∅=∅IifLim⁡dom⁡∅⋃ran⁡∅F⁡∅⁡⋃dom⁡∅∈V→I∈V
27 22 26 simplbiim ⊢∅∈dom⁡g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g→I∈V
28 ndmfv ⊢¬∅∈dom⁡g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g→g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡∅=∅
29 27 28 nsyl5 ⊢¬I∈V→g∈V⟼ifg=∅IifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡∅=∅
30 6 29 eqtrid ⊢¬I∈V→rec⁡FI⁡∅=∅