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 e. _V -> rec ( F , I ) = rec ( F , (/) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( z = (/) -> ( rec ( F , I ) ` z ) = ( rec ( F , I ) ` (/) ) )
2 fveq2 
 |-  ( z = (/) -> ( rec ( F , (/) ) ` z ) = ( rec ( F , (/) ) ` (/) ) )
3 1 2 eqeq12d 
 |-  ( z = (/) -> ( ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) <-> ( rec ( F , I ) ` (/) ) = ( rec ( F , (/) ) ` (/) ) ) )
4 3 imbi2d 
 |-  ( z = (/) -> ( ( -. I e. _V -> ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) ) <-> ( -. I e. _V -> ( rec ( F , I ) ` (/) ) = ( rec ( F , (/) ) ` (/) ) ) ) )
5 fveq2 
 |-  ( z = y -> ( rec ( F , I ) ` z ) = ( rec ( F , I ) ` y ) )
6 fveq2 
 |-  ( z = y -> ( rec ( F , (/) ) ` z ) = ( rec ( F , (/) ) ` y ) )
7 5 6 eqeq12d 
 |-  ( z = y -> ( ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) <-> ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) )
8 7 imbi2d 
 |-  ( z = y -> ( ( -. I e. _V -> ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) ) <-> ( -. I e. _V -> ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) ) )
9 fveq2 
 |-  ( z = suc y -> ( rec ( F , I ) ` z ) = ( rec ( F , I ) ` suc y ) )
10 fveq2 
 |-  ( z = suc y -> ( rec ( F , (/) ) ` z ) = ( rec ( F , (/) ) ` suc y ) )
11 9 10 eqeq12d 
 |-  ( z = suc y -> ( ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) <-> ( rec ( F , I ) ` suc y ) = ( rec ( F , (/) ) ` suc y ) ) )
12 11 imbi2d 
 |-  ( z = suc y -> ( ( -. I e. _V -> ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) ) <-> ( -. I e. _V -> ( rec ( F , I ) ` suc y ) = ( rec ( F , (/) ) ` suc y ) ) ) )
13 fveq2 
 |-  ( z = x -> ( rec ( F , I ) ` z ) = ( rec ( F , I ) ` x ) )
14 fveq2 
 |-  ( z = x -> ( rec ( F , (/) ) ` z ) = ( rec ( F , (/) ) ` x ) )
15 13 14 eqeq12d 
 |-  ( z = x -> ( ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) <-> ( rec ( F , I ) ` x ) = ( rec ( F , (/) ) ` x ) ) )
16 15 imbi2d 
 |-  ( z = x -> ( ( -. I e. _V -> ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) ) <-> ( -. I e. _V -> ( rec ( F , I ) ` x ) = ( rec ( F , (/) ) ` x ) ) ) )
17 rdgprc0 
 |-  ( -. I e. _V -> ( rec ( F , I ) ` (/) ) = (/) )
18 0ex 
 |-  (/) e. _V
19 18 rdg0 
 |-  ( rec ( F , (/) ) ` (/) ) = (/)
20 17 19 eqtr4di 
 |-  ( -. I e. _V -> ( rec ( F , I ) ` (/) ) = ( rec ( F , (/) ) ` (/) ) )
21 fveq2 
 |-  ( ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) -> ( F ` ( rec ( F , I ) ` y ) ) = ( F ` ( rec ( F , (/) ) ` y ) ) )
22 rdgsuc 
 |-  ( y e. On -> ( rec ( F , I ) ` suc y ) = ( F ` ( rec ( F , I ) ` y ) ) )
23 rdgsuc 
 |-  ( y e. On -> ( rec ( F , (/) ) ` suc y ) = ( F ` ( rec ( F , (/) ) ` y ) ) )
24 22 23 eqeq12d 
 |-  ( y e. On -> ( ( rec ( F , I ) ` suc y ) = ( rec ( F , (/) ) ` suc y ) <-> ( F ` ( rec ( F , I ) ` y ) ) = ( F ` ( rec ( F , (/) ) ` y ) ) ) )
25 21 24 imbitrrid 
 |-  ( y e. On -> ( ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) -> ( rec ( F , I ) ` suc y ) = ( rec ( F , (/) ) ` suc y ) ) )
26 25 imim2d 
 |-  ( y e. On -> ( ( -. I e. _V -> ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) -> ( -. I e. _V -> ( rec ( F , I ) ` suc y ) = ( rec ( F , (/) ) ` suc y ) ) ) )
27 r19.21v 
 |-  ( A. y e. z ( -. I e. _V -> ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) <-> ( -. I e. _V -> A. y e. z ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) )
28 limord 
 |-  ( Lim z -> Ord z )
29 ordsson 
 |-  ( Ord z -> z C_ On )
30 rdgfnon 
 |-  rec ( F , I ) Fn On
31 rdgfnon 
 |-  rec ( F , (/) ) Fn On
32 fvreseq 
 |-  ( ( ( rec ( F , I ) Fn On /\ rec ( F , (/) ) Fn On ) /\ z C_ On ) -> ( ( rec ( F , I ) |` z ) = ( rec ( F , (/) ) |` z ) <-> A. y e. z ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) )
33 30 31 32 mpanl12 
 |-  ( z C_ On -> ( ( rec ( F , I ) |` z ) = ( rec ( F , (/) ) |` z ) <-> A. y e. z ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) )
34 28 29 33 3syl 
 |-  ( Lim z -> ( ( rec ( F , I ) |` z ) = ( rec ( F , (/) ) |` z ) <-> A. y e. z ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) )
35 rneq 
 |-  ( ( rec ( F , I ) |` z ) = ( rec ( F , (/) ) |` z ) -> ran ( rec ( F , I ) |` z ) = ran ( rec ( F , (/) ) |` z ) )
36 df-ima 
 |-  ( rec ( F , I ) " z ) = ran ( rec ( F , I ) |` z )
37 df-ima 
 |-  ( rec ( F , (/) ) " z ) = ran ( rec ( F , (/) ) |` z )
38 35 36 37 3eqtr4g 
 |-  ( ( rec ( F , I ) |` z ) = ( rec ( F , (/) ) |` z ) -> ( rec ( F , I ) " z ) = ( rec ( F , (/) ) " z ) )
39 38 unieqd 
 |-  ( ( rec ( F , I ) |` z ) = ( rec ( F , (/) ) |` z ) -> U. ( rec ( F , I ) " z ) = U. ( rec ( F , (/) ) " z ) )
40 vex 
 |-  z e. _V
41 rdglim 
 |-  ( ( z e. _V /\ Lim z ) -> ( rec ( F , I ) ` z ) = U. ( rec ( F , I ) " z ) )
42 rdglim 
 |-  ( ( z e. _V /\ Lim z ) -> ( rec ( F , (/) ) ` z ) = U. ( rec ( F , (/) ) " z ) )
43 41 42 eqeq12d 
 |-  ( ( z e. _V /\ Lim z ) -> ( ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) <-> U. ( rec ( F , I ) " z ) = U. ( rec ( F , (/) ) " z ) ) )
44 40 43 mpan 
 |-  ( Lim z -> ( ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) <-> U. ( rec ( F , I ) " z ) = U. ( rec ( F , (/) ) " z ) ) )
45 39 44 imbitrrid 
 |-  ( Lim z -> ( ( rec ( F , I ) |` z ) = ( rec ( F , (/) ) |` z ) -> ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) ) )
46 34 45 sylbird 
 |-  ( Lim z -> ( A. y e. z ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) -> ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) ) )
47 46 imim2d 
 |-  ( Lim z -> ( ( -. I e. _V -> A. y e. z ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) -> ( -. I e. _V -> ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) ) ) )
48 27 47 biimtrid 
 |-  ( Lim z -> ( A. y e. z ( -. I e. _V -> ( rec ( F , I ) ` y ) = ( rec ( F , (/) ) ` y ) ) -> ( -. I e. _V -> ( rec ( F , I ) ` z ) = ( rec ( F , (/) ) ` z ) ) ) )
49 4 8 12 16 20 26 48 tfinds 
 |-  ( x e. On -> ( -. I e. _V -> ( rec ( F , I ) ` x ) = ( rec ( F , (/) ) ` x ) ) )
50 49 com12 
 |-  ( -. I e. _V -> ( x e. On -> ( rec ( F , I ) ` x ) = ( rec ( F , (/) ) ` x ) ) )
51 50 ralrimiv 
 |-  ( -. I e. _V -> A. x e. On ( rec ( F , I ) ` x ) = ( rec ( F , (/) ) ` x ) )
52 eqfnfv 
 |-  ( ( rec ( F , I ) Fn On /\ rec ( F , (/) ) Fn On ) -> ( rec ( F , I ) = rec ( F , (/) ) <-> A. x e. On ( rec ( F , I ) ` x ) = ( rec ( F , (/) ) ` x ) ) )
53 30 31 52 mp2an 
 |-  ( rec ( F , I ) = rec ( F , (/) ) <-> A. x e. On ( rec ( F , I ) ` x ) = ( rec ( F , (/) ) ` x ) )
54 51 53 sylibr 
 |-  ( -. I e. _V -> rec ( F , I ) = rec ( F , (/) ) )