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 ) ) ) ) ) ) ) |