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 syl5bb
 |-  ( 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 syl5bb
 |-  ( ( 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 abbi2i
 |-  ( ( 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 ) ) ) ) ) ) )