Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfrdg4 Unicode version

Theorem dfrdg4 24488
Description: A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
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 of Theorem dfrdg4
Dummy variables  a 
b  f  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfrdg3 24153 . 2  |-  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 772 . . . . . . . 8  |-  ( ( 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 5258 . . . . . . . . . 10  |-  ( f  Fn  x  <->  ( Fun  f  /\  dom  f  =  x ) )
4 ancom 437 . . . . . . . . . 10  |-  ( ( Fun  f  /\  dom  f  =  x )  <->  ( dom  f  =  x  /\  Fun  f ) )
5 eqcom 2285 . . . . . . . . . . 11  |-  ( dom  f  =  x  <->  x  =  dom  f )
65anbi1i 676 . . . . . . . . . 10  |-  ( ( dom  f  =  x  /\  Fun  f )  <-> 
( x  =  dom  f  /\  Fun  f ) )
73, 4, 63bitri 262 . . . . . . . . 9  |-  ( f  Fn  x  <->  ( x  =  dom  f  /\  Fun  f ) )
87anbi1i 676 . . . . . . . 8  |-  ( ( 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 630 . . . . . . . 8  |-  ( ( ( 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 ) ) ) ) ) ) ) )
102, 8, 93bitri 262 . . . . . . 7  |-  ( ( 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 ) ) ) ) ) ) ) )
1110exbii 1569 . . . . . 6  |-  ( 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 2791 . . . . . . . 8  |-  f  e. 
_V
1312dmex 4941 . . . . . . 7  |-  dom  f  e.  _V
14 eleq1 2343 . . . . . . . . 9  |-  ( x  =  dom  f  -> 
( x  e.  On  <->  dom  f  e.  On ) )
15 raleq 2736 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
1614, 15anbi12d 691 . . . . . . . 8  |-  ( 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 ) ) ) ) ) ) )
1716anbi2d 684 . . . . . . 7  |-  ( 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 ) ) ) ) ) ) ) )
1813, 17ceqsexv 2823 . . . . . 6  |-  ( 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 ) ) ) ) ) ) )
1911, 18bitri 240 . . . . 5  |-  ( 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 2549 . . . . 5  |-  ( 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 3162 . . . . . 6  |-  ( 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 3358 . . . . . . . 8  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( f  e.  Funs  /\  f  e.  ( `'Domain " On ) ) )
2312elfuns 24454 . . . . . . . . 9  |-  ( f  e.  Funs  <->  Fun  f )
2412elima 5017 . . . . . . . . . 10  |-  ( f  e.  ( `'Domain " On ) 
<->  E. x  e.  On  x `'Domain f )
25 df-rex 2549 . . . . . . . . . 10  |-  ( E. x  e.  On  x `'Domain f  <->  E. x ( x  e.  On  /\  x `'Domain f ) )
26 ancom 437 . . . . . . . . . . . . 13  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x `'Domain f  /\  x  e.  On ) )
27 vex 2791 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
2827, 12brcnv 4864 . . . . . . . . . . . . . . 15  |-  ( x `'Domain f  <->  fDomain x )
2912, 27brdomain 24472 . . . . . . . . . . . . . . 15  |-  ( fDomain
x  <->  x  =  dom  f )
3028, 29bitri 240 . . . . . . . . . . . . . 14  |-  ( x `'Domain f  <->  x  =  dom  f )
3130anbi1i 676 . . . . . . . . . . . . 13  |-  ( ( x `'Domain f  /\  x  e.  On )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3226, 31bitri 240 . . . . . . . . . . . 12  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3332exbii 1569 . . . . . . . . . . 11  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  E. x
( x  =  dom  f  /\  x  e.  On ) )
3413, 14ceqsexv 2823 . . . . . . . . . . 11  |-  ( E. x ( x  =  dom  f  /\  x  e.  On )  <->  dom  f  e.  On )
3533, 34bitri 240 . . . . . . . . . 10  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  dom  f  e.  On )
3624, 25, 353bitri 262 . . . . . . . . 9  |-  ( f  e.  ( `'Domain " On ) 
<->  dom  f  e.  On )
3723, 36anbi12i 678 . . . . . . . 8  |-  ( ( f  e.  Funs  /\  f  e.  ( `'Domain " On ) )  <->  ( Fun  f  /\  dom  f  e.  On ) )
3822, 37bitri 240 . . . . . . 7  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( Fun  f  /\  dom  f  e.  On ) )
3938anbi1i 676 . . . . . 6  |-  ( ( 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 )
) ) ) ) ) ) )
40 brdif 4071 . . . . . . . . . . . . . . 15  |-  ( 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 ) )
41 vex 2791 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
4212, 41brco 4852 . . . . . . . . . . . . . . . . 17  |-  ( f ( `'  _E  o. Domain ) y  <->  E. x ( fDomain
x  /\  x `'  _E  y ) )
4329anbi1i 676 . . . . . . . . . . . . . . . . . . 19  |-  ( ( fDomain x  /\  x `'  _E  y )  <->  ( x  =  dom  f  /\  x `'  _E  y ) )
4443exbii 1569 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  E. x ( x  =  dom  f  /\  x `'  _E  y
) )
45 breq1 4026 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  dom  f  -> 
( x `'  _E  y 
<->  dom  f `'  _E  y ) )
4613, 45ceqsexv 2823 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( x  =  dom  f  /\  x `'  _E  y )  <->  dom  f `'  _E  y )
4744, 46bitri 240 . . . . . . . . . . . . . . . . 17  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  dom  f `'  _E  y )
4813, 41brcnv 4864 . . . . . . . . . . . . . . . . . 18  |-  ( dom  f `'  _E  y  <->  y  _E  dom  f )
4913epelc 4307 . . . . . . . . . . . . . . . . . 18  |-  ( y  _E  dom  f  <->  y  e.  dom  f )
5048, 49bitri 240 . . . . . . . . . . . . . . . . 17  |-  ( dom  f `'  _E  y  <->  y  e.  dom  f )
5142, 47, 503bitri 262 . . . . . . . . . . . . . . . 16  |-  ( f ( `'  _E  o. Domain ) y  <->  y  e.  dom  f )
5251anbi1i 676 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) )
5340, 52bitri 240 . . . . . . . . . . . . . 14  |-  ( 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 ) )
54 onelon 4417 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( dom  f  e.  On  /\  y  e.  dom  f
)  ->  y  e.  On )
55543adant1 973 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
y  e.  On )
56 brun 4069 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( <.
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 ) )
57 brxp 4720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( <. f ,  y >.  e.  ( _V  X.  { (/) } )  /\  x  e. 
{ U. { A } } ) )
58 opelxp 4719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  ( f  e.  _V  /\  y  e. 
{ (/) } ) )
5912, 58mpbiran 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  e.  {
(/) } )
60 elsn 3655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  { (/) }  <->  y  =  (/) )
6159, 60bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  =  (/) )
62 elsn 3655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  { U. { A } }  <->  x  =  U. { A } )
6361, 62anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
<. f ,  y >.  e.  ( _V  X.  { (/)
} )  /\  x  e.  { U. { A } } )  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
6457, 63bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
65 brun 4069 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( <.
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 ) )
6627brres 4961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( <. f ,  y >. ( Bigcup  o. Img ) x  /\  <.
f ,  y >.  e.  ( _V  X.  Limits ) ) )
67 opex 4237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  <. f ,  y >.  e.  _V
6867, 27brco 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  E. z ( <. f ,  y >.Img z  /\  z Bigcup x ) )
69 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  z  e. 
_V
7012, 41, 69brimg 24476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.Img z 
<->  z  =  ( f
" y ) )
7127brbigcup 24438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z
Bigcup x  <->  U. z  =  x )
7270, 71anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.Img z  /\  z Bigcup x )  <-> 
( z  =  ( f " y )  /\  U. z  =  x ) )
7372exbii 1569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( <. f ,  y >.Img z  /\  z Bigcup x )  <->  E. z
( z  =  ( f " y )  /\  U. z  =  x ) )
74 imaexg 5026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f  e.  _V  ->  (
f " y )  e.  _V )
7512, 74ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f
" y )  e. 
_V
76 unieq 3836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  ( f "
y )  ->  U. z  =  U. ( f "
y ) )
7776eqeq1d 2291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  ( f "
y )  ->  ( U. z  =  x  <->  U. ( f " y
)  =  x ) )
7875, 77ceqsexv 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  U. (
f " y )  =  x )
79 eqcom 2285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( U. ( f " y
)  =  x  <->  x  =  U. ( f " y
) )
8078, 79bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  x  =  U. ( f " y
) )
8168, 73, 803bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  x  =  U. ( f
" y ) )
82 opelxp 4719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
( f  e.  _V  /\  y  e.  Limits ) )
8312, 82mpbiran 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
y  e.  Limits )
8441ellimits 24450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  Limits 
<->  Lim  y )
8583, 84bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <->  Lim  y )
8681, 85anbi12ci 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
<. f ,  y >.
( Bigcup  o. Img ) x  /\  <. f ,  y
>.  e.  ( _V  X.  Limits ) )  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8766, 86bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8827brres 4961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.
( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) x  <->  ( <. f ,  y >. (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) ) x  /\  <. f ,  y >.  e.  ( _V  X.  ran Succ )
) )
8967, 27brco 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.
(FullFun F  o.  (Apply  o. pprod
(  _I  ,  Bigcup ) ) ) x  <->  E. a
( <. f ,  y
>. (Apply  o. pprod (  _I  ,  Bigcup ) ) a  /\  aFullFun F x ) )
90 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  a  e. 
_V
9167, 90brco 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  E. z
( <. f ,  y
>.pprod (  _I  ,  Bigcup ) z  /\  zApply a
) )
9212, 41, 69brpprod3a 24426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <->  E. a E. b ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b ) )
93 3anrot 939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( f  _I  a  /\  y Bigcup b  /\  z  = 
<. a ,  b >.
) )
9490ideq 4836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  _I  a  <->  f  =  a )
95 equcom 1647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  =  a  <->  a  =  f )
9694, 95bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( f  _I  a  <->  a  =  f )
97 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  b  e. 
_V
9897brbigcup 24438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y
Bigcup b  <->  U. y  =  b )
99 eqcom 2285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( U. y  =  b  <->  b  =  U. y )
10098, 99bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y
Bigcup b  <->  b  =  U. y )
101 biid 227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( z  =  <. a ,  b
>. 
<->  z  =  <. a ,  b >. )
10296, 100, 1013anbi123i 1140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f  _I  a  /\  y Bigcup b  /\  z  =  <. a ,  b
>. )  <->  ( a  =  f  /\  b  = 
U. y  /\  z  =  <. a ,  b
>. ) )
10393, 102bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b
>. ) )
1041032exbii 1570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 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
>. ) )
10541uniex 4516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  U. y  e.  _V
106 opeq1 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( a  =  f  ->  <. a ,  b >.  =  <. f ,  b >. )
107106eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( a  =  f  ->  (
z  =  <. a ,  b >.  <->  z  =  <. f ,  b >.
) )
108 opeq2 3797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( b  =  U. y  ->  <. f ,  b >.  =  <. f ,  U. y >. )
109108eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( b  =  U. y  -> 
( z  =  <. f ,  b >.  <->  z  =  <. f ,  U. y >. ) )
11012, 105, 107, 109ceqsex2v 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( E. a E. b ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b >. )  <->  z  =  <. f ,  U. y >. )
11192, 104, 1103bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <-> 
z  =  <. f ,  U. y >. )
112111anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
<. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <-> 
( z  =  <. f ,  U. y >.  /\  zApply a ) )
113112exbii 1569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( <. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <->  E. z
( z  =  <. f ,  U. y >.  /\  zApply a ) )
114 opex 4237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  <. f ,  U. y >.  e.  _V
115 breq1 4026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z  =  <. f ,  U. y >.  ->  ( zApply a 
<-> 
<. f ,  U. y >.Apply a ) )
116114, 115ceqsexv 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <->  <. f ,  U. y >.Apply a )
11712, 105, 90brapply 24477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( <.
f ,  U. y >.Apply a  <->  a  =  ( f `  U. y
) )
118116, 117bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <-> 
a  =  ( f `
 U. y ) )
11991, 113, 1183bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  a  =  ( f `  U. y ) )
12090, 27brfullfun 24486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( aFullFun
F x  <->  x  =  ( F `  a ) )
121119, 120anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  /\  aFullFun F x )  <->  ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) ) )
122121exbii 1569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. a ( <. f ,  y >. (Apply  o. pprod
(  _I  ,  Bigcup ) ) a  /\  aFullFun F x )  <->  E. a
( a  =  ( f `  U. y
)  /\  x  =  ( F `  a ) ) )
123 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f `
 U. y )  e.  _V
124 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( a  =  ( f `  U. y )  ->  ( F `  a )  =  ( F `  ( f `  U. y ) ) )
125124eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  =  ( f `  U. y )  ->  (
x  =  ( F `
 a )  <->  x  =  ( F `  ( f `
 U. y ) ) ) )
126123, 125ceqsexv 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. a ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) )  <->  x  =  ( F `  ( f `
 U. y ) ) )
12789, 122, 1263bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
(FullFun F  o.  (Apply  o. pprod
(  _I  ,  Bigcup ) ) ) x  <->  x  =  ( F `  ( f `
 U. y ) ) )
128 opelxp 4719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
( f  e.  _V  /\  y  e.  ran Succ )
)
12912, 128mpbiran 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
y  e.  ran Succ )
13041elrn 4919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ran Succ  <->  E. z  zSucc y )
13169, 41brsuccf 24480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( zSucc y  <->  y  =  suc  z )
132131exbii 1569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z  zSucc y  <->  E. z 
y  =  suc  z
)
133129, 130, 1323bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <->  E. z  y  =  suc  z )
134127, 133anbi12ci 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
<. f ,  y >.
(FullFun F  o.  (Apply  o. pprod
(  _I  ,  Bigcup ) ) ) x  /\  <.
f ,  y >.  e.  ( _V  X.  ran Succ ) )  <->  ( E. z 
y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
13588, 134bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
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 ) ) ) )
13687, 135orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
<. 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 ) ) ) ) )
13765, 136bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
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 ) ) ) ) )
13864, 137orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
<. 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 ) ) ) ) ) )
13956, 138bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
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 ) ) ) ) ) )
140 onzsl 4637 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  On  <->  ( y  =  (/)  \/  E. z  e.  On  y  =  suc  z  \/  ( y  e.  _V  /\  Lim  y
) ) )
141 nlim0 4450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  (/)
142 limeq 4404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  ( Lim  y  <->  Lim  (/) ) )
143141, 142mtbiri 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  Lim  y )
144143intnanrd 883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
145 nsuceq0 4472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  suc  z  =/=  (/)
146 neeq2 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  (/)  ->  ( suc  z  =/=  y  <->  suc  z  =/=  (/) ) )
147145, 146mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  (/)  ->  suc  z  =/=  y )
148147necomd 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  (/)  ->  y  =/= 
suc  z )
149148neneqd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  -.  y  =  suc  z )
150149nexdv 1857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  E. z  y  =  suc  z )
151150intnanrd 883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
152 ioran 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  ( ( 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 ) ) ) ) )
153144, 151, 152sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  -.  (
( Lim  y  /\  x  =  U. (
f " y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `
 U. y ) ) ) ) )
154 orel2 372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( -.  ( ( 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 } ) ) )
155153, 154syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 } ) ) )
156 iftrue 3571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  =  if ( A  e. 
_V ,  A ,  (/) ) )
157 unisnif 24464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  U. { A }  =  if ( A  e.  _V ,  A ,  (/) )
158156, 157syl6eqr 2333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. { A }
)
159158eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  <->  x  =  U. { A } ) )
160159biimprd 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  U. { A }  ->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
161160adantld 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  (/)  ->  ( ( y  =  (/)  /\  x  =  U. { A }
)  ->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
162155, 161syld 40 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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 ) ) ) ) ) )
163159biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  ->  x  =  U. { A } ) )
164163anc2li 540 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  -> 
( y  =  (/)  /\  x  =  U. { A } ) ) )
165 orc 374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  =  (/)  /\  x  =  U. { A }
)  ->  ( (
y  =  (/)  /\  x  =  U. { A }
)  \/  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) ) )
166164, 165syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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 ) ) ) ) ) ) )
167162, 166impbid 183 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) ) ) ) ) )
168 neeq1 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  suc  z  -> 
( y  =/=  (/)  <->  suc  z  =/=  (/) ) )
169145, 168mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
y  =/=  (/) )
170169neneqd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  y  =  (/) )
171170intnanrd 883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
172171rexlimivw 2663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
173 orel1 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( -.  ( 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 ) ) ) ) ) )
174172, 173syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) ) ) )
175 nlimsucg 4633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  _V  ->  -.  Lim  suc  z )
17669, 175ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  suc  z
177 limeq 4404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
( Lim  y  <->  Lim  suc  z
) )
178176, 177mtbiri 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  Lim  y )
179178rexlimivw 2663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  Lim  y )
180179intnanrd 883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
181 orel1 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( -.  ( 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 ) ) ) ) )
182180, 181syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) ) )
183 df-ne 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( suc  z  =/=  (/)  <->  -.  suc  z  =  (/) )
184145, 183mpbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  -.  suc  z  =  (/)
185 iffalse 3572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -. 
suc  z  =  (/)  ->  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 ) ) ) )
186184, 185ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  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
) ) )
187 iffalse 3572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -. 
Lim  suc  z  ->  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) ) )
18869, 175, 187mp2b 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) )
189186, 188eqtri 2303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  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
) )
190 eqeq1 2289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  suc  z  -> 
( y  =  (/)  <->  suc  z  =  (/) ) )
191 unieq 3836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  suc  z  ->  U. y  =  U. suc  z )
192191fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  suc  z  -> 
( f `  U. y )  =  ( f `  U. suc  z ) )
193192fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  suc  z  -> 
( F `  (
f `  U. y ) )  =  ( F `
 ( f `  U. suc  z ) ) )
194177, 193ifbieq2d 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 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
) ) ) )
195190, 194ifbieq2d 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 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 ) ) ) ) )
196189, 195, 1933eqtr4a 2341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  ->  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  =  ( F `
 ( f `  U. y ) ) )
197196rexlimivw 2663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) ) )
198197eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) ) ) )
199198biimprd 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) ) ) ) )
200199adantld 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) ) ) )
201174, 182, 2003syld 51 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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 ) ) ) ) ) )
202 rexex 2602 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. z  e.  On  y  =  suc  z  ->  E. z 
y  =  suc  z
)
203198biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) )
204 olc 373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 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 ) ) ) ) )
205204olcd 382 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 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 ) ) ) ) ) )
206202, 203, 205ee12an 1353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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 ) ) ) ) ) ) )
207201, 206impbid 183 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) ) ) ) ) )
208143con2i 112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  y  =  (/) )
209208intnanrd 883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  (
y  =  (/)  /\  x  =  U. { A }
) )
210209, 173syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) ) ) ) )
211178exlimiv 1666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z  y  =  suc  z  ->  -.  Lim  y )
212211con2i 112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  E. z 
y  =  suc  z
)
213212intnanrd 883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
214 orel2 372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  ( 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
) ) ) )
215213, 214syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Lim  y  ->  ( (
( Lim  y  /\  x  =  U. (
f " y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `
 U. y ) ) ) )  -> 
( Lim  y  /\  x  =  U. (
f " y ) ) ) )
216 iffalse 3572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( -.  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 ) ) ) )
217208, 216syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 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 ) ) ) )
218 iftrue 3571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( Lim  y  ->  if ( Lim  y ,  U. (
f " y ) ,  ( F `  ( f `  U. y ) ) )  =  U. ( f
" y ) )
219217, 218eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Lim  y  ->  if (
y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. ( f "
y ) )
220219eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  <->  x  =  U. ( f " y
) ) )
221220biimprd 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  ( x  =  U. ( f "
y )  ->  x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
222221adantld 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) ) ) ) )
223210, 215, 2223syld 51 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) ) ) )
224223adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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 ) ) ) ) ) )
225220biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  ->  x  =  U. ( f " y
) ) )
226225anc2li 540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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
) ) ) )
227 orc 374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  -> 
( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )
228227olcd 382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 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 ) ) ) ) ) )
229226, 228syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) ) ) ) )
230229adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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 ) ) ) ) ) ) )
231224, 230impbid 183 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 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 ) ) ) ) ) )
232167, 207, 2313jaoi 1245 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 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 ) ) ) ) ) )
233140, 232sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) ) ) ) )
234139, 233syl5bb 248 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) ) ) ) ) )
23555, 234syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 ) ) ) ) ) )
23627, 67brcnv 4864 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x `'Apply <. f ,  y
>. 
<-> 
<. f ,  y >.Apply x )
23712, 41, 27brapply 24477 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
f ,  y >.Apply x 
<->  x  =  ( f `
 y ) )
238236, 237bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x `'Apply <. f ,  y
>. 
<->  x  =  ( f `
 y ) )
239238a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( x `'Apply <. f ,  y >.  <->  x  =  ( f `  y
) ) )
240235, 239anbi12d 691 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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
) ) ) )
241 ancom 437 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  /\  x  =  ( f `  y ) )  <->  ( x  =  ( f `  y )  /\  x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
242240, 241syl6bb 252 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) ) ) ) ) )
243242exbidv 1612 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) ) ) ) ) )
244 df-br 4024 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 )
) ) ) ) )
24567elfix 24443 . . . . . . . . . . . . . . . . . . . 20  |-  ( <.
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 >. )
24667, 67brco 4852 . . . . . . . . . . . . . . . . . . . 20  |-  ( <.
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 >. )
)
247244, 245, 2463bitri 262 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 >. )
)
248 fvex 5539 . . . . . . . . . . . . . . . . . . . 20  |-  ( f `
 y )  e. 
_V
249248eqvinc 2895 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) ) ) ) )
250243, 247, 2493bitr4g 279 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) ) ) )
251250notbid 285 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) ) ) ) ) )
2522513expia 1153 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) ) ) ) )
253252pm5.32d 620 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) ) ) ) ) )
254 annim 414 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) ) ) ) )
255253, 254syl6bb 252 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) ) ) ) ) )
25653, 255syl5bb 248 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) ) ) ) )
257256exbidv 1612 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) ) ) ) )
258 exnal 1561 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) ) )
259257, 258syl6rbb 253 . . . . . . . . . . 11  |-  ( ( 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 ) )
26012eldm 4876 . . . . . . . . . . 11  |-  ( 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 )
261259, 260syl6bbr 254 . . . . . . . . . 10  |-  ( ( 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 )
) ) ) ) ) ) )
262261con1bid 320 . . . . . . . . 9  |-  ( ( 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 ) ) ) ) ) ) )
263 df-ral 2548 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
264262, 263syl6bbr 254 . . . . . . . 8  |-  ( ( 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 ) ) ) ) ) )
265264pm5.32i 618 . . . . . . 7  |-  ( ( ( 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 ) ) ) ) ) )
266 anass 630 . . . . . . 7  |-  ( ( ( 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 ) ) ) ) ) ) )
267265, 266bitri 240 . . . . . 6  |-  ( ( ( 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 ) ) ) ) ) ) )
26821, 39, 2673bitri 262 . . . . 5  |-  ( 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 ) ) ) ) ) ) )
26919, 20, 2683bitr4ri 269 . . . 4  |-  ( 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 ) ) ) ) ) )
270269abbi2i 2394 . . 3  |-  ( (
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 ) ) ) ) ) }
271270unieqi 3837 . 2  |-  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 ) ) ) ) ) }
2721, 271eqtr4i 2306 1  |-  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 )
) ) ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    \/ w3o 933    /\ w3a 934   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684   {cab 2269    =/= wne 2446   A.wral 2543   E.wrex 2544   _Vcvv 2788    \ cdif 3149    u. cun 3150    i^i cin 3151   (/)c0 3455   ifcif 3565   {csn 3640   <.cop 3643   U.cuni 3827   class class class wbr 4023    _E cep 4303    _I cid 4304   Oncon0 4392   Lim wlim 4393   suc csuc 4394    X. cxp 4687   `'ccnv 4688   dom cdm 4689   ran crn 4690    |` cres 4691   "cima 4692    o. ccom 4693   Fun wfun 5249    Fn wfn 5250   ` cfv 5255   reccrdg 6422  pprodcpprod 24374   Bigcupcbigcup 24377   Fixcfix 24378   Limitsclimits 24379   Funscfuns 24380  Imgcimg 24385  Domaincdomain 24386  Applycapply 24388  Succcsuccf 24391  FullFuncfullfn 24393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-1st 6122  df-2nd 6123  df-recs 6388  df-rdg 6423  df-symdif 24362  df-txp 24395  df-pprod 24396  df-bigcup 24399  df-fix 24400  df-limits 24401  df-funs 24402  df-singleton 24403  df-singles 24404  df-image 24405  df-cart 24406  df-img 24407  df-domain 24408  df-cup 24410  df-succf 24413  df-apply 24414  df-funpart 24415  df-fullfun 24416
  Copyright terms: Public domain W3C validator