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

Theorem dfrdg4 30667
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 30394 . 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 804 . . . . . . . 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 5547 . . . . . . . . . 10  |-  ( f  Fn  x  <->  ( Fun  f  /\  dom  f  =  x ) )
4 ancom 451 . . . . . . . . . 10  |-  ( ( Fun  f  /\  dom  f  =  x )  <->  ( dom  f  =  x  /\  Fun  f ) )
5 eqcom 2435 . . . . . . . . . . 11  |-  ( dom  f  =  x  <->  x  =  dom  f )
65anbi1i 699 . . . . . . . . . 10  |-  ( ( dom  f  =  x  /\  Fun  f )  <-> 
( x  =  dom  f  /\  Fun  f ) )
73, 4, 63bitri 274 . . . . . . . . 9  |-  ( f  Fn  x  <->  ( x  =  dom  f  /\  Fun  f ) )
87anbi1i 699 . . . . . . . 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 653 . . . . . . . 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 274 . . . . . . 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 1712 . . . . . 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 3025 . . . . . . . 8  |-  f  e. 
_V
1312dmex 6684 . . . . . . 7  |-  dom  f  e.  _V
14 eleq1 2494 . . . . . . . . 9  |-  ( x  =  dom  f  -> 
( x  e.  On  <->  dom  f  e.  On ) )
15 raleq 2964 . . . . . . . . 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 715 . . . . . . . 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 708 . . . . . . 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 3060 . . . . . 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 252 . . . . 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 2720 . . . . 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 3389 . . . . . 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 3592 . . . . . . . 8  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( f  e.  Funs  /\  f  e.  ( `'Domain " On ) ) )
2312elfuns 30631 . . . . . . . . 9  |-  ( f  e.  Funs  <->  Fun  f )
2412elima 5135 . . . . . . . . . 10  |-  ( f  e.  ( `'Domain " On ) 
<->  E. x  e.  On  x `'Domain f )
25 df-rex 2720 . . . . . . . . . 10  |-  ( E. x  e.  On  x `'Domain f  <->  E. x ( x  e.  On  /\  x `'Domain f ) )
26 ancom 451 . . . . . . . . . . . . 13  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x `'Domain f  /\  x  e.  On ) )
27 vex 3025 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
2827, 12brcnv 4979 . . . . . . . . . . . . . . 15  |-  ( x `'Domain f  <->  fDomain x )
2912, 27brdomain 30649 . . . . . . . . . . . . . . 15  |-  ( fDomain
x  <->  x  =  dom  f )
3028, 29bitri 252 . . . . . . . . . . . . . 14  |-  ( x `'Domain f  <->  x  =  dom  f )
3130anbi1i 699 . . . . . . . . . . . . 13  |-  ( ( x `'Domain f  /\  x  e.  On )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3226, 31bitri 252 . . . . . . . . . . . 12  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3332exbii 1712 . . . . . . . . . . 11  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  E. x
( x  =  dom  f  /\  x  e.  On ) )
3413, 14ceqsexv 3060 . . . . . . . . . . 11  |-  ( E. x ( x  =  dom  f  /\  x  e.  On )  <->  dom  f  e.  On )
3533, 34bitri 252 . . . . . . . . . 10  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  dom  f  e.  On )
3624, 25, 353bitri 274 . . . . . . . . 9  |-  ( f  e.  ( `'Domain " On ) 
<->  dom  f  e.  On )
3723, 36anbi12i 701 . . . . . . . 8  |-  ( ( f  e.  Funs  /\  f  e.  ( `'Domain " On ) )  <->  ( Fun  f  /\  dom  f  e.  On ) )
3822, 37bitri 252 . . . . . . 7  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( Fun  f  /\  dom  f  e.  On ) )
3938anbi1i 699 . . . . . 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 4417 . . . . . . . . . . . . . . 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 3025 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
4212, 41brco 4967 . . . . . . . . . . . . . . . . 17  |-  ( f ( `'  _E  o. Domain ) y  <->  E. x ( fDomain
x  /\  x `'  _E  y ) )
4329anbi1i 699 . . . . . . . . . . . . . . . . . . 19  |-  ( ( fDomain x  /\  x `'  _E  y )  <->  ( x  =  dom  f  /\  x `'  _E  y ) )
4443exbii 1712 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  E. x ( x  =  dom  f  /\  x `'  _E  y
) )
45 breq1 4369 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  dom  f  -> 
( x `'  _E  y 
<->  dom  f `'  _E  y ) )
4613, 45ceqsexv 3060 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( x  =  dom  f  /\  x `'  _E  y )  <->  dom  f `'  _E  y )
4744, 46bitri 252 . . . . . . . . . . . . . . . . 17  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  dom  f `'  _E  y )
4813, 41brcnv 4979 . . . . . . . . . . . . . . . . . 18  |-  ( dom  f `'  _E  y  <->  y  _E  dom  f )
4913epelc 4709 . . . . . . . . . . . . . . . . . 18  |-  ( y  _E  dom  f  <->  y  e.  dom  f )
5048, 49bitri 252 . . . . . . . . . . . . . . . . 17  |-  ( dom  f `'  _E  y  <->  y  e.  dom  f )
5142, 47, 503bitri 274 . . . . . . . . . . . . . . . 16  |-  ( f ( `'  _E  o. Domain ) y  <->  y  e.  dom  f )
5251anbi1i 699 . . . . . . . . . . . . . . 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 252 . . . . . . . . . . . . . 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 5410 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( dom  f  e.  On  /\  y  e.  dom  f
)  ->  y  e.  On )
55543adant1 1023 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
y  e.  On )
56 brun 4415 . . . . . . . . . . . . . . . . . . . . . . . . 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 4827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( <. f ,  y >.  e.  ( _V  X.  { (/) } )  /\  x  e. 
{ U. { A } } ) )
58 opelxp 4826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  ( f  e.  _V  /\  y  e. 
{ (/) } ) )
5912, 58mpbiran 926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  e.  {
(/) } )
60 elsn 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  { (/) }  <->  y  =  (/) )
6159, 60bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  =  (/) )
62 elsn 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  { U. { A } }  <->  x  =  U. { A } )
6361, 62anbi12i 701 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
<. f ,  y >.  e.  ( _V  X.  { (/)
} )  /\  x  e.  { U. { A } } )  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
6457, 63bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
65 brun 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( <. f ,  y >. ( Bigcup  o. Img ) x  /\  <.
f ,  y >.  e.  ( _V  X.  Limits ) ) )
67 opex 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  <. f ,  y >.  e.  _V
6867, 27brco 4967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  E. z ( <. f ,  y >.Img z  /\  z Bigcup x ) )
69 vex 3025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  z  e. 
_V
7012, 41, 69brimg 30653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.Img z 
<->  z  =  ( f
" y ) )
7127brbigcup 30614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z
Bigcup x  <->  U. z  =  x )
7270, 71anbi12i 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.Img z  /\  z Bigcup x )  <-> 
( z  =  ( f " y )  /\  U. z  =  x ) )
7372exbii 1712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( <. f ,  y >.Img z  /\  z Bigcup x )  <->  E. z
( z  =  ( f " y )  /\  U. z  =  x ) )
74 imaexg 6688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f  e.  _V  ->  (
f " y )  e.  _V )
7512, 74ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f
" y )  e. 
_V
76 unieq 4170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  ( f "
y )  ->  U. z  =  U. ( f "
y ) )
7776eqeq1d 2430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  ( f "
y )  ->  ( U. z  =  x  <->  U. ( f " y
)  =  x ) )
7875, 77ceqsexv 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  U. (
f " y )  =  x )
79 eqcom 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( U. ( f " y
)  =  x  <->  x  =  U. ( f " y
) )
8078, 79bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  x  =  U. ( f " y
) )
8168, 73, 803bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  x  =  U. ( f
" y ) )
82 opelxp 4826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
( f  e.  _V  /\  y  e.  Limits ) )
8312, 82mpbiran 926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
y  e.  Limits )
8441ellimits 30626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  Limits 
<->  Lim  y )
8583, 84bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <->  Lim  y )
8681, 85anbi12ci 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
<. f ,  y >.
( Bigcup  o. Img ) x  /\  <. f ,  y
>.  e.  ( _V  X.  Limits ) )  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8766, 86bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8827brres 5073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  a  e. 
_V
9167, 90brco 4967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  E. z
( <. f ,  y
>.pprod (  _I  ,  Bigcup ) z  /\  zApply a
) )
9212, 41, 69brpprod3a 30602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <->  E. a E. b ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b ) )
93 3anrot 987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( f  _I  a  /\  y Bigcup b  /\  z  = 
<. a ,  b >.
) )
9490ideq 4949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  _I  a  <->  f  =  a )
95 equcom 1848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  =  a  <->  a  =  f )
9694, 95bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( f  _I  a  <->  a  =  f )
97 vex 3025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  b  e. 
_V
9897brbigcup 30614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y
Bigcup b  <->  U. y  =  b )
99 eqcom 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( U. y  =  b  <->  b  =  U. y )
10098, 99bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y
Bigcup b  <->  b  =  U. y )
101 biid 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( z  =  <. a ,  b
>. 
<->  z  =  <. a ,  b >. )
10296, 100, 1013anbi123i 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f  _I  a  /\  y Bigcup b  /\  z  =  <. a ,  b
>. )  <->  ( a  =  f  /\  b  = 
U. y  /\  z  =  <. a ,  b
>. ) )
10393, 102bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b
>. ) )
1041032exbii 1713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  U. y  e.  _V
106 opeq1 4130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( a  =  f  ->  <. a ,  b >.  =  <. f ,  b >. )
107106eqeq2d 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( a  =  f  ->  (
z  =  <. a ,  b >.  <->  z  =  <. f ,  b >.
) )
108 opeq2 4131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( b  =  U. y  ->  <. f ,  b >.  =  <. f ,  U. y >. )
109108eqeq2d 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( b  =  U. y  -> 
( z  =  <. f ,  b >.  <->  z  =  <. f ,  U. y >. ) )
11012, 105, 107, 109ceqsex2v 3062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( E. a E. b ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b >. )  <->  z  =  <. f ,  U. y >. )
11192, 104, 1103bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <-> 
z  =  <. f ,  U. y >. )
112111anbi1i 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
<. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <-> 
( z  =  <. f ,  U. y >.  /\  zApply a ) )
113112exbii 1712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( <. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <->  E. z
( z  =  <. f ,  U. y >.  /\  zApply a ) )
114 opex 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  <. f ,  U. y >.  e.  _V
115 breq1 4369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z  =  <. f ,  U. y >.  ->  ( zApply a 
<-> 
<. f ,  U. y >.Apply a ) )
116114, 115ceqsexv 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <->  <. f ,  U. y >.Apply a )
11712, 105, 90brapply 30654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( <.
f ,  U. y >.Apply a  <->  a  =  ( f `  U. y
) )
118116, 117bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <-> 
a  =  ( f `
 U. y ) )
11991, 113, 1183bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  a  =  ( f `  U. y ) )
12090, 27brfullfun 30664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( aFullFun
F x  <->  x  =  ( F `  a ) )
121119, 120anbi12i 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  /\  aFullFun F x )  <->  ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) ) )
122121exbii 1712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f `
 U. y )  e.  _V
124 fveq2 5825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( a  =  ( f `  U. y )  ->  ( F `  a )  =  ( F `  ( f `  U. y ) ) )
125124eqeq2d 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  =  ( f `  U. y )  ->  (
x  =  ( F `
 a )  <->  x  =  ( F `  ( f `
 U. y ) ) ) )
126123, 125ceqsexv 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. a ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) )  <->  x  =  ( F `  ( f `
 U. y ) ) )
12789, 122, 1263bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
(FullFun F  o.  (Apply  o. pprod
(  _I  ,  Bigcup ) ) ) x  <->  x  =  ( F `  ( f `
 U. y ) ) )
128 opelxp 4826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
( f  e.  _V  /\  y  e.  ran Succ )
)
12912, 128mpbiran 926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
y  e.  ran Succ )
13041elrn 5037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ran Succ  <->  E. z  zSucc y )
13169, 41brsuccf 30657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( zSucc y  <->  y  =  suc  z )
132131exbii 1712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z  zSucc y  <->  E. z 
y  =  suc  z
)
133129, 130, 1323bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <->  E. z  y  =  suc  z )
134127, 133anbi12ci 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 523 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 252 . . . . . . . . . . . . . . . . . . . . . . . . . 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 523 . . . . . . . . . . . . . . . . . . . . . . . . 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 252 . . . . . . . . . . . . . . . . . . . . . . . 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 6631 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  On  <->  ( y  =  (/)  \/  E. z  e.  On  y  =  suc  z  \/  ( y  e.  _V  /\  Lim  y
) ) )
141 nlim0 5443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  (/)
142 limeq 5397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  ( Lim  y  <->  Lim  (/) ) )
143141, 142mtbiri 304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  Lim  y )
144143intnanrd 925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
145 nsuceq0 5465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  suc  z  =/=  (/)
146 neeq2 2664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  (/)  ->  ( suc  z  =/=  y  <->  suc  z  =/=  (/) ) )
147145, 146mpbiri 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  (/)  ->  suc  z  =/=  y )
148147necomd 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  (/)  ->  y  =/= 
suc  z )
149148neneqd 2606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  -.  y  =  suc  z )
150149nexdv 1775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  E. z  y  =  suc  z )
151150intnanrd 925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
152 ioran 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  -.  (
( Lim  y  /\  x  =  U. (
f " y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `
 U. y ) ) ) ) )
154 orel2 384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 30641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  U. { A }  =  if ( A  e.  _V ,  A ,  (/) )
158156, 157syl6eqr 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. { A }
)
159158eqeq2d 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  <->  x  =  U. { A } ) )
160159biimprd 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  U. { A }  ->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
161160adantld 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 45 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  ->  x  =  U. { A } ) )
164163anc2li 559 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 386 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 34 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 193 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  suc  z  -> 
( y  =/=  (/)  <->  suc  z  =/=  (/) ) )
169145, 168mpbiri 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
y  =/=  (/) )
170169neneqd 2606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  y  =  (/) )
171170intnanrd 925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
172171rexlimivw 2853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
173 orel1 383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  _V  ->  -.  Lim  suc  z )
17669, 175ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  suc  z
177 limeq 5397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
( Lim  y  <->  Lim  suc  z
) )
178176, 177mtbiri 304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  Lim  y )
179178rexlimivw 2853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  Lim  y )
180179intnanrd 925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
181 orel1 383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
183145neii 2603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  -.  suc  z  =  (/)
184183iffalsei 3864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
185 iffalse 3863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -. 
Lim  suc  z  ->  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) ) )
18669, 175, 185mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) )
187184, 186eqtri 2450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
188 eqeq1 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  suc  z  -> 
( y  =  (/)  <->  suc  z  =  (/) ) )
189 unieq 4170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  suc  z  ->  U. y  =  U. suc  z )
190189fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  suc  z  -> 
( f `  U. y )  =  ( f `  U. suc  z ) )
191190fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  suc  z  -> 
( F `  (
f `  U. y ) )  =  ( F `
 ( f `  U. suc  z ) ) )
192177, 191ifbieq2d 3879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
193188, 192ifbieq2d 3879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
194187, 193, 1913eqtr4a 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
195194rexlimivw 2853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
196195eqeq2d 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
197196biimprd 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
198197adantld 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
199174, 182, 1983syld 57 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
200 rexex 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. z  e.  On  y  =  suc  z  ->  E. z 
y  =  suc  z
)
201196biimpd 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
202 olc 385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
203202olcd 394 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
204200, 201, 203syl6an 547 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
205199, 204impbid 193 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
206143con2i 123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  y  =  (/) )
207206intnanrd 925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  (
y  =  (/)  /\  x  =  U. { A }
) )
208207, 173syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
209178exlimiv 1770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z  y  =  suc  z  ->  -.  Lim  y )
210209con2i 123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  E. z 
y  =  suc  z
)
211210intnanrd 925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
212 orel2 384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
213211, 212syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
214206iffalsed 3865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
215 iftrue 3860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( Lim  y  ->  if ( Lim  y ,  U. (
f " y ) ,  ( F `  ( f `  U. y ) ) )  =  U. ( f
" y ) )
216214, 215eqtrd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Lim  y  ->  if (
y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. ( f "
y ) )
217216eqeq2d 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
218217biimprd 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
219218adantld 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
220208, 213, 2193syld 57 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
221220adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
222217biimpd 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
223222anc2li 559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
224 orc 386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  -> 
( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )
225224olcd 394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
226223, 225syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
227226adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
228221, 227impbid 193 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
229167, 205, 2283jaoi 1327 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
230140, 229sylbi 198 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
231139, 230syl5bb 260 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
23255, 231syl 17 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
23327, 67brcnv 4979 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x `'Apply <. f ,  y
>. 
<-> 
<. f ,  y >.Apply x )
23412, 41, 27brapply 30654 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
f ,  y >.Apply x 
<->  x  =  ( f `
 y ) )
235233, 234bitri 252 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x `'Apply <. f ,  y
>. 
<->  x  =  ( f `
 y ) )
236235a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( x `'Apply <. f ,  y >.  <->  x  =  ( f `  y
) ) )
237232, 236anbi12d 715 . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
238 ancom 451 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
239237, 238syl6bb 264 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
240239exbidv 1762 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
241 df-br 4367 . . . . . . . . . . . . . . . . . . . 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 )
) ) ) ) )
24267elfix 30619 . . . . . . . . . . . . . . . . . . . 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 >. )
24367, 67brco 4967 . . . . . . . . . . . . . . . . . . . 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 >. )
)
244241, 242, 2433bitri 274 . . . . . . . . . . . . . . . . . . 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 >. )
)
245 fvex 5835 . . . . . . . . . . . . . . . . . . . 20  |-  ( f `
 y )  e. 
_V
246245eqvinc 3141 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
247240, 244, 2463bitr4g 291 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
248247notbid 295 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
2492483expia 1207 . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
250249pm5.32d 643 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
251 annim 426 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
252250, 251syl6bb 264 . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
25353, 252syl5bb 260 . . . . . . . . . . . . 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 ) ) ) ) ) ) )
254253exbidv 1762 . . . . . . . . . . . 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 ) ) ) ) ) ) )
255 exnal 1693 . . . . . . . . . . . 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 ) ) ) ) ) )
256254, 255syl6rbb 265 . . . . . . . . . . 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 ) )
25712eldm 4994 . . . . . . . . . . 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 )
258256, 257syl6bbr 266 . . . . . . . . . 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 )
) ) ) ) ) ) )
259258con1bid 331 . . . . . . . . 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 ) ) ) ) ) ) )
260 df-ral 2719 . . . . . . . . 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 ) ) ) ) ) )
261259, 260syl6bbr 266 . . . . . . . 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 ) ) ) ) ) )
262261pm5.32i 641 . . . . . . 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 ) ) ) ) ) )
263 anass 653 . . . . . . 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 ) ) ) ) ) ) )
264262, 263bitri 252 . . . . . 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 ) ) ) ) ) ) )
26521, 39, 2643bitri 274 . . . . 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 ) ) ) ) ) ) )
26619, 20, 2653bitr4ri 281 . . . 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 ) ) ) ) ) )
267266abbi2i 2543 . . 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 ) ) ) ) ) }
268267unieqi 4171 . 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 ) ) ) ) ) }
2691, 268eqtr4i 2453 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 187    \/ wo 369    /\ wa 370    \/ w3o 981    /\ w3a 982   A.wal 1435    = wceq 1437   E.wex 1657    e. wcel 1872   {cab 2414    =/= wne 2599   A.wral 2714   E.wrex 2715   _Vcvv 3022    \ cdif 3376    u. cun 3377    i^i cin 3378   (/)c0 3704   ifcif 3854   {csn 3941   <.cop 3947   U.cuni 4162   class class class wbr 4366    _E cep 4705    _I cid 4706    X. cxp 4794   `'ccnv 4795   dom cdm 4796   ran crn 4797    |` cres 4798   "cima 4799    o. ccom 4800   Oncon0 5385   Lim wlim 5386   suc csuc 5387   Fun wfun 5538    Fn wfn 5539   ` cfv 5544   reccrdg 7082  pprodcpprod 30546   Bigcupcbigcup 30549   Fixcfix 30550   Limitsclimits 30551   Funscfuns 30552  Imgcimg 30557  Domaincdomain 30558  Applycapply 30560  Succcsuccf 30563  FullFuncfullfn 30565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-symdif 3636  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-txp 30569  df-pprod 30570  df-bigcup 30573  df-fix 30574  df-limits 30575  df-funs 30576  df-singleton 30577  df-singles 30578  df-image 30579  df-cart 30580  df-img 30581  df-domain 30582  df-cup 30584  df-succf 30587  df-apply 30588  df-funpart 30589  df-fullfun 30590
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator