This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfrdg4

Description: A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfrdg4 
|- rec ( F , A ) = U. ( ( Funs i^i ( `' Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfrdg3 
 |-  rec ( F , A ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }
2 an12 
 |-  ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) <-> ( f Fn x /\ ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
3 df-fn 
 |-  ( f Fn x <-> ( Fun f /\ dom f = x ) )
4 ancom 
 |-  ( ( Fun f /\ dom f = x ) <-> ( dom f = x /\ Fun f ) )
5 eqcom 
 |-  ( dom f = x <-> x = dom f )
6 5 anbi1i 
 |-  ( ( dom f = x /\ Fun f ) <-> ( x = dom f /\ Fun f ) )
7 3 4 6 3bitri 
 |-  ( f Fn x <-> ( x = dom f /\ Fun f ) )
8 7 anbi1i 
 |-  ( ( f Fn x /\ ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) <-> ( ( x = dom f /\ Fun f ) /\ ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
9 anass 
 |-  ( ( ( x = dom f /\ Fun f ) /\ ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) <-> ( x = dom f /\ ( Fun f /\ ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) ) )
10 2 8 9 3bitri 
 |-  ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) <-> ( x = dom f /\ ( Fun f /\ ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) ) )
11 10 exbii 
 |-  ( E. x ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) <-> E. x ( x = dom f /\ ( Fun f /\ ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) ) )
12 vex 
 |-  f e. _V
13 12 dmex 
 |-  dom f e. _V
14 eleq1 
 |-  ( x = dom f -> ( x e. On <-> dom f e. On ) )
15 raleq 
 |-  ( x = dom f -> ( A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
16 14 15 anbi12d 
 |-  ( x = dom f -> ( ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> ( dom f e. On /\ A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
17 16 anbi2d 
 |-  ( x = dom f -> ( ( Fun f /\ ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) <-> ( Fun f /\ ( dom f e. On /\ A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) ) )
18 13 17 ceqsexv 
 |-  ( E. x ( x = dom f /\ ( Fun f /\ ( x e. On /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) ) <-> ( Fun f /\ ( dom f e. On /\ A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
19 11 18 bitri 
 |-  ( E. x ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) <-> ( Fun f /\ ( dom f e. On /\ A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
20 df-rex 
 |-  ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> E. x ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
21 eldif 
 |-  ( f e. ( ( Funs i^i ( `' Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) <-> ( f e. ( Funs i^i ( `' Domain " On ) ) /\ -. f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) )
22 elin 
 |-  ( f e. ( Funs i^i ( `' Domain " On ) ) <-> ( f e. Funs /\ f e. ( `' Domain " On ) ) )
23 12 elfuns 
 |-  ( f e. Funs <-> Fun f )
24 12 elima 
 |-  ( f e. ( `' Domain " On ) <-> E. x e. On x `' Domain f )
25 df-rex 
 |-  ( E. x e. On x `' Domain f <-> E. x ( x e. On /\ x `' Domain f ) )
26 vex 
 |-  x e. _V
27 26 12 brcnv 
 |-  ( x `' Domain f <-> f Domain x )
28 12 26 brdomain 
 |-  ( f Domain x <-> x = dom f )
29 27 28 bitri 
 |-  ( x `' Domain f <-> x = dom f )
30 29 anbi1ci 
 |-  ( ( x e. On /\ x `' Domain f ) <-> ( x = dom f /\ x e. On ) )
31 30 exbii 
 |-  ( E. x ( x e. On /\ x `' Domain f ) <-> E. x ( x = dom f /\ x e. On ) )
32 13 14 ceqsexv 
 |-  ( E. x ( x = dom f /\ x e. On ) <-> dom f e. On )
33 31 32 bitri 
 |-  ( E. x ( x e. On /\ x `' Domain f ) <-> dom f e. On )
34 24 25 33 3bitri 
 |-  ( f e. ( `' Domain " On ) <-> dom f e. On )
35 23 34 anbi12i 
 |-  ( ( f e. Funs /\ f e. ( `' Domain " On ) ) <-> ( Fun f /\ dom f e. On ) )
36 22 35 bitri 
 |-  ( f e. ( Funs i^i ( `' Domain " On ) ) <-> ( Fun f /\ dom f e. On ) )
37 36 anbi1i 
 |-  ( ( f e. ( Funs i^i ( `' Domain " On ) ) /\ -. f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) <-> ( ( Fun f /\ dom f e. On ) /\ -. f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) )
38 brdif 
 |-  ( f ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) y <-> ( f ( `' _E o. Domain ) y /\ -. f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y ) )
39 vex 
 |-  y e. _V
40 12 39 brco 
 |-  ( f ( `' _E o. Domain ) y <-> E. x ( f Domain x /\ x `' _E y ) )
41 28 anbi1i 
 |-  ( ( f Domain x /\ x `' _E y ) <-> ( x = dom f /\ x `' _E y ) )
42 41 exbii 
 |-  ( E. x ( f Domain x /\ x `' _E y ) <-> E. x ( x = dom f /\ x `' _E y ) )
43 breq1 
 |-  ( x = dom f -> ( x `' _E y <-> dom f `' _E y ) )
44 13 43 ceqsexv 
 |-  ( E. x ( x = dom f /\ x `' _E y ) <-> dom f `' _E y )
45 42 44 bitri 
 |-  ( E. x ( f Domain x /\ x `' _E y ) <-> dom f `' _E y )
46 13 39 brcnv 
 |-  ( dom f `' _E y <-> y _E dom f )
47 13 epeli 
 |-  ( y _E dom f <-> y e. dom f )
48 46 47 bitri 
 |-  ( dom f `' _E y <-> y e. dom f )
49 40 45 48 3bitri 
 |-  ( f ( `' _E o. Domain ) y <-> y e. dom f )
50 49 anbi1i 
 |-  ( ( f ( `' _E o. Domain ) y /\ -. f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y ) <-> ( y e. dom f /\ -. f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y ) )
51 38 50 bitri 
 |-  ( f ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) y <-> ( y e. dom f /\ -. f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y ) )
52 onelon 
 |-  ( ( dom f e. On /\ y e. dom f ) -> y e. On )
53 52 3adant1 
 |-  ( ( Fun f /\ dom f e. On /\ y e. dom f ) -> y e. On )
54 brun 
 |-  ( <. f , y >. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) x <-> ( <. f , y >. ( ( _V X. { (/) } ) X. { U. { A } } ) x \/ <. f , y >. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) x ) )
55 brxp 
 |-  ( <. f , y >. ( ( _V X. { (/) } ) X. { U. { A } } ) x <-> ( <. f , y >. e. ( _V X. { (/) } ) /\ x e. { U. { A } } ) )
56 opelxp 
 |-  ( <. f , y >. e. ( _V X. { (/) } ) <-> ( f e. _V /\ y e. { (/) } ) )
57 12 56 mpbiran 
 |-  ( <. f , y >. e. ( _V X. { (/) } ) <-> y e. { (/) } )
58 velsn 
 |-  ( y e. { (/) } <-> y = (/) )
59 57 58 bitri 
 |-  ( <. f , y >. e. ( _V X. { (/) } ) <-> y = (/) )
60 velsn 
 |-  ( x e. { U. { A } } <-> x = U. { A } )
61 59 60 anbi12i 
 |-  ( ( <. f , y >. e. ( _V X. { (/) } ) /\ x e. { U. { A } } ) <-> ( y = (/) /\ x = U. { A } ) )
62 55 61 bitri 
 |-  ( <. f , y >. ( ( _V X. { (/) } ) X. { U. { A } } ) x <-> ( y = (/) /\ x = U. { A } ) )
63 brun 
 |-  ( <. f , y >. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) x <-> ( <. f , y >. ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) x \/ <. f , y >. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) x ) )
64 26 brresi 
 |-  ( <. f , y >. ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) x <-> ( <. f , y >. e. ( _V X. Limits ) /\ <. f , y >. ( Bigcup o. Img ) x ) )
65 opelxp 
 |-  ( <. f , y >. e. ( _V X. Limits ) <-> ( f e. _V /\ y e. Limits ) )
66 12 65 mpbiran 
 |-  ( <. f , y >. e. ( _V X. Limits ) <-> y e. Limits )
67 39 ellimits 
 |-  ( y e. Limits <-> Lim y )
68 66 67 bitri 
 |-  ( <. f , y >. e. ( _V X. Limits ) <-> Lim y )
69 opex 
 |-  <. f , y >. e. _V
70 69 26 brco 
 |-  ( <. f , y >. ( Bigcup o. Img ) x <-> E. z ( <. f , y >. Img z /\ z Bigcup x ) )
71 vex 
 |-  z e. _V
72 12 39 71 brimg 
 |-  ( <. f , y >. Img z <-> z = ( f " y ) )
73 26 brbigcup 
 |-  ( z Bigcup x <-> U. z = x )
74 72 73 anbi12i 
 |-  ( ( <. f , y >. Img z /\ z Bigcup x ) <-> ( z = ( f " y ) /\ U. z = x ) )
75 74 exbii 
 |-  ( E. z ( <. f , y >. Img z /\ z Bigcup x ) <-> E. z ( z = ( f " y ) /\ U. z = x ) )
76 12 imaex 
 |-  ( f " y ) e. _V
77 unieq 
 |-  ( z = ( f " y ) -> U. z = U. ( f " y ) )
78 77 eqeq1d 
 |-  ( z = ( f " y ) -> ( U. z = x <-> U. ( f " y ) = x ) )
79 76 78 ceqsexv 
 |-  ( E. z ( z = ( f " y ) /\ U. z = x ) <-> U. ( f " y ) = x )
80 eqcom 
 |-  ( U. ( f " y ) = x <-> x = U. ( f " y ) )
81 79 80 bitri 
 |-  ( E. z ( z = ( f " y ) /\ U. z = x ) <-> x = U. ( f " y ) )
82 70 75 81 3bitri 
 |-  ( <. f , y >. ( Bigcup o. Img ) x <-> x = U. ( f " y ) )
83 68 82 anbi12i 
 |-  ( ( <. f , y >. e. ( _V X. Limits ) /\ <. f , y >. ( Bigcup o. Img ) x ) <-> ( Lim y /\ x = U. ( f " y ) ) )
84 64 83 bitri 
 |-  ( <. f , y >. ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) x <-> ( Lim y /\ x = U. ( f " y ) ) )
85 26 brresi 
 |-  ( <. f , y >. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) x <-> ( <. f , y >. e. ( _V X. ran Succ ) /\ <. f , y >. ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) x ) )
86 opelxp 
 |-  ( <. f , y >. e. ( _V X. ran Succ ) <-> ( f e. _V /\ y e. ran Succ ) )
87 12 86 mpbiran 
 |-  ( <. f , y >. e. ( _V X. ran Succ ) <-> y e. ran Succ )
88 39 elrn 
 |-  ( y e. ran Succ <-> E. z z Succ y )
89 71 39 brsuccf 
 |-  ( z Succ y <-> y = suc z )
90 89 exbii 
 |-  ( E. z z Succ y <-> E. z y = suc z )
91 87 88 90 3bitri 
 |-  ( <. f , y >. e. ( _V X. ran Succ ) <-> E. z y = suc z )
92 69 26 brco 
 |-  ( <. f , y >. ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) x <-> E. a ( <. f , y >. ( Apply o. pprod ( _I , Bigcup ) ) a /\ a FullFun F x ) )
93 vex 
 |-  a e. _V
94 69 93 brco 
 |-  ( <. f , y >. ( Apply o. pprod ( _I , Bigcup ) ) a <-> E. z ( <. f , y >. pprod ( _I , Bigcup ) z /\ z Apply a ) )
95 12 39 71 brpprod3a 
 |-  ( <. f , y >. pprod ( _I , Bigcup ) z <-> E. a E. b ( z = <. a , b >. /\ f _I a /\ y Bigcup b ) )
96 3anrot 
 |-  ( ( z = <. a , b >. /\ f _I a /\ y Bigcup b ) <-> ( f _I a /\ y Bigcup b /\ z = <. a , b >. ) )
97 93 ideq 
 |-  ( f _I a <-> f = a )
98 equcom 
 |-  ( f = a <-> a = f )
99 97 98 bitri 
 |-  ( f _I a <-> a = f )
100 vex 
 |-  b e. _V
101 100 brbigcup 
 |-  ( y Bigcup b <-> U. y = b )
102 eqcom 
 |-  ( U. y = b <-> b = U. y )
103 101 102 bitri 
 |-  ( y Bigcup b <-> b = U. y )
104 biid 
 |-  ( z = <. a , b >. <-> z = <. a , b >. )
105 99 103 104 3anbi123i 
 |-  ( ( f _I a /\ y Bigcup b /\ z = <. a , b >. ) <-> ( a = f /\ b = U. y /\ z = <. a , b >. ) )
106 96 105 bitri 
 |-  ( ( z = <. a , b >. /\ f _I a /\ y Bigcup b ) <-> ( a = f /\ b = U. y /\ z = <. a , b >. ) )
107 106 2exbii 
 |-  ( E. a E. b ( z = <. a , b >. /\ f _I a /\ y Bigcup b ) <-> E. a E. b ( a = f /\ b = U. y /\ z = <. a , b >. ) )
108 vuniex 
 |-  U. y e. _V
109 opeq1 
 |-  ( a = f -> <. a , b >. = <. f , b >. )
110 109 eqeq2d 
 |-  ( a = f -> ( z = <. a , b >. <-> z = <. f , b >. ) )
111 opeq2 
 |-  ( b = U. y -> <. f , b >. = <. f , U. y >. )
112 111 eqeq2d 
 |-  ( b = U. y -> ( z = <. f , b >. <-> z = <. f , U. y >. ) )
113 12 108 110 112 ceqsex2v 
 |-  ( E. a E. b ( a = f /\ b = U. y /\ z = <. a , b >. ) <-> z = <. f , U. y >. )
114 95 107 113 3bitri 
 |-  ( <. f , y >. pprod ( _I , Bigcup ) z <-> z = <. f , U. y >. )
115 114 anbi1i 
 |-  ( ( <. f , y >. pprod ( _I , Bigcup ) z /\ z Apply a ) <-> ( z = <. f , U. y >. /\ z Apply a ) )
116 115 exbii 
 |-  ( E. z ( <. f , y >. pprod ( _I , Bigcup ) z /\ z Apply a ) <-> E. z ( z = <. f , U. y >. /\ z Apply a ) )
117 opex 
 |-  <. f , U. y >. e. _V
118 breq1 
 |-  ( z = <. f , U. y >. -> ( z Apply a <-> <. f , U. y >. Apply a ) )
119 117 118 ceqsexv 
 |-  ( E. z ( z = <. f , U. y >. /\ z Apply a ) <-> <. f , U. y >. Apply a )
120 12 108 93 brapply 
 |-  ( <. f , U. y >. Apply a <-> a = ( f ` U. y ) )
121 119 120 bitri 
 |-  ( E. z ( z = <. f , U. y >. /\ z Apply a ) <-> a = ( f ` U. y ) )
122 94 116 121 3bitri 
 |-  ( <. f , y >. ( Apply o. pprod ( _I , Bigcup ) ) a <-> a = ( f ` U. y ) )
123 93 26 brfullfun 
 |-  ( a FullFun F x <-> x = ( F ` a ) )
124 122 123 anbi12i 
 |-  ( ( <. f , y >. ( Apply o. pprod ( _I , Bigcup ) ) a /\ a FullFun F x ) <-> ( a = ( f ` U. y ) /\ x = ( F ` a ) ) )
125 124 exbii 
 |-  ( E. a ( <. f , y >. ( Apply o. pprod ( _I , Bigcup ) ) a /\ a FullFun F x ) <-> E. a ( a = ( f ` U. y ) /\ x = ( F ` a ) ) )
126 fvex 
 |-  ( f ` U. y ) e. _V
127 fveq2 
 |-  ( a = ( f ` U. y ) -> ( F ` a ) = ( F ` ( f ` U. y ) ) )
128 127 eqeq2d 
 |-  ( a = ( f ` U. y ) -> ( x = ( F ` a ) <-> x = ( F ` ( f ` U. y ) ) ) )
129 126 128 ceqsexv 
 |-  ( E. a ( a = ( f ` U. y ) /\ x = ( F ` a ) ) <-> x = ( F ` ( f ` U. y ) ) )
130 92 125 129 3bitri 
 |-  ( <. f , y >. ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) x <-> x = ( F ` ( f ` U. y ) ) )
131 91 130 anbi12i 
 |-  ( ( <. f , y >. e. ( _V X. ran Succ ) /\ <. f , y >. ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) x ) <-> ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) )
132 85 131 bitri 
 |-  ( <. f , y >. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) x <-> ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) )
133 84 132 orbi12i 
 |-  ( ( <. f , y >. ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) x \/ <. f , y >. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) x ) <-> ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) )
134 63 133 bitri 
 |-  ( <. f , y >. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) x <-> ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) )
135 62 134 orbi12i 
 |-  ( ( <. f , y >. ( ( _V X. { (/) } ) X. { U. { A } } ) x \/ <. f , y >. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) x ) <-> ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) )
136 54 135 bitri 
 |-  ( <. f , y >. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) x <-> ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) )
137 onzsl 
 |-  ( y e. On <-> ( y = (/) \/ E. z e. On y = suc z \/ ( y e. _V /\ Lim y ) ) )
138 nlim0 
 |-  -. Lim (/)
139 limeq 
 |-  ( y = (/) -> ( Lim y <-> Lim (/) ) )
140 138 139 mtbiri 
 |-  ( y = (/) -> -. Lim y )
141 140 intnanrd 
 |-  ( y = (/) -> -. ( Lim y /\ x = U. ( f " y ) ) )
142 nsuceq0 
 |-  suc z =/= (/)
143 neeq2 
 |-  ( y = (/) -> ( suc z =/= y <-> suc z =/= (/) ) )
144 142 143 mpbiri 
 |-  ( y = (/) -> suc z =/= y )
145 144 necomd 
 |-  ( y = (/) -> y =/= suc z )
146 145 neneqd 
 |-  ( y = (/) -> -. y = suc z )
147 146 nexdv 
 |-  ( y = (/) -> -. E. z y = suc z )
148 147 intnanrd 
 |-  ( y = (/) -> -. ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) )
149 ioran 
 |-  ( -. ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) <-> ( -. ( Lim y /\ x = U. ( f " y ) ) /\ -. ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) )
150 141 148 149 sylanbrc 
 |-  ( y = (/) -> -. ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) )
151 orel2 
 |-  ( -. ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) -> ( y = (/) /\ x = U. { A } ) ) )
152 150 151 syl 
 |-  ( y = (/) -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) -> ( y = (/) /\ x = U. { A } ) ) )
153 iftrue 
 |-  ( y = (/) -> if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = if ( A e. _V , A , (/) ) )
154 unisnif 
 |-  U. { A } = if ( A e. _V , A , (/) )
155 153 154 eqtr4di 
 |-  ( y = (/) -> if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = U. { A } )
156 155 eqeq2d 
 |-  ( y = (/) -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> x = U. { A } ) )
157 156 biimprd 
 |-  ( y = (/) -> ( x = U. { A } -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
158 157 adantld 
 |-  ( y = (/) -> ( ( y = (/) /\ x = U. { A } ) -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
159 152 158 syld 
 |-  ( y = (/) -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
160 156 biimpd 
 |-  ( y = (/) -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) -> x = U. { A } ) )
161 160 anc2li 
 |-  ( y = (/) -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) -> ( y = (/) /\ x = U. { A } ) ) )
162 orc 
 |-  ( ( y = (/) /\ x = U. { A } ) -> ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) )
163 161 162 syl6 
 |-  ( y = (/) -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) -> ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) ) )
164 159 163 impbid 
 |-  ( y = (/) -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) <-> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
165 neeq1 
 |-  ( y = suc z -> ( y =/= (/) <-> suc z =/= (/) ) )
166 142 165 mpbiri 
 |-  ( y = suc z -> y =/= (/) )
167 166 neneqd 
 |-  ( y = suc z -> -. y = (/) )
168 167 intnanrd 
 |-  ( y = suc z -> -. ( y = (/) /\ x = U. { A } ) )
169 168 rexlimivw 
 |-  ( E. z e. On y = suc z -> -. ( y = (/) /\ x = U. { A } ) )
170 orel1 
 |-  ( -. ( y = (/) /\ x = U. { A } ) -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) -> ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) )
171 169 170 syl 
 |-  ( E. z e. On y = suc z -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) -> ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) )
172 nlimsucg 
 |-  ( z e. _V -> -. Lim suc z )
173 172 elv 
 |-  -. Lim suc z
174 limeq 
 |-  ( y = suc z -> ( Lim y <-> Lim suc z ) )
175 173 174 mtbiri 
 |-  ( y = suc z -> -. Lim y )
176 175 rexlimivw 
 |-  ( E. z e. On y = suc z -> -. Lim y )
177 176 intnanrd 
 |-  ( E. z e. On y = suc z -> -. ( Lim y /\ x = U. ( f " y ) ) )
178 orel1 
 |-  ( -. ( Lim y /\ x = U. ( f " y ) ) -> ( ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) -> ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) )
179 177 178 syl 
 |-  ( E. z e. On y = suc z -> ( ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) -> ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) )
180 142 neii 
 |-  -. suc z = (/)
181 180 iffalsei 
 |-  if ( suc z = (/) , if ( A e. _V , A , (/) ) , if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) ) = if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) )
182 iffalse 
 |-  ( -. Lim suc z -> if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) = ( F ` ( f ` U. suc z ) ) )
183 71 172 182 mp2b 
 |-  if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) = ( F ` ( f ` U. suc z ) )
184 181 183 eqtri 
 |-  if ( suc z = (/) , if ( A e. _V , A , (/) ) , if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) ) = ( F ` ( f ` U. suc z ) )
185 eqeq1 
 |-  ( y = suc z -> ( y = (/) <-> suc z = (/) ) )
186 unieq 
 |-  ( y = suc z -> U. y = U. suc z )
187 186 fveq2d 
 |-  ( y = suc z -> ( f ` U. y ) = ( f ` U. suc z ) )
188 187 fveq2d 
 |-  ( y = suc z -> ( F ` ( f ` U. y ) ) = ( F ` ( f ` U. suc z ) ) )
189 174 188 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 ) ) ) )
190 185 189 ifbieq2d 
 |-  ( y = suc z -> if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = if ( suc z = (/) , if ( A e. _V , A , (/) ) , if ( Lim suc z , U. ( f " y ) , ( F ` ( f ` U. suc z ) ) ) ) )
191 184 190 188 3eqtr4a 
 |-  ( y = suc z -> if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = ( F ` ( f ` U. y ) ) )
192 191 rexlimivw 
 |-  ( E. z e. On y = suc z -> if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = ( F ` ( f ` U. y ) ) )
193 192 eqeq2d 
 |-  ( E. z e. On y = suc z -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> x = ( F ` ( f ` U. y ) ) ) )
194 193 biimprd 
 |-  ( E. z e. On y = suc z -> ( x = ( F ` ( f ` U. y ) ) -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
195 194 adantld 
 |-  ( E. z e. On y = suc z -> ( ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
196 171 179 195 3syld 
 |-  ( E. z e. On y = suc z -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
197 rexex 
 |-  ( E. z e. On y = suc z -> E. z y = suc z )
198 193 biimpd 
 |-  ( E. z e. On y = suc z -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) -> x = ( F ` ( f ` U. y ) ) ) )
199 olc 
 |-  ( ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) -> ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) )
200 199 olcd 
 |-  ( ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) -> ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) )
201 197 198 200 syl6an 
 |-  ( E. z e. On y = suc z -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) -> ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) ) )
202 196 201 impbid 
 |-  ( E. z e. On y = suc z -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) <-> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
203 140 con2i 
 |-  ( Lim y -> -. y = (/) )
204 203 intnanrd 
 |-  ( Lim y -> -. ( y = (/) /\ x = U. { A } ) )
205 204 170 syl 
 |-  ( Lim y -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) -> ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) )
206 175 exlimiv 
 |-  ( E. z y = suc z -> -. Lim y )
207 206 con2i 
 |-  ( Lim y -> -. E. z y = suc z )
208 207 intnanrd 
 |-  ( Lim y -> -. ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) )
209 orel2 
 |-  ( -. ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) -> ( ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) -> ( Lim y /\ x = U. ( f " y ) ) ) )
210 208 209 syl 
 |-  ( Lim y -> ( ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) -> ( Lim y /\ x = U. ( f " y ) ) ) )
211 203 iffalsed 
 |-  ( Lim y -> if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) )
212 iftrue 
 |-  ( Lim y -> if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) = U. ( f " y ) )
213 211 212 eqtrd 
 |-  ( Lim y -> if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = U. ( f " y ) )
214 213 eqeq2d 
 |-  ( Lim y -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> x = U. ( f " y ) ) )
215 214 biimprd 
 |-  ( Lim y -> ( x = U. ( f " y ) -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
216 215 adantld 
 |-  ( Lim y -> ( ( Lim y /\ x = U. ( f " y ) ) -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
217 205 210 216 3syld 
 |-  ( Lim y -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
218 217 adantl 
 |-  ( ( y e. _V /\ Lim y ) -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) -> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
219 214 biimpd 
 |-  ( Lim y -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) -> x = U. ( f " y ) ) )
220 219 anc2li 
 |-  ( Lim y -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) -> ( Lim y /\ x = U. ( f " y ) ) ) )
221 orc 
 |-  ( ( Lim y /\ x = U. ( f " y ) ) -> ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) )
222 221 olcd 
 |-  ( ( Lim y /\ x = U. ( f " y ) ) -> ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) )
223 220 222 syl6 
 |-  ( Lim y -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) -> ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) ) )
224 223 adantl 
 |-  ( ( y e. _V /\ Lim y ) -> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) -> ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) ) )
225 218 224 impbid 
 |-  ( ( y e. _V /\ Lim y ) -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) <-> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
226 164 202 225 3jaoi 
 |-  ( ( y = (/) \/ E. z e. On y = suc z \/ ( y e. _V /\ Lim y ) ) -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) <-> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
227 137 226 sylbi 
 |-  ( y e. On -> ( ( ( y = (/) /\ x = U. { A } ) \/ ( ( Lim y /\ x = U. ( f " y ) ) \/ ( E. z y = suc z /\ x = ( F ` ( f ` U. y ) ) ) ) ) <-> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
228 136 227 bitrid 
 |-  ( y e. On -> ( <. f , y >. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) x <-> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
229 53 228 syl 
 |-  ( ( Fun f /\ dom f e. On /\ y e. dom f ) -> ( <. f , y >. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) x <-> x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
230 26 69 brcnv 
 |-  ( x `' Apply <. f , y >. <-> <. f , y >. Apply x )
231 12 39 26 brapply 
 |-  ( <. f , y >. Apply x <-> x = ( f ` y ) )
232 230 231 bitri 
 |-  ( x `' Apply <. f , y >. <-> x = ( f ` y ) )
233 232 a1i 
 |-  ( ( Fun f /\ dom f e. On /\ y e. dom f ) -> ( x `' Apply <. f , y >. <-> x = ( f ` y ) ) )
234 229 233 anbi12d 
 |-  ( ( Fun f /\ dom f e. On /\ y e. dom f ) -> ( ( <. f , y >. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) x /\ x `' Apply <. f , y >. ) <-> ( x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) /\ x = ( f ` y ) ) ) )
235 234 biancomd 
 |-  ( ( Fun f /\ dom f e. On /\ y e. dom f ) -> ( ( <. f , y >. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) x /\ x `' Apply <. f , y >. ) <-> ( x = ( f ` y ) /\ x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
236 235 exbidv 
 |-  ( ( Fun f /\ dom f e. On /\ y e. dom f ) -> ( E. x ( <. f , y >. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) x /\ x `' Apply <. f , y >. ) <-> E. x ( x = ( f ` y ) /\ x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
237 df-br 
 |-  ( f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y <-> <. f , y >. e. Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) )
238 69 elfix 
 |-  ( <. f , y >. e. Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) <-> <. f , y >. ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) <. f , y >. )
239 69 69 brco 
 |-  ( <. f , y >. ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) <. f , y >. <-> E. x ( <. f , y >. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) x /\ x `' Apply <. f , y >. ) )
240 237 238 239 3bitri 
 |-  ( f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y <-> E. x ( <. f , y >. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) x /\ x `' Apply <. f , y >. ) )
241 fvex 
 |-  ( f ` y ) e. _V
242 241 eqvinc 
 |-  ( ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> E. x ( x = ( f ` y ) /\ x = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
243 236 240 242 3bitr4g 
 |-  ( ( Fun f /\ dom f e. On /\ y e. dom f ) -> ( f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y <-> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
244 243 notbid 
 |-  ( ( Fun f /\ dom f e. On /\ y e. dom f ) -> ( -. f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y <-> -. ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
245 244 3expia 
 |-  ( ( Fun f /\ dom f e. On ) -> ( y e. dom f -> ( -. f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y <-> -. ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
246 245 pm5.32d 
 |-  ( ( Fun f /\ dom f e. On ) -> ( ( y e. dom f /\ -. f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y ) <-> ( y e. dom f /\ -. ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
247 annim 
 |-  ( ( y e. dom f /\ -. ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> -. ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
248 246 247 bitrdi 
 |-  ( ( Fun f /\ dom f e. On ) -> ( ( y e. dom f /\ -. f Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) y ) <-> -. ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
249 51 248 bitrid 
 |-  ( ( Fun f /\ dom f e. On ) -> ( f ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) y <-> -. ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
250 249 exbidv 
 |-  ( ( Fun f /\ dom f e. On ) -> ( E. y f ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) y <-> E. y -. ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
251 exnal 
 |-  ( E. y -. ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> -. A. y ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
252 250 251 bitr2di 
 |-  ( ( Fun f /\ dom f e. On ) -> ( -. A. y ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> E. y f ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) y ) )
253 12 eldm 
 |-  ( f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) <-> E. y f ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) y )
254 252 253 bitr4di 
 |-  ( ( Fun f /\ dom f e. On ) -> ( -. A. y ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) )
255 254 con1bid 
 |-  ( ( Fun f /\ dom f e. On ) -> ( -. f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) <-> A. y ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
256 df-ral 
 |-  ( A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> A. y ( y e. dom f -> ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
257 255 256 bitr4di 
 |-  ( ( Fun f /\ dom f e. On ) -> ( -. f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) <-> A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
258 257 pm5.32i 
 |-  ( ( ( Fun f /\ dom f e. On ) /\ -. f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) <-> ( ( Fun f /\ dom f e. On ) /\ A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
259 anass 
 |-  ( ( ( Fun f /\ dom f e. On ) /\ A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> ( Fun f /\ ( dom f e. On /\ A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
260 258 259 bitri 
 |-  ( ( ( Fun f /\ dom f e. On ) /\ -. f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) <-> ( Fun f /\ ( dom f e. On /\ A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
261 21 37 260 3bitri 
 |-  ( f e. ( ( Funs i^i ( `' Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) <-> ( Fun f /\ ( dom f e. On /\ A. y e. dom f ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
262 19 20 261 3bitr4ri 
 |-  ( f e. ( ( Funs i^i ( `' Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) <-> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
263 262 eqabi 
 |-  ( ( Funs i^i ( `' Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }
264 263 unieqi 
 |-  U. ( ( Funs i^i ( `' Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( A e. _V , A , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }
265 1 264 eqtr4i 
 |-  rec ( F , A ) = U. ( ( Funs i^i ( `' Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( ( FullFun F o. ( Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) )