Metamath Proof Explorer

Theorem dfrdg2

Description: Alternate definition of the recursive function generator when I is a set. (Contributed by Scott Fenton, 26-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dfrdg2 ⊢I∈V→rec⁡FI=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y

Proof

Step Hyp Ref Expression
1 rdgeq2 ⊢i=I→rec⁡Fi=rec⁡FI
2 ifeq1 ⊢i=I→ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
3 2 eqeq2d ⊢i=I→f⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y↔f⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
4 3 ralbidv ⊢i=I→∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y↔∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
5 4 anbi2d ⊢i=I→fFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y↔fFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
6 5 rexbidv ⊢i=I→∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y↔∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
7 6 abbidv ⊢i=I→f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y=f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
8 7 unieqd ⊢i=I→⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
9 1 8 eqeq12d ⊢i=I→rec⁡Fi=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y↔rec⁡FI=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y
10 df-rdg ⊢rec⁡Fi=recs⁡g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
11 dfrecs3 ⊢recs⁡g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y
12 vex ⊢f∈V
13 12 resex ⊢f↾y∈V
14 eqeq1 ⊢g=f↾y→g=∅↔f↾y=∅
15 relres ⊢Rel⁡f↾y
16 reldm0 ⊢Rel⁡f↾y→f↾y=∅↔dom⁡f↾y=∅
17 15 16 ax-mp ⊢f↾y=∅↔dom⁡f↾y=∅
18 14 17 bitrdi ⊢g=f↾y→g=∅↔dom⁡f↾y=∅
19 dmeq ⊢g=f↾y→dom⁡g=dom⁡f↾y
20 limeq ⊢dom⁡g=dom⁡f↾y→Lim⁡dom⁡g↔Lim⁡dom⁡f↾y
21 19 20 syl ⊢g=f↾y→Lim⁡dom⁡g↔Lim⁡dom⁡f↾y
22 rneq ⊢g=f↾y→ran⁡g=ran⁡f↾y
23 df-ima ⊢fy=ran⁡f↾y
24 22 23 eqtr4di ⊢g=f↾y→ran⁡g=fy
25 24 unieqd ⊢g=f↾y→⋃ran⁡g=⋃fy
26 id ⊢g=f↾y→g=f↾y
27 19 unieqd ⊢g=f↾y→⋃dom⁡g=⋃dom⁡f↾y
28 26 27 fveq12d ⊢g=f↾y→g⁡⋃dom⁡g=f↾y⁡⋃dom⁡f↾y
29 28 fveq2d ⊢g=f↾y→F⁡g⁡⋃dom⁡g=F⁡f↾y⁡⋃dom⁡f↾y
30 21 25 29 ifbieq12d ⊢g=f↾y→ifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=ifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y
31 18 30 ifbieq2d ⊢g=f↾y→ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=ifdom⁡f↾y=∅iifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y
32 eqid ⊢g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
33 vex ⊢i∈V
34 imaexg ⊢f∈V→fy∈V
35 12 34 ax-mp ⊢fy∈V
36 35 uniex ⊢⋃fy∈V
37 fvex ⊢F⁡f↾y⁡⋃dom⁡f↾y∈V
38 36 37 ifex ⊢ifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y∈V
39 33 38 ifex ⊢ifdom⁡f↾y=∅iifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y∈V
40 31 32 39 fvmpt ⊢f↾y∈V→g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y=ifdom⁡f↾y=∅iifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y
41 13 40 ax-mp ⊢g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y=ifdom⁡f↾y=∅iifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y
42 dmres ⊢dom⁡f↾y=y∩dom⁡f
43 onelss ⊢x∈On→y∈x→y⊆x
44 43 imp ⊢x∈On∧y∈x→y⊆x
45 44 3adant2 ⊢x∈On∧fFnx∧y∈x→y⊆x
46 fndm ⊢fFnx→dom⁡f=x
47 46 3ad2ant2 ⊢x∈On∧fFnx∧y∈x→dom⁡f=x
48 45 47 sseqtrrd ⊢x∈On∧fFnx∧y∈x→y⊆dom⁡f
49 df-ss ⊢y⊆dom⁡f↔y∩dom⁡f=y
50 48 49 sylib ⊢x∈On∧fFnx∧y∈x→y∩dom⁡f=y
51 42 50 eqtrid ⊢x∈On∧fFnx∧y∈x→dom⁡f↾y=y
52 eqeq1 ⊢dom⁡f↾y=y→dom⁡f↾y=∅↔y=∅
53 limeq ⊢dom⁡f↾y=y→Lim⁡dom⁡f↾y↔Lim⁡y
54 unieq ⊢dom⁡f↾y=y→⋃dom⁡f↾y=⋃y
55 54 fveq2d ⊢dom⁡f↾y=y→f↾y⁡⋃dom⁡f↾y=f↾y⁡⋃y
56 55 fveq2d ⊢dom⁡f↾y=y→F⁡f↾y⁡⋃dom⁡f↾y=F⁡f↾y⁡⋃y
57 53 56 ifbieq2d ⊢dom⁡f↾y=y→ifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y=ifLim⁡y⋃fyF⁡f↾y⁡⋃y
58 52 57 ifbieq2d ⊢dom⁡f↾y=y→ifdom⁡f↾y=∅iifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y=ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y
59 onelon ⊢x∈On∧y∈x→y∈On
60 eloni ⊢y∈On→Ord⁡y
61 59 60 syl ⊢x∈On∧y∈x→Ord⁡y
62 61 3adant2 ⊢x∈On∧fFnx∧y∈x→Ord⁡y
63 ordzsl ⊢Ord⁡y↔y=∅∨∃z∈Ony=suc⁡z∨Lim⁡y
64 iftrue ⊢y=∅→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=i
65 iftrue ⊢y=∅→ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y=i
66 64 65 eqtr4d ⊢y=∅→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
67 vex ⊢z∈V
68 67 sucid ⊢z∈suc⁡z
69 fvres ⊢z∈suc⁡z→f↾suc⁡z⁡z=f⁡z
70 68 69 ax-mp ⊢f↾suc⁡z⁡z=f⁡z
71 eloni ⊢z∈On→Ord⁡z
72 ordunisuc ⊢Ord⁡z→⋃suc⁡z=z
73 71 72 syl ⊢z∈On→⋃suc⁡z=z
74 73 fveq2d ⊢z∈On→f↾suc⁡z⁡⋃suc⁡z=f↾suc⁡z⁡z
75 73 fveq2d ⊢z∈On→f⁡⋃suc⁡z=f⁡z
76 70 74 75 3eqtr4a ⊢z∈On→f↾suc⁡z⁡⋃suc⁡z=f⁡⋃suc⁡z
77 76 fveq2d ⊢z∈On→F⁡f↾suc⁡z⁡⋃suc⁡z=F⁡f⁡⋃suc⁡z
78 nsuceq0 ⊢suc⁡z≠∅
79 78 neii ⊢¬suc⁡z=∅
80 79 iffalsei ⊢ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f↾suc⁡z⁡⋃suc⁡z=ifLim⁡suc⁡z⋃fyF⁡f↾suc⁡z⁡⋃suc⁡z
81 nlimsucg ⊢z∈V→¬Lim⁡suc⁡z
82 iffalse ⊢¬Lim⁡suc⁡z→ifLim⁡suc⁡z⋃fyF⁡f↾suc⁡z⁡⋃suc⁡z=F⁡f↾suc⁡z⁡⋃suc⁡z
83 67 81 82 mp2b ⊢ifLim⁡suc⁡z⋃fyF⁡f↾suc⁡z⁡⋃suc⁡z=F⁡f↾suc⁡z⁡⋃suc⁡z
84 80 83 eqtri ⊢ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f↾suc⁡z⁡⋃suc⁡z=F⁡f↾suc⁡z⁡⋃suc⁡z
85 79 iffalsei ⊢ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f⁡⋃suc⁡z=ifLim⁡suc⁡z⋃fyF⁡f⁡⋃suc⁡z
86 iffalse ⊢¬Lim⁡suc⁡z→ifLim⁡suc⁡z⋃fyF⁡f⁡⋃suc⁡z=F⁡f⁡⋃suc⁡z
87 67 81 86 mp2b ⊢ifLim⁡suc⁡z⋃fyF⁡f⁡⋃suc⁡z=F⁡f⁡⋃suc⁡z
88 85 87 eqtri ⊢ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f⁡⋃suc⁡z=F⁡f⁡⋃suc⁡z
89 77 84 88 3eqtr4g ⊢z∈On→ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f↾suc⁡z⁡⋃suc⁡z=ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f⁡⋃suc⁡z
90 eqeq1 ⊢y=suc⁡z→y=∅↔suc⁡z=∅
91 limeq ⊢y=suc⁡z→Lim⁡y↔Lim⁡suc⁡z
92 reseq2 ⊢y=suc⁡z→f↾y=f↾suc⁡z
93 unieq ⊢y=suc⁡z→⋃y=⋃suc⁡z
94 92 93 fveq12d ⊢y=suc⁡z→f↾y⁡⋃y=f↾suc⁡z⁡⋃suc⁡z
95 94 fveq2d ⊢y=suc⁡z→F⁡f↾y⁡⋃y=F⁡f↾suc⁡z⁡⋃suc⁡z
96 91 95 ifbieq2d ⊢y=suc⁡z→ifLim⁡y⋃fyF⁡f↾y⁡⋃y=ifLim⁡suc⁡z⋃fyF⁡f↾suc⁡z⁡⋃suc⁡z
97 90 96 ifbieq2d ⊢y=suc⁡z→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f↾suc⁡z⁡⋃suc⁡z
98 93 fveq2d ⊢y=suc⁡z→f⁡⋃y=f⁡⋃suc⁡z
99 98 fveq2d ⊢y=suc⁡z→F⁡f⁡⋃y=F⁡f⁡⋃suc⁡z
100 91 99 ifbieq2d ⊢y=suc⁡z→ifLim⁡y⋃fyF⁡f⁡⋃y=ifLim⁡suc⁡z⋃fyF⁡f⁡⋃suc⁡z
101 90 100 ifbieq2d ⊢y=suc⁡z→ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y=ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f⁡⋃suc⁡z
102 97 101 eqeq12d ⊢y=suc⁡z→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y↔ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f↾suc⁡z⁡⋃suc⁡z=ifsuc⁡z=∅iifLim⁡suc⁡z⋃fyF⁡f⁡⋃suc⁡z
103 89 102 syl5ibrcom ⊢z∈On→y=suc⁡z→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
104 103 rexlimiv ⊢∃z∈Ony=suc⁡z→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
105 iftrue ⊢Lim⁡y→ifLim⁡y⋃fyF⁡f↾y⁡⋃y=⋃fy
106 df-lim ⊢Lim⁡y↔Ord⁡y∧y≠∅∧y=⋃y
107 106 simp2bi ⊢Lim⁡y→y≠∅
108 107 neneqd ⊢Lim⁡y→¬y=∅
109 108 iffalsed ⊢Lim⁡y→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ifLim⁡y⋃fyF⁡f↾y⁡⋃y
110 iftrue ⊢Lim⁡y→ifLim⁡y⋃fyF⁡f⁡⋃y=⋃fy
111 105 109 110 3eqtr4d ⊢Lim⁡y→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ifLim⁡y⋃fyF⁡f⁡⋃y
112 108 iffalsed ⊢Lim⁡y→ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y=ifLim⁡y⋃fyF⁡f⁡⋃y
113 111 112 eqtr4d ⊢Lim⁡y→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
114 66 104 113 3jaoi ⊢y=∅∨∃z∈Ony=suc⁡z∨Lim⁡y→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
115 63 114 sylbi ⊢Ord⁡y→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
116 62 115 syl ⊢x∈On∧fFnx∧y∈x→ify=∅iifLim⁡y⋃fyF⁡f↾y⁡⋃y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
117 58 116 sylan9eqr ⊢x∈On∧fFnx∧y∈x∧dom⁡f↾y=y→ifdom⁡f↾y=∅iifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
118 51 117 mpdan ⊢x∈On∧fFnx∧y∈x→ifdom⁡f↾y=∅iifLim⁡dom⁡f↾y⋃fyF⁡f↾y⁡⋃dom⁡f↾y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
119 41 118 eqtrid ⊢x∈On∧fFnx∧y∈x→g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
120 119 eqeq2d ⊢x∈On∧fFnx∧y∈x→f⁡y=g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y↔f⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
121 120 3expa ⊢x∈On∧fFnx∧y∈x→f⁡y=g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y↔f⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
122 121 ralbidva ⊢x∈On∧fFnx→∀y∈xf⁡y=g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y↔∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
123 122 pm5.32da ⊢x∈On→fFnx∧∀y∈xf⁡y=g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y↔fFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
124 123 rexbiia ⊢∃x∈OnfFnx∧∀y∈xf⁡y=g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y↔∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
125 124 abbii ⊢f|∃x∈OnfFnx∧∀y∈xf⁡y=g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y=f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
126 125 unieqi ⊢⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=g∈V⟼ifg=∅iifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡f↾y=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
127 10 11 126 3eqtri ⊢rec⁡Fi=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅iifLim⁡y⋃fyF⁡f⁡⋃y
128 9 127 vtoclg ⊢I∈V→rec⁡FI=⋃f|∃x∈OnfFnx∧∀y∈xf⁡y=ify=∅IifLim⁡y⋃fyF⁡f⁡⋃y