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

Theorem dfrdg4 25711
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 25375 . 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 773 . . . . . . . 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 5424 . . . . . . . . . 10  |-  ( f  Fn  x  <->  ( Fun  f  /\  dom  f  =  x ) )
4 ancom 438 . . . . . . . . . 10  |-  ( ( Fun  f  /\  dom  f  =  x )  <->  ( dom  f  =  x  /\  Fun  f ) )
5 eqcom 2414 . . . . . . . . . . 11  |-  ( dom  f  =  x  <->  x  =  dom  f )
65anbi1i 677 . . . . . . . . . 10  |-  ( ( dom  f  =  x  /\  Fun  f )  <-> 
( x  =  dom  f  /\  Fun  f ) )
73, 4, 63bitri 263 . . . . . . . . 9  |-  ( f  Fn  x  <->  ( x  =  dom  f  /\  Fun  f ) )
87anbi1i 677 . . . . . . . 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 631 . . . . . . . 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 263 . . . . . . 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 1589 . . . . . 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 2927 . . . . . . . 8  |-  f  e. 
_V
1312dmex 5099 . . . . . . 7  |-  dom  f  e.  _V
14 eleq1 2472 . . . . . . . . 9  |-  ( x  =  dom  f  -> 
( x  e.  On  <->  dom  f  e.  On ) )
15 raleq 2872 . . . . . . . . 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 692 . . . . . . . 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 685 . . . . . . 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 2959 . . . . . 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 241 . . . . 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 2680 . . . . 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 3298 . . . . . 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 3498 . . . . . . . 8  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( f  e.  Funs  /\  f  e.  ( `'Domain " On ) ) )
2312elfuns 25676 . . . . . . . . 9  |-  ( f  e.  Funs  <->  Fun  f )
2412elima 5175 . . . . . . . . . 10  |-  ( f  e.  ( `'Domain " On ) 
<->  E. x  e.  On  x `'Domain f )
25 df-rex 2680 . . . . . . . . . 10  |-  ( E. x  e.  On  x `'Domain f  <->  E. x ( x  e.  On  /\  x `'Domain f ) )
26 ancom 438 . . . . . . . . . . . . 13  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x `'Domain f  /\  x  e.  On ) )
27 vex 2927 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
2827, 12brcnv 5022 . . . . . . . . . . . . . . 15  |-  ( x `'Domain f  <->  fDomain x )
2912, 27brdomain 25694 . . . . . . . . . . . . . . 15  |-  ( fDomain
x  <->  x  =  dom  f )
3028, 29bitri 241 . . . . . . . . . . . . . 14  |-  ( x `'Domain f  <->  x  =  dom  f )
3130anbi1i 677 . . . . . . . . . . . . 13  |-  ( ( x `'Domain f  /\  x  e.  On )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3226, 31bitri 241 . . . . . . . . . . . 12  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3332exbii 1589 . . . . . . . . . . 11  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  E. x
( x  =  dom  f  /\  x  e.  On ) )
3413, 14ceqsexv 2959 . . . . . . . . . . 11  |-  ( E. x ( x  =  dom  f  /\  x  e.  On )  <->  dom  f  e.  On )
3533, 34bitri 241 . . . . . . . . . 10  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  dom  f  e.  On )
3624, 25, 353bitri 263 . . . . . . . . 9  |-  ( f  e.  ( `'Domain " On ) 
<->  dom  f  e.  On )
3723, 36anbi12i 679 . . . . . . . 8  |-  ( ( f  e.  Funs  /\  f  e.  ( `'Domain " On ) )  <->  ( Fun  f  /\  dom  f  e.  On ) )
3822, 37bitri 241 . . . . . . 7  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( Fun  f  /\  dom  f  e.  On ) )
3938anbi1i 677 . . . . . 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 4228 . . . . . . . . . . . . . . 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 2927 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
4212, 41brco 5010 . . . . . . . . . . . . . . . . 17  |-  ( f ( `'  _E  o. Domain ) y  <->  E. x ( fDomain
x  /\  x `'  _E  y ) )
4329anbi1i 677 . . . . . . . . . . . . . . . . . . 19  |-  ( ( fDomain x  /\  x `'  _E  y )  <->  ( x  =  dom  f  /\  x `'  _E  y ) )
4443exbii 1589 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  E. x ( x  =  dom  f  /\  x `'  _E  y
) )
45 breq1 4183 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  dom  f  -> 
( x `'  _E  y 
<->  dom  f `'  _E  y ) )
4613, 45ceqsexv 2959 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( x  =  dom  f  /\  x `'  _E  y )  <->  dom  f `'  _E  y )
4744, 46bitri 241 . . . . . . . . . . . . . . . . 17  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  dom  f `'  _E  y )
4813, 41brcnv 5022 . . . . . . . . . . . . . . . . . 18  |-  ( dom  f `'  _E  y  <->  y  _E  dom  f )
4913epelc 4464 . . . . . . . . . . . . . . . . . 18  |-  ( y  _E  dom  f  <->  y  e.  dom  f )
5048, 49bitri 241 . . . . . . . . . . . . . . . . 17  |-  ( dom  f `'  _E  y  <->  y  e.  dom  f )
5142, 47, 503bitri 263 . . . . . . . . . . . . . . . 16  |-  ( f ( `'  _E  o. Domain ) y  <->  y  e.  dom  f )
5251anbi1i 677 . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . 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 4574 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( dom  f  e.  On  /\  y  e.  dom  f
)  ->  y  e.  On )
55543adant1 975 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
y  e.  On )
56 brun 4226 . . . . . . . . . . . . . . . . . . . . . . . . 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 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( <. f ,  y >.  e.  ( _V  X.  { (/) } )  /\  x  e. 
{ U. { A } } ) )
58 opelxp 4875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  ( f  e.  _V  /\  y  e. 
{ (/) } ) )
5912, 58mpbiran 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  e.  {
(/) } )
60 elsn 3797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  { (/) }  <->  y  =  (/) )
6159, 60bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  =  (/) )
62 elsn 3797 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  { U. { A } }  <->  x  =  U. { A } )
6361, 62anbi12i 679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
<. f ,  y >.  e.  ( _V  X.  { (/)
} )  /\  x  e.  { U. { A } } )  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
6457, 63bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
65 brun 4226 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( <. f ,  y >. ( Bigcup  o. Img ) x  /\  <.
f ,  y >.  e.  ( _V  X.  Limits ) ) )
67 opex 4395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  <. f ,  y >.  e.  _V
6867, 27brco 5010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  E. z ( <. f ,  y >.Img z  /\  z Bigcup x ) )
69 vex 2927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  z  e. 
_V
7012, 41, 69brimg 25698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.Img z 
<->  z  =  ( f
" y ) )
7127brbigcup 25660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z
Bigcup x  <->  U. z  =  x )
7270, 71anbi12i 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.Img z  /\  z Bigcup x )  <-> 
( z  =  ( f " y )  /\  U. z  =  x ) )
7372exbii 1589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( <. f ,  y >.Img z  /\  z Bigcup x )  <->  E. z
( z  =  ( f " y )  /\  U. z  =  x ) )
74 imaexg 5184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f  e.  _V  ->  (
f " y )  e.  _V )
7512, 74ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f
" y )  e. 
_V
76 unieq 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  ( f "
y )  ->  U. z  =  U. ( f "
y ) )
7776eqeq1d 2420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  ( f "
y )  ->  ( U. z  =  x  <->  U. ( f " y
)  =  x ) )
7875, 77ceqsexv 2959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  U. (
f " y )  =  x )
79 eqcom 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( U. ( f " y
)  =  x  <->  x  =  U. ( f " y
) )
8078, 79bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  x  =  U. ( f " y
) )
8168, 73, 803bitri 263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  x  =  U. ( f
" y ) )
82 opelxp 4875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
( f  e.  _V  /\  y  e.  Limits ) )
8312, 82mpbiran 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
y  e.  Limits )
8441ellimits 25672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  Limits 
<->  Lim  y )
8583, 84bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <->  Lim  y )
8681, 85anbi12ci 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
<. f ,  y >.
( Bigcup  o. Img ) x  /\  <. f ,  y
>.  e.  ( _V  X.  Limits ) )  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8766, 86bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8827brres 5119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  a  e. 
_V
9167, 90brco 5010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  E. z
( <. f ,  y
>.pprod (  _I  ,  Bigcup ) z  /\  zApply a
) )
9212, 41, 69brpprod3a 25648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <->  E. a E. b ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b ) )
93 3anrot 941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( f  _I  a  /\  y Bigcup b  /\  z  = 
<. a ,  b >.
) )
9490ideq 4992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  _I  a  <->  f  =  a )
95 equcom 1688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  =  a  <->  a  =  f )
9694, 95bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( f  _I  a  <->  a  =  f )
97 vex 2927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  b  e. 
_V
9897brbigcup 25660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y
Bigcup b  <->  U. y  =  b )
99 eqcom 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( U. y  =  b  <->  b  =  U. y )
10098, 99bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y
Bigcup b  <->  b  =  U. y )
101 biid 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( z  =  <. a ,  b
>. 
<->  z  =  <. a ,  b >. )
10296, 100, 1013anbi123i 1142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f  _I  a  /\  y Bigcup b  /\  z  =  <. a ,  b
>. )  <->  ( a  =  f  /\  b  = 
U. y  /\  z  =  <. a ,  b
>. ) )
10393, 102bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b
>. ) )
1041032exbii 1590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  U. y  e.  _V
106 opeq1 3952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( a  =  f  ->  <. a ,  b >.  =  <. f ,  b >. )
107106eqeq2d 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( a  =  f  ->  (
z  =  <. a ,  b >.  <->  z  =  <. f ,  b >.
) )
108 opeq2 3953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( b  =  U. y  ->  <. f ,  b >.  =  <. f ,  U. y >. )
109108eqeq2d 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( b  =  U. y  -> 
( z  =  <. f ,  b >.  <->  z  =  <. f ,  U. y >. ) )
11012, 105, 107, 109ceqsex2v 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( E. a E. b ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b >. )  <->  z  =  <. f ,  U. y >. )
11192, 104, 1103bitri 263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <-> 
z  =  <. f ,  U. y >. )
112111anbi1i 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
<. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <-> 
( z  =  <. f ,  U. y >.  /\  zApply a ) )
113112exbii 1589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( <. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <->  E. z
( z  =  <. f ,  U. y >.  /\  zApply a ) )
114 opex 4395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  <. f ,  U. y >.  e.  _V
115 breq1 4183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z  =  <. f ,  U. y >.  ->  ( zApply a 
<-> 
<. f ,  U. y >.Apply a ) )
116114, 115ceqsexv 2959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <->  <. f ,  U. y >.Apply a )
11712, 105, 90brapply 25699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( <.
f ,  U. y >.Apply a  <->  a  =  ( f `  U. y
) )
118116, 117bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <-> 
a  =  ( f `
 U. y ) )
11991, 113, 1183bitri 263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  a  =  ( f `  U. y ) )
12090, 27brfullfun 25709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( aFullFun
F x  <->  x  =  ( F `  a ) )
121119, 120anbi12i 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  /\  aFullFun F x )  <->  ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) ) )
122121exbii 1589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f `
 U. y )  e.  _V
124 fveq2 5695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( a  =  ( f `  U. y )  ->  ( F `  a )  =  ( F `  ( f `  U. y ) ) )
125124eqeq2d 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  =  ( f `  U. y )  ->  (
x  =  ( F `
 a )  <->  x  =  ( F `  ( f `
 U. y ) ) ) )
126123, 125ceqsexv 2959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. a ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) )  <->  x  =  ( F `  ( f `
 U. y ) ) )
12789, 122, 1263bitri 263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
(FullFun F  o.  (Apply  o. pprod
(  _I  ,  Bigcup ) ) ) x  <->  x  =  ( F `  ( f `
 U. y ) ) )
128 opelxp 4875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
( f  e.  _V  /\  y  e.  ran Succ )
)
12912, 128mpbiran 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
y  e.  ran Succ )
13041elrn 5077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ran Succ  <->  E. z  zSucc y )
13169, 41brsuccf 25702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( zSucc y  <->  y  =  suc  z )
132131exbii 1589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z  zSucc y  <->  E. z 
y  =  suc  z
)
133129, 130, 1323bitri 263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <->  E. z  y  =  suc  z )
134127, 133anbi12ci 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 508 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . . . . . . . . . . . . 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 508 . . . . . . . . . . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . . . . . . . . . . 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 4793 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  On  <->  ( y  =  (/)  \/  E. z  e.  On  y  =  suc  z  \/  ( y  e.  _V  /\  Lim  y
) ) )
141 nlim0 4607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  (/)
142 limeq 4561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  ( Lim  y  <->  Lim  (/) ) )
143141, 142mtbiri 295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  Lim  y )
144143intnanrd 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
145 nsuceq0 4629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  suc  z  =/=  (/)
146 neeq2 2584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  (/)  ->  ( suc  z  =/=  y  <->  suc  z  =/=  (/) ) )
147145, 146mpbiri 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  (/)  ->  suc  z  =/=  y )
148147necomd 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  (/)  ->  y  =/= 
suc  z )
149148neneqd 2591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  -.  y  =  suc  z )
150149nexdv 1937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  E. z  y  =  suc  z )
151150intnanrd 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
152 ioran 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  -.  (
( Lim  y  /\  x  =  U. (
f " y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `
 U. y ) ) ) ) )
154 orel2 373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 25686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  U. { A }  =  if ( A  e.  _V ,  A ,  (/) )
158156, 157syl6eqr 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. { A }
)
159158eqeq2d 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  <->  x  =  U. { A } ) )
160159biimprd 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  U. { A }  ->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
161160adantld 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 42 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  ->  x  =  U. { A } ) )
164163anc2li 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 375 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 31 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 184 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  suc  z  -> 
( y  =/=  (/)  <->  suc  z  =/=  (/) ) )
169145, 168mpbiri 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
y  =/=  (/) )
170169neneqd 2591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  y  =  (/) )
171170intnanrd 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
172171rexlimivw 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
173 orel1 372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  _V  ->  -.  Lim  suc  z )
17669, 175ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  suc  z
177 limeq 4561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
( Lim  y  <->  Lim  suc  z
) )
178176, 177mtbiri 295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  Lim  y )
179178rexlimivw 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  Lim  y )
180179intnanrd 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
181 orel1 372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( suc  z  =/=  (/)  <->  -.  suc  z  =  (/) )
184145, 183mpbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  -.  suc  z  =  (/)
185 iffalse 3714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -. 
Lim  suc  z  ->  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) ) )
18869, 175, 187mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) )
189186, 188eqtri 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  suc  z  -> 
( y  =  (/)  <->  suc  z  =  (/) ) )
191 unieq 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  suc  z  ->  U. y  =  U. suc  z )
192191fveq2d 5699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  suc  z  -> 
( f `  U. y )  =  ( f `  U. suc  z ) )
193192fveq2d 5699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  suc  z  -> 
( F `  (
f `  U. y ) )  =  ( F `
 ( f `  U. suc  z ) ) )
194177, 193ifbieq2d 3727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 53 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. z  e.  On  y  =  suc  z  ->  E. z 
y  =  suc  z
)
203198biimpd 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 383 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 184 . . . . . . . . . . . . . . . . . . . . . . . . . 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 114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  y  =  (/) )
209208intnanrd 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  (
y  =  (/)  /\  x  =  U. { A }
) )
210209, 173syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z  y  =  suc  z  ->  -.  Lim  y )
212211con2i 114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  E. z 
y  =  suc  z
)
213212intnanrd 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
214 orel2 373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( Lim  y  ->  if ( Lim  y ,  U. (
f " y ) ,  ( F `  ( f `  U. y ) ) )  =  U. ( f
" y ) )
219217, 218eqtrd 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Lim  y  ->  if (
y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. ( f "
y ) )
220219eqeq2d 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 53 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  -> 
( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )
228227olcd 383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 184 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1247 . . . . . . . . . . . . . . . . . . . . . . . . 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 188 . . . . . . . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . 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 5022 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x `'Apply <. f ,  y
>. 
<-> 
<. f ,  y >.Apply x )
23712, 41, 27brapply 25699 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
f ,  y >.Apply x 
<->  x  =  ( f `
 y ) )
238236, 237bitri 241 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x `'Apply <. f ,  y
>. 
<->  x  =  ( f `
 y ) )
239238a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( x `'Apply <. f ,  y >.  <->  x  =  ( f `  y
) ) )
240235, 239anbi12d 692 . . . . . . . . . . . . . . . . . . . . 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 438 . . . . . . . . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . . . . . . . . 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 1633 . . . . . . . . . . . . . . . . . . 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 4181 . . . . . . . . . . . . . . . . . . . 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 25665 . . . . . . . . . . . . . . . . . . . 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 5010 . . . . . . . . . . . . . . . . . . . 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 263 . . . . . . . . . . . . . . . . . . 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 5709 . . . . . . . . . . . . . . . . . . . 20  |-  ( f `
 y )  e. 
_V
249248eqvinc 3031 . . . . . . . . . . . . . . . . . . 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 280 . . . . . . . . . . . . . . . . . 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 286 . . . . . . . . . . . . . . . . 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 1155 . . . . . . . . . . . . . . . 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 621 . . . . . . . . . . . . . . 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 415 . . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . 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 1633 . . . . . . . . . . . 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 1580 . . . . . . . . . . . 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 254 . . . . . . . . . . 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 5034 . . . . . . . . . . 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 255 . . . . . . . . . 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 321 . . . . . . . . 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 2679 . . . . . . . . 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 255 . . . . . . . 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 619 . . . . . . 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 631 . . . . . . 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 241 . . . . . 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 263 . . . . 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 270 . . . 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 2523 . . 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 3993 . 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 2435 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 177    \/ wo 358    /\ wa 359    \/ w3o 935    /\ w3a 936   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1721   {cab 2398    =/= wne 2575   A.wral 2674   E.wrex 2675   _Vcvv 2924    \ cdif 3285    u. cun 3286    i^i cin 3287   (/)c0 3596   ifcif 3707   {csn 3782   <.cop 3785   U.cuni 3983   class class class wbr 4180    _E cep 4460    _I cid 4461   Oncon0 4549   Lim wlim 4550   suc csuc 4551    X. cxp 4843   `'ccnv 4844   dom cdm 4845   ran crn 4846    |` cres 4847   "cima 4848    o. ccom 4849   Fun wfun 5415    Fn wfn 5416   ` cfv 5421   reccrdg 6634  pprodcpprod 25596   Bigcupcbigcup 25599   Fixcfix 25600   Limitsclimits 25601   Funscfuns 25602  Imgcimg 25607  Domaincdomain 25608  Applycapply 25610  Succcsuccf 25613  FullFuncfullfn 25615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-1st 6316  df-2nd 6317  df-recs 6600  df-rdg 6635  df-symdif 25584  df-txp 25617  df-pprod 25618  df-bigcup 25621  df-fix 25622  df-limits 25623  df-funs 25624  df-singleton 25625  df-singles 25626  df-image 25627  df-cart 25628  df-img 25629  df-domain 25630  df-cup 25632  df-succf 25635  df-apply 25636  df-funpart 25637  df-fullfun 25638
  Copyright terms: Public domain W3C validator