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

Theorem dfrdg4 25800
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 25429 . 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 774 . . . . . . . 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 5460 . . . . . . . . . 10  |-  ( f  Fn  x  <->  ( Fun  f  /\  dom  f  =  x ) )
4 ancom 439 . . . . . . . . . 10  |-  ( ( Fun  f  /\  dom  f  =  x )  <->  ( dom  f  =  x  /\  Fun  f ) )
5 eqcom 2440 . . . . . . . . . . 11  |-  ( dom  f  =  x  <->  x  =  dom  f )
65anbi1i 678 . . . . . . . . . 10  |-  ( ( dom  f  =  x  /\  Fun  f )  <-> 
( x  =  dom  f  /\  Fun  f ) )
73, 4, 63bitri 264 . . . . . . . . 9  |-  ( f  Fn  x  <->  ( x  =  dom  f  /\  Fun  f ) )
87anbi1i 678 . . . . . . . 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 632 . . . . . . . 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 264 . . . . . . 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 1593 . . . . . 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 2961 . . . . . . . 8  |-  f  e. 
_V
1312dmex 5135 . . . . . . 7  |-  dom  f  e.  _V
14 eleq1 2498 . . . . . . . . 9  |-  ( x  =  dom  f  -> 
( x  e.  On  <->  dom  f  e.  On ) )
15 raleq 2906 . . . . . . . . 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 693 . . . . . . . 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 686 . . . . . . 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 2993 . . . . . 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 242 . . . . 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 2713 . . . . 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 3332 . . . . . 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 3532 . . . . . . . 8  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( f  e.  Funs  /\  f  e.  ( `'Domain " On ) ) )
2312elfuns 25765 . . . . . . . . 9  |-  ( f  e.  Funs  <->  Fun  f )
2412elima 5211 . . . . . . . . . 10  |-  ( f  e.  ( `'Domain " On ) 
<->  E. x  e.  On  x `'Domain f )
25 df-rex 2713 . . . . . . . . . 10  |-  ( E. x  e.  On  x `'Domain f  <->  E. x ( x  e.  On  /\  x `'Domain f ) )
26 ancom 439 . . . . . . . . . . . . 13  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x `'Domain f  /\  x  e.  On ) )
27 vex 2961 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
2827, 12brcnv 5058 . . . . . . . . . . . . . . 15  |-  ( x `'Domain f  <->  fDomain x )
2912, 27brdomain 25783 . . . . . . . . . . . . . . 15  |-  ( fDomain
x  <->  x  =  dom  f )
3028, 29bitri 242 . . . . . . . . . . . . . 14  |-  ( x `'Domain f  <->  x  =  dom  f )
3130anbi1i 678 . . . . . . . . . . . . 13  |-  ( ( x `'Domain f  /\  x  e.  On )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3226, 31bitri 242 . . . . . . . . . . . 12  |-  ( ( x  e.  On  /\  x `'Domain f )  <->  ( x  =  dom  f  /\  x  e.  On ) )
3332exbii 1593 . . . . . . . . . . 11  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  E. x
( x  =  dom  f  /\  x  e.  On ) )
3413, 14ceqsexv 2993 . . . . . . . . . . 11  |-  ( E. x ( x  =  dom  f  /\  x  e.  On )  <->  dom  f  e.  On )
3533, 34bitri 242 . . . . . . . . . 10  |-  ( E. x ( x  e.  On  /\  x `'Domain
f )  <->  dom  f  e.  On )
3624, 25, 353bitri 264 . . . . . . . . 9  |-  ( f  e.  ( `'Domain " On ) 
<->  dom  f  e.  On )
3723, 36anbi12i 680 . . . . . . . 8  |-  ( ( f  e.  Funs  /\  f  e.  ( `'Domain " On ) )  <->  ( Fun  f  /\  dom  f  e.  On ) )
3822, 37bitri 242 . . . . . . 7  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( Fun  f  /\  dom  f  e.  On ) )
3938anbi1i 678 . . . . . 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 4263 . . . . . . . . . . . . . . 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 2961 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
4212, 41brco 5046 . . . . . . . . . . . . . . . . 17  |-  ( f ( `'  _E  o. Domain ) y  <->  E. x ( fDomain
x  /\  x `'  _E  y ) )
4329anbi1i 678 . . . . . . . . . . . . . . . . . . 19  |-  ( ( fDomain x  /\  x `'  _E  y )  <->  ( x  =  dom  f  /\  x `'  _E  y ) )
4443exbii 1593 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  E. x ( x  =  dom  f  /\  x `'  _E  y
) )
45 breq1 4218 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  dom  f  -> 
( x `'  _E  y 
<->  dom  f `'  _E  y ) )
4613, 45ceqsexv 2993 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( x  =  dom  f  /\  x `'  _E  y )  <->  dom  f `'  _E  y )
4744, 46bitri 242 . . . . . . . . . . . . . . . . 17  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  dom  f `'  _E  y )
4813, 41brcnv 5058 . . . . . . . . . . . . . . . . . 18  |-  ( dom  f `'  _E  y  <->  y  _E  dom  f )
4913epelc 4499 . . . . . . . . . . . . . . . . . 18  |-  ( y  _E  dom  f  <->  y  e.  dom  f )
5048, 49bitri 242 . . . . . . . . . . . . . . . . 17  |-  ( dom  f `'  _E  y  <->  y  e.  dom  f )
5142, 47, 503bitri 264 . . . . . . . . . . . . . . . 16  |-  ( f ( `'  _E  o. Domain ) y  <->  y  e.  dom  f )
5251anbi1i 678 . . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . . 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 4609 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( dom  f  e.  On  /\  y  e.  dom  f
)  ->  y  e.  On )
55543adant1 976 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
y  e.  On )
56 brun 4261 . . . . . . . . . . . . . . . . . . . . . . . . 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 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( <. f ,  y >.  e.  ( _V  X.  { (/) } )  /\  x  e. 
{ U. { A } } ) )
58 opelxp 4911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  ( f  e.  _V  /\  y  e. 
{ (/) } ) )
5912, 58mpbiran 886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  e.  {
(/) } )
60 elsn 3831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  { (/) }  <->  y  =  (/) )
6159, 60bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.  e.  ( _V  X.  { (/)
} )  <->  y  =  (/) )
62 elsn 3831 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  { U. { A } }  <->  x  =  U. { A } )
6361, 62anbi12i 680 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
<. f ,  y >.  e.  ( _V  X.  { (/)
} )  /\  x  e.  { U. { A } } )  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
6457, 63bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
f ,  y >.
( ( _V  X.  { (/) } )  X. 
{ U. { A } } ) x  <->  ( y  =  (/)  /\  x  = 
U. { A }
) )
65 brun 4261 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( <. f ,  y >. ( Bigcup  o. Img ) x  /\  <.
f ,  y >.  e.  ( _V  X.  Limits ) ) )
67 opex 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  <. f ,  y >.  e.  _V
6867, 27brco 5046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  E. z ( <. f ,  y >.Img z  /\  z Bigcup x ) )
69 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  z  e. 
_V
7012, 41, 69brimg 25787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.Img z 
<->  z  =  ( f
" y ) )
7127brbigcup 25748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z
Bigcup x  <->  U. z  =  x )
7270, 71anbi12i 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.Img z  /\  z Bigcup x )  <-> 
( z  =  ( f " y )  /\  U. z  =  x ) )
7372exbii 1593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( <. f ,  y >.Img z  /\  z Bigcup x )  <->  E. z
( z  =  ( f " y )  /\  U. z  =  x ) )
74 imaexg 5220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f  e.  _V  ->  (
f " y )  e.  _V )
7512, 74ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f
" y )  e. 
_V
76 unieq 4026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  ( f "
y )  ->  U. z  =  U. ( f "
y ) )
7776eqeq1d 2446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  ( f "
y )  ->  ( U. z  =  x  <->  U. ( f " y
)  =  x ) )
7875, 77ceqsexv 2993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  U. (
f " y )  =  x )
79 eqcom 2440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( U. ( f " y
)  =  x  <->  x  =  U. ( f " y
) )
8078, 79bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z ( z  =  ( f " y
)  /\  U. z  =  x )  <->  x  =  U. ( f " y
) )
8168, 73, 803bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
( Bigcup  o. Img ) x  <->  x  =  U. ( f
" y ) )
82 opelxp 4911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
( f  e.  _V  /\  y  e.  Limits ) )
8312, 82mpbiran 886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <-> 
y  e.  Limits )
8441ellimits 25760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  Limits 
<->  Lim  y )
8583, 84bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  Limits )  <->  Lim  y )
8681, 85anbi12ci 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
<. f ,  y >.
( Bigcup  o. Img ) x  /\  <. f ,  y
>.  e.  ( _V  X.  Limits ) )  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8766, 86bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
f ,  y >.
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) ) x  <->  ( Lim  y  /\  x  =  U. ( f " y
) ) )
8827brres 5155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  a  e. 
_V
9167, 90brco 5046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  E. z
( <. f ,  y
>.pprod (  _I  ,  Bigcup ) z  /\  zApply a
) )
9212, 41, 69brpprod3a 25736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <->  E. a E. b ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b ) )
93 3anrot 942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( f  _I  a  /\  y Bigcup b  /\  z  = 
<. a ,  b >.
) )
9490ideq 5028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  _I  a  <->  f  =  a )
95 equcom 1693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f  =  a  <->  a  =  f )
9694, 95bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( f  _I  a  <->  a  =  f )
97 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  b  e. 
_V
9897brbigcup 25748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y
Bigcup b  <->  U. y  =  b )
99 eqcom 2440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( U. y  =  b  <->  b  =  U. y )
10098, 99bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y
Bigcup b  <->  b  =  U. y )
101 biid 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( z  =  <. a ,  b
>. 
<->  z  =  <. a ,  b >. )
10296, 100, 1013anbi123i 1143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f  _I  a  /\  y Bigcup b  /\  z  =  <. a ,  b
>. )  <->  ( a  =  f  /\  b  = 
U. y  /\  z  =  <. a ,  b
>. ) )
10393, 102bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( z  =  <. a ,  b >.  /\  f  _I  a  /\  y Bigcup b )  <->  ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b
>. ) )
1041032exbii 1594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  U. y  e.  _V
106 opeq1 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( a  =  f  ->  <. a ,  b >.  =  <. f ,  b >. )
107106eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( a  =  f  ->  (
z  =  <. a ,  b >.  <->  z  =  <. f ,  b >.
) )
108 opeq2 3987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( b  =  U. y  ->  <. f ,  b >.  =  <. f ,  U. y >. )
109108eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( b  =  U. y  -> 
( z  =  <. f ,  b >.  <->  z  =  <. f ,  U. y >. ) )
11012, 105, 107, 109ceqsex2v 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( E. a E. b ( a  =  f  /\  b  =  U. y  /\  z  =  <. a ,  b >. )  <->  z  =  <. f ,  U. y >. )
11192, 104, 1103bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( <.
f ,  y >.pprod (  _I  ,  Bigcup ) z  <-> 
z  =  <. f ,  U. y >. )
112111anbi1i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
<. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <-> 
( z  =  <. f ,  U. y >.  /\  zApply a ) )
113112exbii 1593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( <. f ,  y >.pprod (  _I  ,  Bigcup ) z  /\  zApply a )  <->  E. z
( z  =  <. f ,  U. y >.  /\  zApply a ) )
114 opex 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  <. f ,  U. y >.  e.  _V
115 breq1 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z  =  <. f ,  U. y >.  ->  ( zApply a 
<-> 
<. f ,  U. y >.Apply a ) )
116114, 115ceqsexv 2993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <->  <. f ,  U. y >.Apply a )
11712, 105, 90brapply 25788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( <.
f ,  U. y >.Apply a  <->  a  =  ( f `  U. y
) )
118116, 117bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. z ( z  = 
<. f ,  U. y >.  /\  zApply a )  <-> 
a  =  ( f `
 U. y ) )
11991, 113, 1183bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  <->  a  =  ( f `  U. y ) )
12090, 27brfullfun 25798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( aFullFun
F x  <->  x  =  ( F `  a ) )
121119, 120anbi12i 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
<. f ,  y >.
(Apply  o. pprod (  _I  ,  Bigcup ) ) a  /\  aFullFun F x )  <->  ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) ) )
122121exbii 1593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f `
 U. y )  e.  _V
124 fveq2 5731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( a  =  ( f `  U. y )  ->  ( F `  a )  =  ( F `  ( f `  U. y ) ) )
125124eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  =  ( f `  U. y )  ->  (
x  =  ( F `
 a )  <->  x  =  ( F `  ( f `
 U. y ) ) ) )
126123, 125ceqsexv 2993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. a ( a  =  ( f `  U. y )  /\  x  =  ( F `  a ) )  <->  x  =  ( F `  ( f `
 U. y ) ) )
12789, 122, 1263bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.
(FullFun F  o.  (Apply  o. pprod
(  _I  ,  Bigcup ) ) ) x  <->  x  =  ( F `  ( f `
 U. y ) ) )
128 opelxp 4911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
( f  e.  _V  /\  y  e.  ran Succ )
)
12912, 128mpbiran 886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <-> 
y  e.  ran Succ )
13041elrn 5113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ran Succ  <->  E. z  zSucc y )
13169, 41brsuccf 25791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( zSucc y  <->  y  =  suc  z )
132131exbii 1593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z  zSucc y  <->  E. z 
y  =  suc  z
)
133129, 130, 1323bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
f ,  y >.  e.  ( _V  X.  ran Succ )  <->  E. z  y  =  suc  z )
134127, 133anbi12ci 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 509 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . . . . . . . . . . . . . . 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 509 . . . . . . . . . . . . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . . . . . . . . . . . . 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 4829 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  On  <->  ( y  =  (/)  \/  E. z  e.  On  y  =  suc  z  \/  ( y  e.  _V  /\  Lim  y
) ) )
141 nlim0 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  (/)
142 limeq 4596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  ( Lim  y  <->  Lim  (/) ) )
143141, 142mtbiri 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  Lim  y )
144143intnanrd 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
145 nsuceq0 4664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  suc  z  =/=  (/)
146 neeq2 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  (/)  ->  ( suc  z  =/=  y  <->  suc  z  =/=  (/) ) )
147145, 146mpbiri 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  (/)  ->  suc  z  =/=  y )
148147necomd 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  (/)  ->  y  =/= 
suc  z )
149148neneqd 2619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  (/)  ->  -.  y  =  suc  z )
150149nexdv 1942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  -.  E. z  y  =  suc  z )
151150intnanrd 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
152 ioran 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  -.  (
( Lim  y  /\  x  =  U. (
f " y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `
 U. y ) ) ) ) )
154 orel2 374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 25775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  U. { A }  =  if ( A  e.  _V ,  A ,  (/) )
158156, 157syl6eqr 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  (/)  ->  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. { A }
)
159158eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  <->  x  =  U. { A } ) )
160159biimprd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  U. { A }  ->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
161160adantld 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 43 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  (/)  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  ->  x  =  U. { A } ) )
164163anc2li 542 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 376 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 185 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  suc  z  -> 
( y  =/=  (/)  <->  suc  z  =/=  (/) ) )
169145, 168mpbiri 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
y  =/=  (/) )
170169neneqd 2619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  y  =  (/) )
171170intnanrd 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
172171rexlimivw 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( y  =  (/)  /\  x  =  U. { A } ) )
173 orel1 373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  _V  ->  -.  Lim  suc  z )
17669, 175ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  Lim  suc  z
177 limeq 4596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  -> 
( Lim  y  <->  Lim  suc  z
) )
178176, 177mtbiri 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  suc  z  ->  -.  Lim  y )
179178rexlimivw 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  Lim  y )
180179intnanrd 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  -.  ( Lim  y  /\  x  =  U. ( f "
y ) ) )
181 orel1 373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( suc  z  =/=  (/)  <->  -.  suc  z  =  (/) )
184145, 183mpbi 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  -.  suc  z  =  (/)
185 iffalse 3748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -. 
suc  z  =  (/)  ->  if ( suc  z  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  suc  z ,  U. (
f " y ) ,  ( F `  ( f `  U. suc  z ) ) ) )  =  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) ) )
186184, 185ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  if ( suc  z  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) ) )  =  if ( Lim  suc  z ,  U. ( f "
y ) ,  ( F `  ( f `
 U. suc  z
) ) )
187 iffalse 3748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -. 
Lim  suc  z  ->  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) ) )
18869, 175, 187mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) )  =  ( F `
 ( f `  U. suc  z ) )
189186, 188eqtri 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  if ( suc  z  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) ) )  =  ( F `  ( f `
 U. suc  z
) )
190 eqeq1 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  suc  z  -> 
( y  =  (/)  <->  suc  z  =  (/) ) )
191 unieq 4026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  suc  z  ->  U. y  =  U. suc  z )
192191fveq2d 5735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  suc  z  -> 
( f `  U. y )  =  ( f `  U. suc  z ) )
193192fveq2d 5735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  suc  z  -> 
( F `  (
f `  U. y ) )  =  ( F `
 ( f `  U. suc  z ) ) )
194177, 193ifbieq2d 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  suc  z  ->  if ( Lim  y , 
U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) )  =  if ( Lim  suc  z ,  U. ( f "
y ) ,  ( F `  ( f `
 U. suc  z
) ) ) )
195190, 194ifbieq2d 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  suc  z  ->  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  =  if ( suc  z  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  suc  z ,  U. ( f " y
) ,  ( F `
 ( f `  U. suc  z ) ) ) ) )
196189, 195, 1933eqtr4a 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  suc  z  ->  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  =  ( F `
 ( f `  U. y ) ) )
197196rexlimivw 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. z  e.  On  y  =  suc  z  ->  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  =  ( F `
 ( f `  U. y ) ) )
198197eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( E. z  e.  On  y  =  suc  z  ->  (
x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  <->  x  =  ( F `  ( f `
 U. y ) ) ) )
199198biimprd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. z  e.  On  y  =  suc  z  ->  (
x  =  ( F `
 ( f `  U. y ) )  ->  x  =  if (
y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) )
200199adantld 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. z  e.  On  y  =  suc  z  ->  (
( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) )  ->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
201174, 182, 2003syld 54 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( E. z  e.  On  y  =  suc  z  ->  (
( ( y  =  (/)  /\  x  =  U. { A } )  \/  ( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )  ->  x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
202 rexex 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. z  e.  On  y  =  suc  z  ->  E. z 
y  =  suc  z
)
203198biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. z  e.  On  y  =  suc  z  ->  (
x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  ->  x  =  ( F `  ( f `  U. y ) ) ) )
204 olc 375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) )  ->  ( ( Lim  y  /\  x  = 
U. ( f "
y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )
205204olcd 384 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) )  ->  ( ( y  =  (/)  /\  x  =  U. { A }
)  \/  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) ) )
206202, 203, 205ee12an 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( E. z  e.  On  y  =  suc  z  ->  (
x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  -> 
( ( y  =  (/)  /\  x  =  U. { A } )  \/  ( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) ) ) )
207201, 206impbid 185 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( E. z  e.  On  y  =  suc  z  ->  (
( ( y  =  (/)  /\  x  =  U. { A } )  \/  ( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )  <->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
208143con2i 115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  y  =  (/) )
209208intnanrd 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  (
y  =  (/)  /\  x  =  U. { A }
) )
210209, 173syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Lim  y  ->  ( (
( y  =  (/)  /\  x  =  U. { A } )  \/  (
( Lim  y  /\  x  =  U. (
f " y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `
 U. y ) ) ) ) )  ->  ( ( Lim  y  /\  x  = 
U. ( f "
y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) ) )
211178exlimiv 1645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. z  y  =  suc  z  ->  -.  Lim  y )
212211con2i 115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  -.  E. z 
y  =  suc  z
)
213212intnanrd 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )
214 orel2 374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) )  ->  ( ( ( Lim  y  /\  x  =  U. ( f "
y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) )  ->  ( Lim  y  /\  x  =  U. ( f " y
) ) ) )
215213, 214syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Lim  y  ->  ( (
( Lim  y  /\  x  =  U. (
f " y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `
 U. y ) ) ) )  -> 
( Lim  y  /\  x  =  U. (
f " y ) ) ) )
216 iffalse 3748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( -.  y  =  (/)  ->  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  =  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )
217208, 216syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( Lim  y  ->  if (
y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  =  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )
218 iftrue 3747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( Lim  y  ->  if ( Lim  y ,  U. (
f " y ) ,  ( F `  ( f `  U. y ) ) )  =  U. ( f
" y ) )
219217, 218eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Lim  y  ->  if (
y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  = 
U. ( f "
y ) )
220219eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Lim  y  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  <->  x  =  U. ( f " y
) ) )
221220biimprd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  ( x  =  U. ( f "
y )  ->  x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
222221adantld 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Lim  y  ->  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  ->  x  =  if (
y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) )
223210, 215, 2223syld 54 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Lim  y  ->  ( (
( y  =  (/)  /\  x  =  U. { A } )  \/  (
( Lim  y  /\  x  =  U. (
f " y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `
 U. y ) ) ) ) )  ->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
224223adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  _V  /\  Lim  y )  ->  (
( ( y  =  (/)  /\  x  =  U. { A } )  \/  ( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )  ->  x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
225220biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Lim  y  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  ->  x  =  U. ( f " y
) ) )
226225anc2li 542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Lim  y  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  ->  ( Lim  y  /\  x  =  U. ( f " y
) ) ) )
227 orc 376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  -> 
( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )
228227olcd 384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  -> 
( ( y  =  (/)  /\  x  =  U. { A } )  \/  ( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) ) )
229226, 228syl6 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Lim  y  ->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  ->  ( (
y  =  (/)  /\  x  =  U. { A }
)  \/  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) ) ) )
230229adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  _V  /\  Lim  y )  ->  (
x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  -> 
( ( y  =  (/)  /\  x  =  U. { A } )  \/  ( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) ) ) )
231224, 230impbid 185 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  e.  _V  /\  Lim  y )  ->  (
( ( y  =  (/)  /\  x  =  U. { A } )  \/  ( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )  <->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
232167, 207, 2313jaoi 1248 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  =  (/)  \/  E. z  e.  On  y  =  suc  z  \/  (
y  e.  _V  /\  Lim  y ) )  -> 
( ( ( y  =  (/)  /\  x  =  U. { A }
)  \/  ( ( Lim  y  /\  x  =  U. ( f "
y ) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )  <->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
233140, 232sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  On  ->  (
( ( y  =  (/)  /\  x  =  U. { A } )  \/  ( ( Lim  y  /\  x  =  U. ( f " y
) )  \/  ( E. z  y  =  suc  z  /\  x  =  ( F `  ( f `  U. y ) ) ) ) )  <->  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
234139, 233syl5bb 250 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  On  ->  ( <. f ,  y >.
( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) x  <-> 
x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) )
23555, 234syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( <. f ,  y
>. ( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) x  <-> 
x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) )
23627, 67brcnv 5058 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x `'Apply <. f ,  y
>. 
<-> 
<. f ,  y >.Apply x )
23712, 41, 27brapply 25788 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
f ,  y >.Apply x 
<->  x  =  ( f `
 y ) )
238236, 237bitri 242 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x `'Apply <. f ,  y
>. 
<->  x  =  ( f `
 y ) )
239238a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( x `'Apply <. f ,  y >.  <->  x  =  ( f `  y
) ) )
240235, 239anbi12d 693 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( ( <. f ,  y >. (
( ( _V  X.  { (/) } )  X. 
{ U. { A } } )  u.  (
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun
F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ ) ) ) ) x  /\  x `'Apply <. f ,  y
>. )  <->  ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) )  /\  x  =  ( f `  y
) ) ) )
241 ancom 439 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  /\  x  =  ( f `  y ) )  <->  ( x  =  ( f `  y )  /\  x  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
242240, 241syl6bb 254 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( ( <. f ,  y >. (
( ( _V  X.  { (/) } )  X. 
{ U. { A } } )  u.  (
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun
F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ ) ) ) ) x  /\  x `'Apply <. f ,  y
>. )  <->  ( x  =  ( f `  y
)  /\  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) ) )
243242exbidv 1637 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( E. x (
<. f ,  y >.
( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) x  /\  x `'Apply <. f ,  y >. )  <->  E. x ( x  =  ( f `  y
)  /\  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) ) )
244 df-br 4216 . . . . . . . . . . . . . . . . . . . 20  |-  ( f Fix ( `'Apply  o.  ( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) y  <->  <. f ,  y
>.  e.  Fix ( `'Apply 
o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) )
24567elfix 25753 . . . . . . . . . . . . . . . . . . . 20  |-  ( <.
f ,  y >.  e.  Fix ( `'Apply  o.  ( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) )  <->  <. f ,  y >.
( `'Apply  o.  (
( ( _V  X.  { (/) } )  X. 
{ U. { A } } )  u.  (
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun
F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ ) ) ) ) ) <. f ,  y >. )
24667, 67brco 5046 . . . . . . . . . . . . . . . . . . . 20  |-  ( <.
f ,  y >.
( `'Apply  o.  (
( ( _V  X.  { (/) } )  X. 
{ U. { A } } )  u.  (
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun
F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ ) ) ) ) ) <. f ,  y >.  <->  E. x
( <. f ,  y
>. ( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) x  /\  x `'Apply <. f ,  y >. )
)
247244, 245, 2463bitri 264 . . . . . . . . . . . . . . . . . . 19  |-  ( f Fix ( `'Apply  o.  ( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) y  <->  E. x ( <.
f ,  y >.
( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) x  /\  x `'Apply <. f ,  y >. )
)
248 fvex 5745 . . . . . . . . . . . . . . . . . . . 20  |-  ( f `
 y )  e. 
_V
249248eqvinc 3065 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f `  y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  <->  E. x
( x  =  ( f `  y )  /\  x  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
250243, 247, 2493bitr4g 281 . . . . . . . . . . . . . . . . . 18  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( f Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) y  <->  ( f `  y )  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
251250notbid 287 . . . . . . . . . . . . . . . . 17  |-  ( ( Fun  f  /\  dom  f  e.  On  /\  y  e.  dom  f )  -> 
( -.  f Fix ( `'Apply  o.  (
( ( _V  X.  { (/) } )  X. 
{ U. { A } } )  u.  (
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun
F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ ) ) ) ) ) y  <->  -.  (
f `  y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
2522513expia 1156 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  f  /\  dom  f  e.  On )  ->  ( y  e.  dom  f  ->  ( -.  f Fix ( `'Apply  o.  (
( ( _V  X.  { (/) } )  X. 
{ U. { A } } )  u.  (
( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun
F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ ) ) ) ) ) y  <->  -.  (
f `  y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) ) )
253252pm5.32d 622 . . . . . . . . . . . . . . 15  |-  ( ( Fun  f  /\  dom  f  e.  On )  ->  ( ( y  e. 
dom  f  /\  -.  f Fix ( `'Apply  o.  ( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) y )  <->  ( y  e.  dom  f  /\  -.  ( f `  y
)  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) ) )
254 annim 416 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  dom  f  /\  -.  ( f `  y )  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) )  <->  -.  (
y  e.  dom  f  ->  ( f `  y
)  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) )
255253, 254syl6bb 254 . . . . . . . . . . . . . 14  |-  ( ( Fun  f  /\  dom  f  e.  On )  ->  ( ( y  e. 
dom  f  /\  -.  f Fix ( `'Apply  o.  ( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) y )  <->  -.  (
y  e.  dom  f  ->  ( f `  y
)  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) ) )
25653, 255syl5bb 250 . . . . . . . . . . . . 13  |-  ( ( Fun  f  /\  dom  f  e.  On )  ->  ( f ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) y  <->  -.  (
y  e.  dom  f  ->  ( f `  y
)  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) ) )
257256exbidv 1637 . . . . . . . . . . . 12  |-  ( ( Fun  f  /\  dom  f  e.  On )  ->  ( E. y  f ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) y  <->  E. y  -.  ( y  e.  dom  f  ->  ( f `  y )  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) ) )
258 exnal 1584 . . . . . . . . . . . 12  |-  ( E. y  -.  ( y  e.  dom  f  -> 
( f `  y
)  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) )  <->  -.  A. y ( y  e.  dom  f  -> 
( f `  y
)  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) )
259257, 258syl6rbb 255 . . . . . . . . . . 11  |-  ( ( Fun  f  /\  dom  f  e.  On )  ->  ( -.  A. y
( y  e.  dom  f  ->  ( f `  y )  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) )  <->  E. y 
f ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) y ) )
26012eldm 5070 . . . . . . . . . . 11  |-  ( f  e.  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) )  <->  E. y  f ( ( `'  _E  o. Domain ) 
\  Fix ( `'Apply  o.  ( ( ( _V 
X.  { (/) } )  X.  { U. { A } } )  u.  ( ( ( Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) y )
261259, 260syl6bbr 256 . . . . . . . . . 10  |-  ( ( Fun  f  /\  dom  f  e.  On )  ->  ( -.  A. y
( y  e.  dom  f  ->  ( f `  y )  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) )  <->  f  e.  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) ) )
262261con1bid 322 . . . . . . . . 9  |-  ( ( Fun  f  /\  dom  f  e.  On )  ->  ( -.  f  e. 
dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) )  <->  A. y ( y  e.  dom  f  -> 
( f `  y
)  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) ) )
263 df-ral 2712 . . . . . . . . 9  |-  ( A. y  e.  dom  f ( f `  y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) )  <->  A. y
( y  e.  dom  f  ->  ( f `  y )  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
264262, 263syl6bbr 256 . . . . . . . 8  |-  ( ( Fun  f  /\  dom  f  e.  On )  ->  ( -.  f  e. 
dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) )  <->  A. y  e.  dom  f ( f `  y )  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
265264pm5.32i 620 . . . . . . 7  |-  ( ( ( Fun  f  /\  dom  f  e.  On )  /\  -.  f  e. 
dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) )  <->  ( ( Fun  f  /\  dom  f  e.  On )  /\  A. y  e.  dom  f ( f `  y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) )
266 anass 632 . . . . . . 7  |-  ( ( ( Fun  f  /\  dom  f  e.  On )  /\  A. y  e. 
dom  f ( f `
 y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) )  <->  ( Fun  f  /\  ( dom  f  e.  On  /\  A. y  e.  dom  f ( f `
 y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) ) )
267265, 266bitri 242 . . . . . 6  |-  ( ( ( Fun  f  /\  dom  f  e.  On )  /\  -.  f  e. 
dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) )  <->  ( Fun  f  /\  ( dom  f  e.  On  /\  A. y  e.  dom  f ( f `
 y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) ) )
26821, 39, 2673bitri 264 . . . . 5  |-  ( f  e.  ( ( Funs 
i^i  ( `'Domain " On ) )  \  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) )  <->  ( Fun  f  /\  ( dom  f  e.  On  /\  A. y  e.  dom  f ( f `
 y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) ) )
26919, 20, 2683bitr4ri 271 . . . 4  |-  ( f  e.  ( ( Funs 
i^i  ( `'Domain " On ) )  \  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) )  <->  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) )
270269abbi2i 2549 . . 3  |-  ( (
Funs  i^i  ( `'Domain " On ) )  \  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) )  =  {
f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  if ( y  =  (/) ,  if ( A  e. 
_V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f " y
) ,  ( F `
 ( f `  U. y ) ) ) ) ) }
271270unieqi 4027 . 2  |-  U. (
( Funs  i^i  ( `'Domain " On ) ) 
\  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) )  =  U. { f  |  E. x  e.  On  (
f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  if ( y  =  (/) ,  if ( A  e.  _V ,  A ,  (/) ) ,  if ( Lim  y ,  U. ( f "
y ) ,  ( F `  ( f `
 U. y ) ) ) ) ) }
2721, 271eqtr4i 2461 1  |-  rec ( F ,  A )  =  U. ( ( Funs 
i^i  ( `'Domain " On ) )  \  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  ( ( ( _V  X.  { (/) } )  X.  { U. { A } } )  u.  ( ( (
Bigcup  o. Img )  |`  ( _V  X.  Limits ) )  u.  ( (FullFun F  o.  (Apply  o. pprod (  _I  ,  Bigcup ) ) )  |`  ( _V  X.  ran Succ )
) ) ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360    \/ w3o 936    /\ w3a 937   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726   {cab 2424    =/= wne 2601   A.wral 2707   E.wrex 2708   _Vcvv 2958    \ cdif 3319    u. cun 3320    i^i cin 3321   (/)c0 3630   ifcif 3741   {csn 3816   <.cop 3819   U.cuni 4017   class class class wbr 4215    _E cep 4495    _I cid 4496   Oncon0 4584   Lim wlim 4585   suc csuc 4586    X. cxp 4879   `'ccnv 4880   dom cdm 4881   ran crn 4882    |` cres 4883   "cima 4884    o. ccom 4885   Fun wfun 5451    Fn wfn 5452   ` cfv 5457   reccrdg 6670  pprodcpprod 25680   Bigcupcbigcup 25683   Fixcfix 25684   Limitsclimits 25685   Funscfuns 25686  Imgcimg 25691  Domaincdomain 25692  Applycapply 25694  Succcsuccf 25697  FullFuncfullfn 25699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-1st 6352  df-2nd 6353  df-recs 6636  df-rdg 6671  df-symdif 25668  df-txp 25703  df-pprod 25704  df-bigcup 25707  df-fix 25708  df-limits 25709  df-funs 25710  df-singleton 25711  df-singles 25712  df-image 25713  df-cart 25714  df-img 25715  df-domain 25716  df-cup 25718  df-succf 25721  df-apply 25722  df-funpart 25723  df-fullfun 25724
  Copyright terms: Public domain W3C validator