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

Theorem dfrdg4 28003
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 27632 . 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 795 . . . . . . . 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 5442 . . . . . . . . . 10  |-  ( f  Fn  x  <->  ( Fun  f  /\  dom  f  =  x ) )
4 ancom 450 . . . . . . . . . 10  |-  ( ( Fun  f  /\  dom  f  =  x )  <->  ( dom  f  =  x  /\  Fun  f ) )
5 eqcom 2445 . . . . . . . . . . 11  |-  ( dom  f  =  x  <->  x  =  dom  f )
65anbi1i 695 . . . . . . . . . 10  |-  ( ( dom  f  =  x  /\  Fun  f )  <-> 
( x  =  dom  f  /\  Fun  f ) )
73, 4, 63bitri 271 . . . . . . . . 9  |-  ( f  Fn  x  <->  ( x  =  dom  f  /\  Fun  f ) )
87anbi1i 695 . . . . . . . 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 649 . . . . . . . 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 271 . . . . . . 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 1634 . . . . . 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 2996 . . . . . . . 8  |-  f  e. 
_V
1312dmex 6532 . . . . . . 7  |-  dom  f  e.  _V
14 eleq1 2503 . . . . . . . . 9  |-  ( x  =  dom  f  -> 
( x  e.  On  <->  dom  f  e.  On ) )
15 raleq 2938 . . . . . . . . 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 710 . . . . . . . 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 703 . . . . . . 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 3030 . . . . . 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 249 . . . . 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 2742 . . . . 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 3359 . . . . . 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 3560 . . . . . . . 8  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( f  e.  Funs  /\  f  e.  ( `'Domain " On ) ) )
2312elfuns 27968 . . . . . . . . 9  |-  ( f  e.  Funs  <->  Fun  f )
2412elima 5195 . . . . . . . . . 10  |-  ( f  e.  ( `'Domain " On ) 
<->  E. x  e.  On  x `'Domain f )
25 df-rex 2742 . . . . . . . . . 10  |-  ( E. x  e.  On  x `'Domain f  <->  E. x ( x  e.  On  /\  x `'Domain f ) )
26 ancom 450 . . . . . . . . . . . . 13  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x `'Domain f  /\  x  e.  On ) )
27 vex 2996 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
2827, 12brcnv 5043 . . . . . . . . . . . . . . 15  |-  ( x `'Domain f  <->  fDomain x )
2912, 27brdomain 27986 . . . . . . . . . . . . . . 15  |-  ( fDomain
x  <->  x  =  dom  f )
3028, 29bitri 249 . . . . . . . . . . . . . 14  |-  ( x `'Domain f  <->  x  =  dom  f )
3130anbi1i 695 . . . . . . . . . . . . 13  |-  ( ( x `'Domain f  /\  x  e.  On )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3226, 31bitri 249 . . . . . . . . . . . 12  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3332exbii 1634 . . . . . . . . . . 11  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  E. x
( x  =  dom  f  /\  x  e.  On ) )
3413, 14ceqsexv 3030 . . . . . . . . . . 11  |-  ( E. x ( x  =  dom  f  /\  x  e.  On )  <->  dom  f  e.  On )
3533, 34bitri 249 . . . . . . . . . 10  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  dom  f  e.  On )
3624, 25, 353bitri 271 . . . . . . . . 9  |-  ( f  e.  ( `'Domain " On ) 
<->  dom  f  e.  On )
3723, 36anbi12i 697 . . . . . . . 8  |-  ( ( f  e.  Funs  /\  f  e.  ( `'Domain " On ) )  <->  ( Fun  f  /\  dom  f  e.  On ) )
3822, 37bitri 249 . . . . . . 7  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( Fun  f  /\  dom  f  e.  On ) )
3938anbi1i 695 . . . . . 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 4363 . . . . . . . . . . . . . . 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 2996 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
4212, 41brco 5031 . . . . . . . . . . . . . . . . 17  |-  ( f ( `'  _E  o. Domain ) y  <->  E. x ( fDomain
x  /\  x `'  _E  y ) )
4329anbi1i 695 . . . . . . . . . . . . . . . . . . 19  |-  ( ( fDomain x  /\  x `'  _E  y )  <->  ( x  =  dom  f  /\  x `'  _E  y ) )
4443exbii 1634 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  E. x ( x  =  dom  f  /\  x `'  _E  y
) )
45 breq1 4316 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  dom  f  -> 
( x `'  _E  y 
<->  dom  f `'  _E  y ) )
4613, 45ceqsexv 3030 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( x  =  dom  f  /\  x `'  _E  y )  <->  dom  f `'  _E  y )
4744, 46bitri 249 . . . . . . . . . . . . . . . . 17  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  dom  f `'  _E  y )
4813, 41brcnv 5043 . . . . . . . . . . . . . . . . . 18  |-  ( dom  f `'  _E  y  <->  y  _E  dom  f )
4913epelc 4655 . . . . . . . . . . . . . . . . . 18  |-  ( y  _E  dom  f  <->  y  e.  dom  f )
5048, 49bitri 249 . . . . . . . . . . . . . . . . 17  |-  ( dom  f `'  _E  y  <->  y  e.  dom  f )
5142, 47, 503bitri 271 . . . . . . . . . . . . . . . 16  |-  ( f ( `'  _E  o. Domain ) y  <->  y  e.  dom  f )
5251anbi1i 695 . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . 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 4765 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( dom  f  e.  On  /\  y  e.  dom  f
)  ->  y  e.  On )
55543adant1 1006 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
y  e.  On )
56 brun 4361 . . . . . . . . . . . . . . . . . . . . . . . . 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 4891 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( <. f ,  y >.  e.  ( _V  X.  { (/) } )  /\  x  e. 
{ U. { A } } ) )
58 opelxp 4890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  ( f  e.  _V  /\  y  e. 
{ (/) } ) )
5912, 58mpbiran 909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  e.  {
(/) } )
60 elsn 3912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  { (/) }  <->  y  =  (/) )
6159, 60bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  =  (/) )
62 elsn 3912 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  { U. { A } }  <->  x  =  U. { A } )
6361, 62anbi12i 697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
<. f ,  y >.  e.  ( _V  X.  { (/)
} )  /\  x  e.  { U. { A } } )  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
6457, 63bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
65 brun 4361 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( <. f ,  y >. ( Bigcup  o. Img ) x  /\  <.
f ,  y >.  e.  ( _V  X.  Limits ) ) )
67 opex 4577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  <. f ,  y >.  e.  _V
6867, 27brco 5031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  E. z ( <. f ,  y >.Img z  /\  z Bigcup x ) )
69 vex 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  z  e. 
_V
7012, 41, 69brimg 27990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.Img z 
<->  z  =  ( f
" y ) )
7127brbigcup 27951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z
Bigcup x  <->  U. z  =  x )
7270, 71anbi12i 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.Img z  /\  z Bigcup x )  <-> 
( z  =  ( f " y )  /\  U. z  =  x ) )
7372exbii 1634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( <. f ,  y >.Img z  /\  z Bigcup x )  <->  E. z
( z  =  ( f " y )  /\  U. z  =  x ) )
74 imaexg 6536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f  e.  _V  ->  (
f " y )  e.  _V )
7512, 74ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f
" y )  e. 
_V
76 unieq 4120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  ( f "
y )  ->  U. z  =  U. ( f "
y ) )
7776eqeq1d 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  ( f "
y )  ->  ( U. z  =  x  <->  U. ( f " y
)  =  x ) )
7875, 77ceqsexv 3030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  U. (
f " y )  =  x )
79 eqcom 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( U. ( f " y
)  =  x  <->  x  =  U. ( f " y
) )
8078, 79bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  x  =  U. ( f " y
) )
8168, 73, 803bitri 271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  x  =  U. ( f
" y ) )
82 opelxp 4890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
( f  e.  _V  /\  y  e.  Limits ) )
8312, 82mpbiran 909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
y  e.  Limits )
8441ellimits 27963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  Limits 
<->  Lim  y )
8583, 84bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <->  Lim  y )
8681, 85anbi12ci 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
<. f ,  y >.
( Bigcup  o. Img ) x  /\  <. f ,  y
>.  e.  ( _V  X.  Limits ) )  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8766, 86bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8827brres 5138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  a  e. 
_V
9167, 90brco 5031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  E. z
( <. f ,  y
>.pprod (  _I  ,  Bigcup ) z  /\  zApply a
) )
9212, 41, 69brpprod3a 27939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <->  E. a E. b ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b ) )
93 3anrot 970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( f  _I  a  /\  y Bigcup b  /\  z  = 
<. a ,  b >.
) )
9490ideq 5013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  _I  a  <->  f  =  a )
95 equcom 1732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  =  a  <->  a  =  f )
9694, 95bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( f  _I  a  <->  a  =  f )
97 vex 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  b  e. 
_V
9897brbigcup 27951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y
Bigcup b  <->  U. y  =  b )
99 eqcom 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( U. y  =  b  <->  b  =  U. y )
10098, 99bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y
Bigcup b  <->  b  =  U. y )
101 biid 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( z  =  <. a ,  b
>. 
<->  z  =  <. a ,  b >. )
10296, 100, 1013anbi123i 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f  _I  a  /\  y Bigcup b  /\  z  =  <. a ,  b
>. )  <->  ( a  =  f  /\  b  = 
U. y  /\  z  =  <. a ,  b
>. ) )
10393, 102bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b
>. ) )
1041032exbii 1635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  U. y  e.  _V
106 opeq1 4080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( a  =  f  ->  <. a ,  b >.  =  <. f ,  b >. )
107106eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( a  =  f  ->  (
z  =  <. a ,  b >.  <->  z  =  <. f ,  b >.
) )
108 opeq2 4081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( b  =  U. y  ->  <. f ,  b >.  =  <. f ,  U. y >. )
109108eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( b  =  U. y  -> 
( z  =  <. f ,  b >.  <->  z  =  <. f ,  U. y >. ) )
11012, 105, 107, 109ceqsex2v 3032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( E. a E. b ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b >. )  <->  z  =  <. f ,  U. y >. )
11192, 104, 1103bitri 271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <-> 
z  =  <. f ,  U. y >. )
112111anbi1i 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
<. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <-> 
( z  =  <. f ,  U. y >.  /\  zApply a ) )
113112exbii 1634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( <. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <->  E. z
( z  =  <. f ,  U. y >.  /\  zApply a ) )
114 opex 4577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  <. f ,  U. y >.  e.  _V
115 breq1 4316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z  =  <. f ,  U. y >.  ->  ( zApply a 
<-> 
<. f ,  U. y >.Apply a ) )
116114, 115ceqsexv 3030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <->  <. f ,  U. y >.Apply a )
11712, 105, 90brapply 27991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( <.
f ,  U. y >.Apply a  <->  a  =  ( f `  U. y
) )
118116, 117bitri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <-> 
a  =  ( f `
 U. y ) )
11991, 113, 1183bitri 271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  a  =  ( f `  U. y ) )
12090, 27brfullfun 28001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( aFullFun
F x  <->  x  =  ( F `  a ) )
121119, 120anbi12i 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  /\  aFullFun F x )  <->  ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) ) )
122121exbii 1634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f `
 U. y )  e.  _V
124 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( a  =  ( f `  U. y )  ->  ( F `  a )  =  ( F `  ( f `  U. y ) ) )
125124eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  =  ( f `  U. y )  ->  (
x  =  ( F `
 a )  <->  x  =  ( F `  ( f `
 U. y ) ) ) )
126123, 125ceqsexv 3030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. a ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) )  <->  x  =  ( F `  ( f `
 U. y ) ) )
12789, 122, 1263bitri 271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
(FullFun F  o.  (Apply  o. pprod
(  _I  ,  Bigcup ) ) ) x  <->  x  =  ( F `  ( f `
 U. y ) ) )
128 opelxp 4890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
( f  e.  _V  /\  y  e.  ran Succ )
)
12912, 128mpbiran 909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
y  e.  ran Succ )
13041elrn 5101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ran Succ  <->  E. z  zSucc y )
13169, 41brsuccf 27994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( zSucc y  <->  y  =  suc  z )
132131exbii 1634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z  zSucc y  <->  E. z 
y  =  suc  z
)
133129, 130, 1323bitri 271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <->  E. z  y  =  suc  z )
134127, 133anbi12ci 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 521 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . . . . . . . . . . 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 521 . . . . . . . . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . . . . . . . . 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 6478 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  On  <->  ( y  =  (/)  \/  E. z  e.  On  y  =  suc  z  \/  ( y  e.  _V  /\  Lim  y
) ) )
141 nlim0 4798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  (/)
142 limeq 4752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  ( Lim  y  <->  Lim  (/) ) )
143141, 142mtbiri 303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  Lim  y )
144143intnanrd 908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
145 nsuceq0 4820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  suc  z  =/=  (/)
146 neeq2 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  (/)  ->  ( suc  z  =/=  y  <->  suc  z  =/=  (/) ) )
147145, 146mpbiri 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  (/)  ->  suc  z  =/=  y )
148147necomd 2640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  (/)  ->  y  =/= 
suc  z )
149148neneqd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  -.  y  =  suc  z )
150149nexdv 1818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  E. z  y  =  suc  z )
151150intnanrd 908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
152 ioran 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  -.  (
( Lim  y  /\  x  =  U. (
f " y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `
 U. y ) ) ) ) )
154 orel2 383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 27978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  U. { A }  =  if ( A  e.  _V ,  A ,  (/) )
158156, 157syl6eqr 2493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. { A }
)
159158eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  <->  x  =  U. { A } ) )
160159biimprd 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  U. { A }  ->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
161160adantld 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 44 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  ->  x  =  U. { A } ) )
164163anc2li 557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 385 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 33 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 191 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  suc  z  -> 
( y  =/=  (/)  <->  suc  z  =/=  (/) ) )
169145, 168mpbiri 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
y  =/=  (/) )
170169neneqd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  y  =  (/) )
171170intnanrd 908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
172171rexlimivw 2858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
173 orel1 382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  _V  ->  -.  Lim  suc  z )
17669, 175ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  suc  z
177 limeq 4752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
( Lim  y  <->  Lim  suc  z
) )
178176, 177mtbiri 303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  Lim  y )
179178rexlimivw 2858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  Lim  y )
180179intnanrd 908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
181 orel1 382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( suc  z  =/=  (/)  <->  -.  suc  z  =  (/) )
184145, 183mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  -.  suc  z  =  (/)
185184iffalsei 3821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
186 iffalse 3820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -. 
Lim  suc  z  ->  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) ) )
18769, 175, 186mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) )
188185, 187eqtri 2463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
189 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  suc  z  -> 
( y  =  (/)  <->  suc  z  =  (/) ) )
190 unieq 4120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  suc  z  ->  U. y  =  U. suc  z )
191190fveq2d 5716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  suc  z  -> 
( f `  U. y )  =  ( f `  U. suc  z ) )
192191fveq2d 5716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  suc  z  -> 
( F `  (
f `  U. y ) )  =  ( F `
 ( f `  U. suc  z ) ) )
193177, 192ifbieq2d 3835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
194189, 193ifbieq2d 3835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
195188, 194, 1923eqtr4a 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
196195rexlimivw 2858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
197196eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
198197biimprd 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
199198adantld 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
200174, 182, 1993syld 55 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
201 rexex 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. z  e.  On  y  =  suc  z  ->  E. z 
y  =  suc  z
)
202197biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
203 olc 384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
204203olcd 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
205201, 202, 204syl6an 545 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
206200, 205impbid 191 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
207143con2i 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  y  =  (/) )
208207intnanrd 908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  (
y  =  (/)  /\  x  =  U. { A }
) )
209208, 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 ) ) ) ) ) )
210178exlimiv 1688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z  y  =  suc  z  ->  -.  Lim  y )
211210con2i 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  E. z 
y  =  suc  z
)
212211intnanrd 908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
213 orel2 383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
214212, 213syl 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 ) ) ) )
215 iffalse 3820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
216207, 215syl 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 ) ) ) )
217 iftrue 3818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( Lim  y  ->  if ( Lim  y ,  U. (
f " y ) ,  ( F `  ( f `  U. y ) ) )  =  U. ( f
" y ) )
218216, 217eqtrd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Lim  y  ->  if (
y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. ( f "
y ) )
219218eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
220219biimprd 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
221220adantld 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
222209, 214, 2213syld 55 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
223222adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
224219biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
225224anc2li 557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
226 orc 385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  -> 
( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )
227226olcd 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
228225, 227syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
229228adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
230223, 229impbid 191 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
231167, 206, 2303jaoi 1281 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
232140, 231sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
233139, 232syl5bb 257 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
23455, 233syl 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 ) ) ) ) ) )
23527, 67brcnv 5043 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x `'Apply <. f ,  y
>. 
<-> 
<. f ,  y >.Apply x )
23612, 41, 27brapply 27991 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
f ,  y >.Apply x 
<->  x  =  ( f `
 y ) )
237235, 236bitri 249 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x `'Apply <. f ,  y
>. 
<->  x  =  ( f `
 y ) )
238237a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( x `'Apply <. f ,  y >.  <->  x  =  ( f `  y
) ) )
239234, 238anbi12d 710 . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
240 ancom 450 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
241239, 240syl6bb 261 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
242241exbidv 1680 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
243 df-br 4314 . . . . . . . . . . . . . . . . . . . 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 )
) ) ) ) )
24467elfix 27956 . . . . . . . . . . . . . . . . . . . 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 >. )
24567, 67brco 5031 . . . . . . . . . . . . . . . . . . . 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 >. )
)
246243, 244, 2453bitri 271 . . . . . . . . . . . . . . . . . . 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 >. )
)
247 fvex 5722 . . . . . . . . . . . . . . . . . . . 20  |-  ( f `
 y )  e. 
_V
248247eqvinc 3107 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
249242, 246, 2483bitr4g 288 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
250249notbid 294 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
2512503expia 1189 . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
252251pm5.32d 639 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
253 annim 425 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
254252, 253syl6bb 261 . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
25553, 254syl5bb 257 . . . . . . . . . . . . 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 ) ) ) ) ) ) )
256255exbidv 1680 . . . . . . . . . . . 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 ) ) ) ) ) ) )
257 exnal 1618 . . . . . . . . . . . 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 ) ) ) ) ) )
258256, 257syl6rbb 262 . . . . . . . . . . 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 ) )
25912eldm 5058 . . . . . . . . . . 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 )
260258, 259syl6bbr 263 . . . . . . . . . 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 )
) ) ) ) ) ) )
261260con1bid 330 . . . . . . . . 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 ) ) ) ) ) ) )
262 df-ral 2741 . . . . . . . . 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 ) ) ) ) ) )
263261, 262syl6bbr 263 . . . . . . . 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 ) ) ) ) ) )
264263pm5.32i 637 . . . . . . 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 ) ) ) ) ) )
265 anass 649 . . . . . . 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 ) ) ) ) ) ) )
266264, 265bitri 249 . . . . . 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 ) ) ) ) ) ) )
26721, 39, 2663bitri 271 . . . . 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 ) ) ) ) ) ) )
26819, 20, 2673bitr4ri 278 . . . 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 ) ) ) ) ) )
269268abbi2i 2560 . . 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 ) ) ) ) ) }
270269unieqi 4121 . 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 ) ) ) ) ) }
2711, 270eqtr4i 2466 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    \/ w3o 964    /\ w3a 965   A.wal 1367    = wceq 1369   E.wex 1586    e. wcel 1756   {cab 2429    =/= wne 2620   A.wral 2736   E.wrex 2737   _Vcvv 2993    \ cdif 3346    u. cun 3347    i^i cin 3348   (/)c0 3658   ifcif 3812   {csn 3898   <.cop 3904   U.cuni 4112   class class class wbr 4313    _E cep 4651    _I cid 4652   Oncon0 4740   Lim wlim 4741   suc csuc 4742    X. cxp 4859   `'ccnv 4860   dom cdm 4861   ran crn 4862    |` cres 4863   "cima 4864    o. ccom 4865   Fun wfun 5433    Fn wfn 5434   ` cfv 5439   reccrdg 6886  pprodcpprod 27883   Bigcupcbigcup 27886   Fixcfix 27887   Limitsclimits 27888   Funscfuns 27889  Imgcimg 27894  Domaincdomain 27895  Applycapply 27897  Succcsuccf 27900  FullFuncfullfn 27902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-om 6498  df-1st 6598  df-2nd 6599  df-recs 6853  df-rdg 6887  df-symdif 27871  df-txp 27906  df-pprod 27907  df-bigcup 27910  df-fix 27911  df-limits 27912  df-funs 27913  df-singleton 27914  df-singles 27915  df-image 27916  df-cart 27917  df-img 27918  df-domain 27919  df-cup 27921  df-succf 27924  df-apply 27925  df-funpart 27926  df-fullfun 27927
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator