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 e. V -> rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 rdgeq2 
 |-  ( i = I -> rec ( F , i ) = rec ( F , I ) )
2 ifeq1 
 |-  ( i = I -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
3 2 eqeq2d 
 |-  ( i = I -> ( ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
4 3 ralbidv 
 |-  ( i = I -> ( A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
5 4 anbi2d 
 |-  ( i = I -> ( ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
6 5 rexbidv 
 |-  ( i = I -> ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
7 6 abbidv 
 |-  ( i = I -> { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
8 7 unieqd 
 |-  ( i = I -> U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
9 1 8 eqeq12d 
 |-  ( i = I -> ( rec ( F , i ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } <-> rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } ) )
10 df-rdg 
 |-  rec ( F , i ) = recs ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
11 dfrecs3 
 |-  recs ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) ) }
12 vex 
 |-  f e. _V
13 12 resex 
 |-  ( f |` y ) e. _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 
 |-  ( f " y ) = ran ( f |` y )
24 22 23 eqtr4di 
 |-  ( g = ( f |` y ) -> ran g = ( f " y ) )
25 24 unieqd 
 |-  ( g = ( f |` y ) -> U. ran g = U. ( f " y ) )
26 id 
 |-  ( g = ( f |` y ) -> g = ( f |` y ) )
27 19 unieqd 
 |-  ( g = ( f |` y ) -> U. dom g = U. dom ( f |` y ) )
28 26 27 fveq12d 
 |-  ( g = ( f |` y ) -> ( g ` U. dom g ) = ( ( f |` y ) ` U. dom ( f |` y ) ) )
29 28 fveq2d 
 |-  ( g = ( f |` y ) -> ( F ` ( g ` U. dom g ) ) = ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) )
30 21 25 29 ifbieq12d 
 |-  ( g = ( f |` y ) -> if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) = if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) )
31 18 30 ifbieq2d 
 |-  ( g = ( f |` y ) -> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) = if ( dom ( f |` y ) = (/) , i , if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) ) )
32 eqid 
 |-  ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) )
33 vex 
 |-  i e. _V
34 imaexg 
 |-  ( f e. _V -> ( f " y ) e. _V )
35 12 34 ax-mp 
 |-  ( f " y ) e. _V
36 35 uniex 
 |-  U. ( f " y ) e. _V
37 fvex 
 |-  ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) e. _V
38 36 37 ifex 
 |-  if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) e. _V
39 33 38 ifex 
 |-  if ( dom ( f |` y ) = (/) , i , if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) ) e. _V
40 31 32 39 fvmpt 
 |-  ( ( f |` y ) e. _V -> ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) = if ( dom ( f |` y ) = (/) , i , if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) ) )
41 13 40 ax-mp 
 |-  ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) = if ( dom ( f |` y ) = (/) , i , if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) )
42 dmres 
 |-  dom ( f |` y ) = ( y i^i dom f )
43 onelss 
 |-  ( x e. On -> ( y e. x -> y C_ x ) )
44 43 imp 
 |-  ( ( x e. On /\ y e. x ) -> y C_ x )
45 44 3adant2 
 |-  ( ( x e. On /\ f Fn x /\ y e. x ) -> y C_ x )
46 fndm 
 |-  ( f Fn x -> dom f = x )
47 46 3ad2ant2 
 |-  ( ( x e. On /\ f Fn x /\ y e. x ) -> dom f = x )
48 45 47 sseqtrrd 
 |-  ( ( x e. On /\ f Fn x /\ y e. x ) -> y C_ dom f )
49 df-ss 
 |-  ( y C_ dom f <-> ( y i^i dom f ) = y )
50 48 49 sylib 
 |-  ( ( x e. On /\ f Fn x /\ y e. x ) -> ( y i^i dom f ) = y )
51 42 50 eqtrid 
 |-  ( ( x e. On /\ f Fn x /\ y e. 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 -> U. dom ( f |` y ) = U. y )
55 54 fveq2d 
 |-  ( dom ( f |` y ) = y -> ( ( f |` y ) ` U. dom ( f |` y ) ) = ( ( f |` y ) ` U. y ) )
56 55 fveq2d 
 |-  ( dom ( f |` y ) = y -> ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) = ( F ` ( ( f |` y ) ` U. y ) ) )
57 53 56 ifbieq2d 
 |-  ( dom ( f |` y ) = y -> if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) = if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) )
58 52 57 ifbieq2d 
 |-  ( dom ( f |` y ) = y -> if ( dom ( f |` y ) = (/) , i , if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) )
59 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
60 eloni 
 |-  ( y e. On -> Ord y )
61 59 60 syl 
 |-  ( ( x e. On /\ y e. x ) -> Ord y )
62 61 3adant2 
 |-  ( ( x e. On /\ f Fn x /\ y e. x ) -> Ord y )
63 ordzsl 
 |-  ( Ord y <-> ( y = (/) \/ E. z e. On y = suc z \/ Lim y ) )
64 iftrue 
 |-  ( y = (/) -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = i )
65 iftrue 
 |-  ( y = (/) -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = i )
66 64 65 eqtr4d 
 |-  ( y = (/) -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
67 vex 
 |-  z e. _V
68 67 sucid 
 |-  z e. suc z
69 fvres 
 |-  ( z e. suc z -> ( ( f |` suc z ) ` z ) = ( f ` z ) )
70 68 69 ax-mp 
 |-  ( ( f |` suc z ) ` z ) = ( f ` z )
71 eloni 
 |-  ( z e. On -> Ord z )
72 ordunisuc 
 |-  ( Ord z -> U. suc z = z )
73 71 72 syl 
 |-  ( z e. On -> U. suc z = z )
74 73 fveq2d 
 |-  ( z e. On -> ( ( f |` suc z ) ` U. suc z ) = ( ( f |` suc z ) ` z ) )
75 73 fveq2d 
 |-  ( z e. On -> ( f ` U. suc z ) = ( f ` z ) )
76 70 74 75 3eqtr4a 
 |-  ( z e. On -> ( ( f |` suc z ) ` U. suc z ) = ( f ` U. suc z ) )
77 76 fveq2d 
 |-  ( z e. On -> ( F ` ( ( f |` suc z ) ` U. suc z ) ) = ( F ` ( f ` U. suc z ) ) )
78 nsuceq0 
 |-  suc z =/= (/)
79 78 neii 
 |-  -. suc z = (/)
80 79 iffalsei 
 |-  if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( ( f |` suc z ) ` U. suc z ) ) ) ) = if ( Lim suc z , U. ( f " y ) , ( F ` ( ( f |` suc z ) ` U. suc z ) ) )
81 nlimsucg 
 |-  ( z e. _V -> -. Lim suc z )
82 iffalse 
 |-  ( -. Lim suc z -> if ( Lim suc z , U. ( f " y ) , ( F ` ( ( f |` suc z ) ` U. suc z ) ) ) = ( F ` ( ( f |` suc z ) ` U. suc z ) ) )
83 67 81 82 mp2b 
 |-  if ( Lim suc z , U. ( f " y ) , ( F ` ( ( f |` suc z ) ` U. suc z ) ) ) = ( F ` ( ( f |` suc z ) ` U. suc z ) )
84 80 83 eqtri 
 |-  if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( ( f |` suc z ) ` U. suc z ) ) ) ) = ( F ` ( ( f |` suc z ) ` U. suc z ) )
85 79 iffalsei 
 |-  if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) ) = if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) )
86 iffalse 
 |-  ( -. Lim suc z -> if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) = ( F ` ( f ` U. suc z ) ) )
87 67 81 86 mp2b 
 |-  if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) = ( F ` ( f ` U. suc z ) )
88 85 87 eqtri 
 |-  if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) ) = ( F ` ( f ` U. suc z ) )
89 77 84 88 3eqtr4g 
 |-  ( z e. On -> if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( ( f |` suc z ) ` U. suc z ) ) ) ) = if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. 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 -> U. y = U. suc z )
94 92 93 fveq12d 
 |-  ( y = suc z -> ( ( f |` y ) ` U. y ) = ( ( f |` suc z ) ` U. suc z ) )
95 94 fveq2d 
 |-  ( y = suc z -> ( F ` ( ( f |` y ) ` U. y ) ) = ( F ` ( ( f |` suc z ) ` U. suc z ) ) )
96 91 95 ifbieq2d 
 |-  ( y = suc z -> if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) = if ( Lim suc z , U. ( f " y ) , ( F ` ( ( f |` suc z ) ` U. suc z ) ) ) )
97 90 96 ifbieq2d 
 |-  ( y = suc z -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( ( f |` suc z ) ` U. suc z ) ) ) ) )
98 93 fveq2d 
 |-  ( y = suc z -> ( f ` U. y ) = ( f ` U. suc z ) )
99 98 fveq2d 
 |-  ( y = suc z -> ( F ` ( f ` U. y ) ) = ( F ` ( f ` U. suc z ) ) )
100 91 99 ifbieq2d 
 |-  ( y = suc z -> if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) = if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) )
101 90 100 ifbieq2d 
 |-  ( y = suc z -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) ) )
102 97 101 eqeq12d 
 |-  ( y = suc z -> ( if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( ( f |` suc z ) ` U. suc z ) ) ) ) = if ( suc z = (/) , i , if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) ) ) )
103 89 102 syl5ibrcom 
 |-  ( z e. On -> ( y = suc z -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
104 103 rexlimiv 
 |-  ( E. z e. On y = suc z -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
105 iftrue 
 |-  ( Lim y -> if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) = U. ( f " y ) )
106 df-lim 
 |-  ( Lim y <-> ( Ord y /\ y =/= (/) /\ y = U. y ) )
107 106 simp2bi 
 |-  ( Lim y -> y =/= (/) )
108 107 neneqd 
 |-  ( Lim y -> -. y = (/) )
109 108 iffalsed 
 |-  ( Lim y -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) )
110 iftrue 
 |-  ( Lim y -> if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) = U. ( f " y ) )
111 105 109 110 3eqtr4d 
 |-  ( Lim y -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) )
112 108 iffalsed 
 |-  ( Lim y -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) )
113 111 112 eqtr4d 
 |-  ( Lim y -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
114 66 104 113 3jaoi 
 |-  ( ( y = (/) \/ E. z e. On y = suc z \/ Lim y ) -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
115 63 114 sylbi 
 |-  ( Ord y -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
116 62 115 syl 
 |-  ( ( x e. On /\ f Fn x /\ y e. x ) -> if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. y ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
117 58 116 sylan9eqr 
 |-  ( ( ( x e. On /\ f Fn x /\ y e. x ) /\ dom ( f |` y ) = y ) -> if ( dom ( f |` y ) = (/) , i , if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
118 51 117 mpdan 
 |-  ( ( x e. On /\ f Fn x /\ y e. x ) -> if ( dom ( f |` y ) = (/) , i , if ( Lim dom ( f |` y ) , U. ( f " y ) , ( F ` ( ( f |` y ) ` U. dom ( f |` y ) ) ) ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
119 41 118 eqtrid 
 |-  ( ( x e. On /\ f Fn x /\ y e. x ) -> ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
120 119 eqeq2d 
 |-  ( ( x e. On /\ f Fn x /\ y e. x ) -> ( ( f ` y ) = ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) <-> ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
121 120 3expa 
 |-  ( ( ( x e. On /\ f Fn x ) /\ y e. x ) -> ( ( f ` y ) = ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) <-> ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
122 121 ralbidva 
 |-  ( ( x e. On /\ f Fn x ) -> ( A. y e. x ( f ` y ) = ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) <-> A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
123 122 pm5.32da 
 |-  ( x e. On -> ( ( f Fn x /\ A. y e. x ( f ` y ) = ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) ) <-> ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
124 123 rexbiia 
 |-  ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) ) <-> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
125 124 abbii 
 |-  { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }
126 125 unieqi 
 |-  U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( ( g e. _V |-> if ( g = (/) , i , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( f |` y ) ) ) } = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }
127 10 11 126 3eqtri 
 |-  rec ( F , i ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , i , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }
128 9 127 vtoclg 
 |-  ( I e. V -> rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )