Metamath Proof Explorer

Theorem rdgprc

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

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

Proof

Step Hyp Ref Expression
1 fveq2 ⊢z=∅→rec⁡FI⁡z=rec⁡FI⁡∅
2 fveq2 ⊢z=∅→rec⁡F∅⁡z=rec⁡F∅⁡∅
3 1 2 eqeq12d ⊢z=∅→rec⁡FI⁡z=rec⁡F∅⁡z↔rec⁡FI⁡∅=rec⁡F∅⁡∅
4 3 imbi2d ⊢z=∅→¬I∈V→rec⁡FI⁡z=rec⁡F∅⁡z↔¬I∈V→rec⁡FI⁡∅=rec⁡F∅⁡∅
5 fveq2 ⊢z=y→rec⁡FI⁡z=rec⁡FI⁡y
6 fveq2 ⊢z=y→rec⁡F∅⁡z=rec⁡F∅⁡y
7 5 6 eqeq12d ⊢z=y→rec⁡FI⁡z=rec⁡F∅⁡z↔rec⁡FI⁡y=rec⁡F∅⁡y
8 7 imbi2d ⊢z=y→¬I∈V→rec⁡FI⁡z=rec⁡F∅⁡z↔¬I∈V→rec⁡FI⁡y=rec⁡F∅⁡y
9 fveq2 ⊢z=suc⁡y→rec⁡FI⁡z=rec⁡FI⁡suc⁡y
10 fveq2 ⊢z=suc⁡y→rec⁡F∅⁡z=rec⁡F∅⁡suc⁡y
11 9 10 eqeq12d ⊢z=suc⁡y→rec⁡FI⁡z=rec⁡F∅⁡z↔rec⁡FI⁡suc⁡y=rec⁡F∅⁡suc⁡y
12 11 imbi2d ⊢z=suc⁡y→¬I∈V→rec⁡FI⁡z=rec⁡F∅⁡z↔¬I∈V→rec⁡FI⁡suc⁡y=rec⁡F∅⁡suc⁡y
13 fveq2 ⊢z=x→rec⁡FI⁡z=rec⁡FI⁡x
14 fveq2 ⊢z=x→rec⁡F∅⁡z=rec⁡F∅⁡x
15 13 14 eqeq12d ⊢z=x→rec⁡FI⁡z=rec⁡F∅⁡z↔rec⁡FI⁡x=rec⁡F∅⁡x
16 15 imbi2d ⊢z=x→¬I∈V→rec⁡FI⁡z=rec⁡F∅⁡z↔¬I∈V→rec⁡FI⁡x=rec⁡F∅⁡x
17 rdgprc0 ⊢¬I∈V→rec⁡FI⁡∅=∅
18 0ex ⊢∅∈V
19 18 rdg0 ⊢rec⁡F∅⁡∅=∅
20 17 19 eqtr4di ⊢¬I∈V→rec⁡FI⁡∅=rec⁡F∅⁡∅
21 fveq2 ⊢rec⁡FI⁡y=rec⁡F∅⁡y→F⁡rec⁡FI⁡y=F⁡rec⁡F∅⁡y
22 rdgsuc ⊢y∈On→rec⁡FI⁡suc⁡y=F⁡rec⁡FI⁡y
23 rdgsuc ⊢y∈On→rec⁡F∅⁡suc⁡y=F⁡rec⁡F∅⁡y
24 22 23 eqeq12d ⊢y∈On→rec⁡FI⁡suc⁡y=rec⁡F∅⁡suc⁡y↔F⁡rec⁡FI⁡y=F⁡rec⁡F∅⁡y
25 21 24 imbitrrid ⊢y∈On→rec⁡FI⁡y=rec⁡F∅⁡y→rec⁡FI⁡suc⁡y=rec⁡F∅⁡suc⁡y
26 25 imim2d ⊢y∈On→¬I∈V→rec⁡FI⁡y=rec⁡F∅⁡y→¬I∈V→rec⁡FI⁡suc⁡y=rec⁡F∅⁡suc⁡y
27 r19.21v ⊢∀y∈z¬I∈V→rec⁡FI⁡y=rec⁡F∅⁡y↔¬I∈V→∀y∈zrec⁡FI⁡y=rec⁡F∅⁡y
28 limord ⊢Lim⁡z→Ord⁡z
29 ordsson ⊢Ord⁡z→z⊆On
30 rdgfnon ⊢rec⁡FIFnOn
31 rdgfnon ⊢rec⁡F∅FnOn
32 fvreseq ⊢rec⁡FIFnOn∧rec⁡F∅FnOn∧z⊆On→rec⁡FI↾z=rec⁡F∅↾z↔∀y∈zrec⁡FI⁡y=rec⁡F∅⁡y
33 30 31 32 mpanl12 ⊢z⊆On→rec⁡FI↾z=rec⁡F∅↾z↔∀y∈zrec⁡FI⁡y=rec⁡F∅⁡y
34 28 29 33 3syl ⊢Lim⁡z→rec⁡FI↾z=rec⁡F∅↾z↔∀y∈zrec⁡FI⁡y=rec⁡F∅⁡y
35 rneq ⊢rec⁡FI↾z=rec⁡F∅↾z→ran⁡rec⁡FI↾z=ran⁡rec⁡F∅↾z
36 df-ima ⊢rec⁡FIz=ran⁡rec⁡FI↾z
37 df-ima ⊢rec⁡F∅z=ran⁡rec⁡F∅↾z
38 35 36 37 3eqtr4g ⊢rec⁡FI↾z=rec⁡F∅↾z→rec⁡FIz=rec⁡F∅z
39 38 unieqd ⊢rec⁡FI↾z=rec⁡F∅↾z→⋃rec⁡FIz=⋃rec⁡F∅z
40 vex ⊢z∈V
41 rdglim ⊢z∈V∧Lim⁡z→rec⁡FI⁡z=⋃rec⁡FIz
42 rdglim ⊢z∈V∧Lim⁡z→rec⁡F∅⁡z=⋃rec⁡F∅z
43 41 42 eqeq12d ⊢z∈V∧Lim⁡z→rec⁡FI⁡z=rec⁡F∅⁡z↔⋃rec⁡FIz=⋃rec⁡F∅z
44 40 43 mpan ⊢Lim⁡z→rec⁡FI⁡z=rec⁡F∅⁡z↔⋃rec⁡FIz=⋃rec⁡F∅z
45 39 44 imbitrrid ⊢Lim⁡z→rec⁡FI↾z=rec⁡F∅↾z→rec⁡FI⁡z=rec⁡F∅⁡z
46 34 45 sylbird ⊢Lim⁡z→∀y∈zrec⁡FI⁡y=rec⁡F∅⁡y→rec⁡FI⁡z=rec⁡F∅⁡z
47 46 imim2d ⊢Lim⁡z→¬I∈V→∀y∈zrec⁡FI⁡y=rec⁡F∅⁡y→¬I∈V→rec⁡FI⁡z=rec⁡F∅⁡z
48 27 47 biimtrid ⊢Lim⁡z→∀y∈z¬I∈V→rec⁡FI⁡y=rec⁡F∅⁡y→¬I∈V→rec⁡FI⁡z=rec⁡F∅⁡z
49 4 8 12 16 20 26 48 tfinds ⊢x∈On→¬I∈V→rec⁡FI⁡x=rec⁡F∅⁡x
50 49 com12 ⊢¬I∈V→x∈On→rec⁡FI⁡x=rec⁡F∅⁡x
51 50 ralrimiv ⊢¬I∈V→∀x∈Onrec⁡FI⁡x=rec⁡F∅⁡x
52 eqfnfv ⊢rec⁡FIFnOn∧rec⁡F∅FnOn→rec⁡FI=rec⁡F∅↔∀x∈Onrec⁡FI⁡x=rec⁡F∅⁡x
53 30 31 52 mp2an ⊢rec⁡FI=rec⁡F∅↔∀x∈Onrec⁡FI⁡x=rec⁡F∅⁡x
54 51 53 sylibr ⊢¬I∈V→rec⁡FI=rec⁡F∅