Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aomclem8 Unicode version

Theorem aomclem8 26828
Description: Lemma for dfac11 26829. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.)
Hypotheses
Ref Expression
aomclem8.a  |-  ( ph  ->  A  e.  On )
aomclem8.y  |-  ( ph  ->  A. a  e.  ~P  ( R1 `  A ) ( a  =/=  (/)  ->  (
y `  a )  e.  ( ( ~P a  i^i  Fin )  \  { (/)
} ) ) )
Assertion
Ref Expression
aomclem8  |-  ( ph  ->  E. b  b  We  ( R1 `  A
) )
Distinct variable groups:    ph, b    A, a, b    y, a, b
Allowed substitution hints:    ph( y, a)    A( y)

Proof of Theorem aomclem8
Dummy variables  c 
d  e  f  g  h  i  j  l are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elequ2 1722 . . . . . . 7  |-  ( h  =  b  ->  (
i  e.  h  <->  i  e.  b ) )
2 elequ2 1722 . . . . . . . 8  |-  ( g  =  c  ->  (
i  e.  g  <->  i  e.  c ) )
32notbid 286 . . . . . . 7  |-  ( g  =  c  ->  ( -.  i  e.  g  <->  -.  i  e.  c ) )
41, 3bi2anan9r 845 . . . . . 6  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( i  e.  h  /\  -.  i  e.  g )  <->  ( i  e.  b  /\  -.  i  e.  c ) ) )
5 elequ2 1722 . . . . . . . . 9  |-  ( g  =  c  ->  (
j  e.  g  <->  j  e.  c ) )
6 elequ2 1722 . . . . . . . . 9  |-  ( h  =  b  ->  (
j  e.  h  <->  j  e.  b ) )
75, 6bi2bian9 846 . . . . . . . 8  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( j  e.  g  <->  j  e.  h
)  <->  ( j  e.  c  <->  j  e.  b ) ) )
87imbi2d 308 . . . . . . 7  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) )  <->  ( j ( e `  U. dom  e ) i  -> 
( j  e.  c  <-> 
j  e.  b ) ) ) )
98ralbidv 2669 . . . . . 6  |-  ( ( g  =  c  /\  h  =  b )  ->  ( A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) )  <->  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  c  <-> 
j  e.  b ) ) ) )
104, 9anbi12d 692 . . . . 5  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) )  <->  ( (
i  e.  b  /\  -.  i  e.  c
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  c  <-> 
j  e.  b ) ) ) ) )
1110rexbidv 2670 . . . 4  |-  ( ( g  =  c  /\  h  =  b )  ->  ( E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) )  <->  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  b  /\  -.  i  e.  c
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  c  <-> 
j  e.  b ) ) ) ) )
12 elequ1 1720 . . . . . . 7  |-  ( i  =  d  ->  (
i  e.  b  <->  d  e.  b ) )
13 elequ1 1720 . . . . . . . 8  |-  ( i  =  d  ->  (
i  e.  c  <->  d  e.  c ) )
1413notbid 286 . . . . . . 7  |-  ( i  =  d  ->  ( -.  i  e.  c  <->  -.  d  e.  c ) )
1512, 14anbi12d 692 . . . . . 6  |-  ( i  =  d  ->  (
( i  e.  b  /\  -.  i  e.  c )  <->  ( d  e.  b  /\  -.  d  e.  c ) ) )
16 breq2 4157 . . . . . . . . 9  |-  ( i  =  d  ->  (
j ( e `  U. dom  e ) i  <-> 
j ( e `  U. dom  e ) d ) )
1716imbi1d 309 . . . . . . . 8  |-  ( i  =  d  ->  (
( j ( e `
 U. dom  e
) i  ->  (
j  e.  c  <->  j  e.  b ) )  <->  ( j
( e `  U. dom  e ) d  -> 
( j  e.  c  <-> 
j  e.  b ) ) ) )
1817ralbidv 2669 . . . . . . 7  |-  ( i  =  d  ->  ( A. j  e.  ( R1 `  U. dom  e
) ( j ( e `  U. dom  e ) i  -> 
( j  e.  c  <-> 
j  e.  b ) )  <->  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) d  -> 
( j  e.  c  <-> 
j  e.  b ) ) ) )
19 breq1 4156 . . . . . . . . 9  |-  ( j  =  f  ->  (
j ( e `  U. dom  e ) d  <-> 
f ( e `  U. dom  e ) d ) )
20 elequ1 1720 . . . . . . . . . 10  |-  ( j  =  f  ->  (
j  e.  c  <->  f  e.  c ) )
21 elequ1 1720 . . . . . . . . . 10  |-  ( j  =  f  ->  (
j  e.  b  <->  f  e.  b ) )
2220, 21bibi12d 313 . . . . . . . . 9  |-  ( j  =  f  ->  (
( j  e.  c  <-> 
j  e.  b )  <-> 
( f  e.  c  <-> 
f  e.  b ) ) )
2319, 22imbi12d 312 . . . . . . . 8  |-  ( j  =  f  ->  (
( j ( e `
 U. dom  e
) d  ->  (
j  e.  c  <->  j  e.  b ) )  <->  ( f
( e `  U. dom  e ) d  -> 
( f  e.  c  <-> 
f  e.  b ) ) ) )
2423cbvralv 2875 . . . . . . 7  |-  ( A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) d  ->  (
j  e.  c  <->  j  e.  b ) )  <->  A. f  e.  ( R1 `  U. dom  e ) ( f ( e `  U. dom  e ) d  -> 
( f  e.  c  <-> 
f  e.  b ) ) )
2518, 24syl6bb 253 . . . . . 6  |-  ( i  =  d  ->  ( A. j  e.  ( R1 `  U. dom  e
) ( j ( e `  U. dom  e ) i  -> 
( j  e.  c  <-> 
j  e.  b ) )  <->  A. f  e.  ( R1 `  U. dom  e ) ( f ( e `  U. dom  e ) d  -> 
( f  e.  c  <-> 
f  e.  b ) ) ) )
2615, 25anbi12d 692 . . . . 5  |-  ( i  =  d  ->  (
( ( i  e.  b  /\  -.  i  e.  c )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  c  <->  j  e.  b ) ) )  <-> 
( ( d  e.  b  /\  -.  d  e.  c )  /\  A. f  e.  ( R1 ` 
U. dom  e )
( f ( e `
 U. dom  e
) d  ->  (
f  e.  c  <->  f  e.  b ) ) ) ) )
2726cbvrexv 2876 . . . 4  |-  ( E. i  e.  ( R1
`  U. dom  e ) ( ( i  e.  b  /\  -.  i  e.  c )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  c  <->  j  e.  b ) ) )  <->  E. d  e.  ( R1 `  U. dom  e
) ( ( d  e.  b  /\  -.  d  e.  c )  /\  A. f  e.  ( R1 `  U. dom  e ) ( f ( e `  U. dom  e ) d  -> 
( f  e.  c  <-> 
f  e.  b ) ) ) )
2811, 27syl6bb 253 . . 3  |-  ( ( g  =  c  /\  h  =  b )  ->  ( E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) )  <->  E. d  e.  ( R1 `  U. dom  e ) ( ( d  e.  b  /\  -.  d  e.  c
)  /\  A. f  e.  ( R1 `  U. dom  e ) ( f ( e `  U. dom  e ) d  -> 
( f  e.  c  <-> 
f  e.  b ) ) ) ) )
2928cbvopabv 4218 . 2  |-  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) }  =  { <. c ,  b >.  |  E. d  e.  ( R1 ` 
U. dom  e )
( ( d  e.  b  /\  -.  d  e.  c )  /\  A. f  e.  ( R1 ` 
U. dom  e )
( f ( e `
 U. dom  e
) d  ->  (
f  e.  c  <->  f  e.  b ) ) ) }
30 nfcv 2523 . . 3  |-  F/_ c sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } )
31 nfcv 2523 . . . 4  |-  F/_ g
( y `  c
)
32 nfcv 2523 . . . 4  |-  F/_ g
( R1 `  dom  e )
33 nfopab1 4215 . . . 4  |-  F/_ g { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) }
3431, 32, 33nfsup 7389 . . 3  |-  F/_ g sup ( ( y `  c ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } )
35 fveq2 5668 . . . 4  |-  ( g  =  c  ->  (
y `  g )  =  ( y `  c ) )
3635supeq1d 7386 . . 3  |-  ( g  =  c  ->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } )  =  sup ( ( y `  c ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) )
3730, 34, 36cbvmpt 4240 . 2  |-  ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) )  =  ( c  e.  _V  |->  sup (
( y `  c
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) )
38 nfcv 2523 . . . 4  |-  F/_ c
( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) )
39 nffvmpt1 5676 . . . 4  |-  F/_ g
( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  c ) )
40 rneq 5035 . . . . . 6  |-  ( g  =  c  ->  ran  g  =  ran  c )
4140difeq2d 3408 . . . . 5  |-  ( g  =  c  ->  (
( R1 `  dom  e )  \  ran  g )  =  ( ( R1 `  dom  e )  \  ran  c ) )
4241fveq2d 5672 . . . 4  |-  ( g  =  c  ->  (
( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) )  =  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  c ) ) )
4338, 39, 42cbvmpt 4240 . . 3  |-  ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) )  =  ( c  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  c ) ) )
44 recseq 6570 . . 3  |-  ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) )  =  ( c  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  c ) ) )  -> recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) )  = recs ( ( c  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  c ) ) ) ) )
4543, 44ax-mp 8 . 2  |- recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) )  = recs ( ( c  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  c ) ) ) )
46 nfv 1626 . . 3  |-  F/ c
|^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } )
47 nfv 1626 . . 3  |-  F/ b
|^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } )
48 nfmpt1 4239 . . . . . . . 8  |-  F/_ g
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) )
4948nfrecs 6571 . . . . . . 7  |-  F/_ grecs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) )
5049nfcnv 4991 . . . . . 6  |-  F/_ g `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) )
51 nfcv 2523 . . . . . 6  |-  F/_ g { c }
5250, 51nfima 5151 . . . . 5  |-  F/_ g
( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { c } )
5352nfint 4002 . . . 4  |-  F/_ g |^| ( `'recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) " { c } )
54 nfcv 2523 . . . . . 6  |-  F/_ g { b }
5550, 54nfima 5151 . . . . 5  |-  F/_ g
( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } )
5655nfint 4002 . . . 4  |-  F/_ g |^| ( `'recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) " { b } )
5753, 56nfel 2531 . . 3  |-  F/ g
|^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { c } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } )
58 nfcv 2523 . . . . . . . . 9  |-  F/_ h _V
59 nfcv 2523 . . . . . . . . . . . 12  |-  F/_ h
( y `  g
)
60 nfcv 2523 . . . . . . . . . . . 12  |-  F/_ h
( R1 `  dom  e )
61 nfopab2 4216 . . . . . . . . . . . 12  |-  F/_ h { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) }
6259, 60, 61nfsup 7389 . . . . . . . . . . 11  |-  F/_ h sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } )
6358, 62nfmpt 4238 . . . . . . . . . 10  |-  F/_ h
( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) )
64 nfcv 2523 . . . . . . . . . 10  |-  F/_ h
( ( R1 `  dom  e )  \  ran  g )
6563, 64nffv 5675 . . . . . . . . 9  |-  F/_ h
( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) )
6658, 65nfmpt 4238 . . . . . . . 8  |-  F/_ h
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) )
6766nfrecs 6571 . . . . . . 7  |-  F/_ hrecs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) )
6867nfcnv 4991 . . . . . 6  |-  F/_ h `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) )
69 nfcv 2523 . . . . . 6  |-  F/_ h { c }
7068, 69nfima 5151 . . . . 5  |-  F/_ h
( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { c } )
7170nfint 4002 . . . 4  |-  F/_ h |^| ( `'recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) " { c } )
72 nfcv 2523 . . . . . 6  |-  F/_ h { b }
7368, 72nfima 5151 . . . . 5  |-  F/_ h
( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } )
7473nfint 4002 . . . 4  |-  F/_ h |^| ( `'recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) " { b } )
7571, 74nfel 2531 . . 3  |-  F/ h |^| ( `'recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) " { c } )  e.  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } )
76 sneq 3768 . . . . . 6  |-  ( g  =  c  ->  { g }  =  { c } )
7776imaeq2d 5143 . . . . 5  |-  ( g  =  c  ->  ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  =  ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { c } ) )
7877inteqd 3997 . . . 4  |-  ( g  =  c  ->  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  =  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { c } ) )
79 sneq 3768 . . . . . 6  |-  ( h  =  b  ->  { h }  =  { b } )
8079imaeq2d 5143 . . . . 5  |-  ( h  =  b  ->  ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } )  =  ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } ) )
8180inteqd 3997 . . . 4  |-  ( h  =  b  ->  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } )  =  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } ) )
82 eleq12 2449 . . . 4  |-  ( (
|^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  =  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { c } )  /\  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } )  =  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } ) )  ->  ( |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } )  <->  |^| ( `'recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) " { c } )  e.  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } ) ) )
8378, 81, 82syl2an 464 . . 3  |-  ( ( g  =  c  /\  h  =  b )  ->  ( |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } )  <->  |^| ( `'recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) " { c } )  e.  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } ) ) )
8446, 47, 57, 75, 83cbvopab 4217 . 2  |-  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) }  =  { <. c ,  b >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { c } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { b } ) }
85 fveq2 5668 . . . . 5  |-  ( g  =  c  ->  ( rank `  g )  =  ( rank `  c
) )
86 fveq2 5668 . . . . 5  |-  ( h  =  b  ->  ( rank `  h )  =  ( rank `  b
) )
8785, 86breqan12d 4168 . . . 4  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( rank `  g
)  _E  ( rank `  h )  <->  ( rank `  c )  _E  ( rank `  b ) ) )
8885, 86eqeqan12d 2402 . . . . 5  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( rank `  g
)  =  ( rank `  h )  <->  ( rank `  c )  =  (
rank `  b )
) )
89 simpl 444 . . . . . 6  |-  ( ( g  =  c  /\  h  =  b )  ->  g  =  c )
90 suceq 4587 . . . . . . . . 9  |-  ( (
rank `  g )  =  ( rank `  c
)  ->  suc  ( rank `  g )  =  suc  ( rank `  c )
)
9185, 90syl 16 . . . . . . . 8  |-  ( g  =  c  ->  suc  ( rank `  g )  =  suc  ( rank `  c
) )
9291adantr 452 . . . . . . 7  |-  ( ( g  =  c  /\  h  =  b )  ->  suc  ( rank `  g
)  =  suc  ( rank `  c ) )
9392fveq2d 5672 . . . . . 6  |-  ( ( g  =  c  /\  h  =  b )  ->  ( e `  suc  ( rank `  g )
)  =  ( e `
 suc  ( rank `  c ) ) )
94 simpr 448 . . . . . 6  |-  ( ( g  =  c  /\  h  =  b )  ->  h  =  b )
9589, 93, 94breq123d 4167 . . . . 5  |-  ( ( g  =  c  /\  h  =  b )  ->  ( g ( e `
 suc  ( rank `  g ) ) h  <-> 
c ( e `  suc  ( rank `  c
) ) b ) )
9688, 95anbi12d 692 . . . 4  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( ( rank `  g )  =  (
rank `  h )  /\  g ( e `  suc  ( rank `  g
) ) h )  <-> 
( ( rank `  c
)  =  ( rank `  b )  /\  c
( e `  suc  ( rank `  c )
) b ) ) )
9787, 96orbi12d 691 . . 3  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( e `  suc  ( rank `  g )
) h ) )  <-> 
( ( rank `  c
)  _E  ( rank `  b )  \/  (
( rank `  c )  =  ( rank `  b
)  /\  c (
e `  suc  ( rank `  c ) ) b ) ) ) )
9897cbvopabv 4218 . 2  |-  { <. g ,  h >.  |  ( ( rank `  g
)  _E  ( rank `  h )  \/  (
( rank `  g )  =  ( rank `  h
)  /\  g (
e `  suc  ( rank `  g ) ) h ) ) }  =  { <. c ,  b
>.  |  ( ( rank `  c )  _E  ( rank `  b
)  \/  ( (
rank `  c )  =  ( rank `  b
)  /\  c (
e `  suc  ( rank `  c ) ) b ) ) }
99 eqid 2387 . 2  |-  ( if ( dom  e  = 
U. dom  e ,  { <. g ,  h >.  |  ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( e `  suc  ( rank `  g )
) h ) ) } ,  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) } )  i^i  (
( R1 `  dom  e )  X.  ( R1 `  dom  e ) ) )  =  ( if ( dom  e  =  U. dom  e ,  { <. g ,  h >.  |  ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( e `  suc  ( rank `  g )
) h ) ) } ,  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) } )  i^i  (
( R1 `  dom  e )  X.  ( R1 `  dom  e ) ) )
100 dmeq 5010 . . . . . . 7  |-  ( l  =  e  ->  dom  l  =  dom  e )
101100unieqd 3968 . . . . . . 7  |-  ( l  =  e  ->  U. dom  l  =  U. dom  e
)
102100, 101eqeq12d 2401 . . . . . 6  |-  ( l  =  e  ->  ( dom  l  =  U. dom  l  <->  dom  e  =  U. dom  e ) )
103 fveq1 5667 . . . . . . . . . 10  |-  ( l  =  e  ->  (
l `  suc  ( rank `  g ) )  =  ( e `  suc  ( rank `  g )
) )
104103breqd 4164 . . . . . . . . 9  |-  ( l  =  e  ->  (
g ( l `  suc  ( rank `  g
) ) h  <->  g (
e `  suc  ( rank `  g ) ) h ) )
105104anbi2d 685 . . . . . . . 8  |-  ( l  =  e  ->  (
( ( rank `  g
)  =  ( rank `  h )  /\  g
( l `  suc  ( rank `  g )
) h )  <->  ( ( rank `  g )  =  ( rank `  h
)  /\  g (
e `  suc  ( rank `  g ) ) h ) ) )
106105orbi2d 683 . . . . . . 7  |-  ( l  =  e  ->  (
( ( rank `  g
)  _E  ( rank `  h )  \/  (
( rank `  g )  =  ( rank `  h
)  /\  g (
l `  suc  ( rank `  g ) ) h ) )  <->  ( ( rank `  g )  _E  ( rank `  h
)  \/  ( (
rank `  g )  =  ( rank `  h
)  /\  g (
e `  suc  ( rank `  g ) ) h ) ) ) )
107106opabbidv 4212 . . . . . 6  |-  ( l  =  e  ->  { <. g ,  h >.  |  ( ( rank `  g
)  _E  ( rank `  h )  \/  (
( rank `  g )  =  ( rank `  h
)  /\  g (
l `  suc  ( rank `  g ) ) h ) ) }  =  { <. g ,  h >.  |  ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( e `  suc  ( rank `  g )
) h ) ) } )
108 eqidd 2388 . . . . . . . . . . . . . . . 16  |-  ( l  =  e  ->  (
y `  g )  =  ( y `  g ) )
109100fveq2d 5672 . . . . . . . . . . . . . . . 16  |-  ( l  =  e  ->  ( R1 `  dom  l )  =  ( R1 `  dom  e ) )
110101fveq2d 5672 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  e  ->  ( R1 `  U. dom  l
)  =  ( R1
`  U. dom  e ) )
111 id 20 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( l  =  e  ->  l  =  e )
112111, 101fveq12d 5674 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  e  ->  (
l `  U. dom  l
)  =  ( e `
 U. dom  e
) )
113112breqd 4164 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  e  ->  (
j ( l `  U. dom  l ) i  <-> 
j ( e `  U. dom  e ) i ) )
114113imbi1d 309 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  e  ->  (
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) )  <->  ( j
( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) )
115110, 114raleqbidv 2859 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  e  ->  ( A. j  e.  ( R1 `  U. dom  l
) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) )  <->  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) )
116115anbi2d 685 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  e  ->  (
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) )  <-> 
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) ) )
117110, 116rexeqbidv 2860 . . . . . . . . . . . . . . . . 17  |-  ( l  =  e  ->  ( E. i  e.  ( R1 `  U. dom  l
) ( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) )  <->  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) ) )
118117opabbidv 4212 . . . . . . . . . . . . . . . 16  |-  ( l  =  e  ->  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  l )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) }  =  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } )
119108, 109, 118supeq123d 26827 . . . . . . . . . . . . . . 15  |-  ( l  =  e  ->  sup ( ( y `  g ) ,  ( R1 `  dom  l
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  l )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } )  =  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) )
120119mpteq2dv 4237 . . . . . . . . . . . . . 14  |-  ( l  =  e  ->  (
g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  l
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  l )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) )  =  ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) )
121109difeq1d 3407 . . . . . . . . . . . . . 14  |-  ( l  =  e  ->  (
( R1 `  dom  l )  \  ran  g )  =  ( ( R1 `  dom  e )  \  ran  g ) )
122120, 121fveq12d 5674 . . . . . . . . . . . . 13  |-  ( l  =  e  ->  (
( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  l
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  l )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l )  \  ran  g ) )  =  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) )
123122mpteq2dv 4237 . . . . . . . . . . . 12  |-  ( l  =  e  ->  (
g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  l
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  l )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l )  \  ran  g ) ) )  =  ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) )
124 recseq 6570 . . . . . . . . . . . 12  |-  ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  l
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  l )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l )  \  ran  g ) ) )  =  ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) )  -> recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  l
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  l )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l )  \  ran  g ) ) ) )  = recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) )
125123, 124syl 16 . . . . . . . . . . 11  |-  ( l  =  e  -> recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  l
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  l )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l )  \  ran  g ) ) ) )  = recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) )
126125cnveqd 4988 . . . . . . . . . 10  |-  ( l  =  e  ->  `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) )  =  `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) )
127126imaeq1d 5142 . . . . . . . . 9  |-  ( l  =  e  ->  ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { g } )  =  ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } ) )
128127inteqd 3997 . . . . . . . 8  |-  ( l  =  e  ->  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { g } )  =  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } ) )
129126imaeq1d 5142 . . . . . . . . 9  |-  ( l  =  e  ->  ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { h } )  =  ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) )
130129inteqd 3997 . . . . . . . 8  |-  ( l  =  e  ->  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { h } )  =  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) )
131128, 130eleq12d 2455 . . . . . . 7  |-  ( l  =  e  ->  ( |^| ( `'recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  l
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  l )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  l )
( j ( l `
 U. dom  l
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l )  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { h } )  <->  |^| ( `'recs ( ( g  e.  _V  |->  ( ( g  e.  _V  |->  sup ( ( y `  g ) ,  ( R1 `  dom  e
) ,  { <. g ,  h >.  |  E. i  e.  ( R1 ` 
U. dom  e )
( ( i  e.  h  /\  -.  i  e.  g )  /\  A. j  e.  ( R1 ` 
U. dom  e )
( j ( e `
 U. dom  e
) i  ->  (
j  e.  g  <->  j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e )  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) ) )
132131opabbidv 4212 . . . . . 6  |-  ( l  =  e  ->  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { h } ) }  =  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) } )
133102, 107, 132ifbieq12d 3704 . . . . 5  |-  ( l  =  e  ->  if ( dom  l  =  U. dom  l ,  { <. g ,  h >.  |  ( ( rank `  g
)  _E  ( rank `  h )  \/  (
( rank `  g )  =  ( rank `  h
)  /\  g (
l `  suc  ( rank `  g ) ) h ) ) } ,  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { h } ) } )  =  if ( dom  e  = 
U. dom  e ,  { <. g ,  h >.  |  ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( e `  suc  ( rank `  g )
) h ) ) } ,  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) } ) )
134109, 109xpeq12d 4843 . . . . 5  |-  ( l  =  e  ->  (
( R1 `  dom  l )  X.  ( R1 `  dom  l ) )  =  ( ( R1 `  dom  e
)  X.  ( R1
`  dom  e )
) )
135133, 134ineq12d 3486 . . . 4  |-  ( l  =  e  ->  ( if ( dom  l  = 
U. dom  l ,  { <. g ,  h >.  |  ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( l `  suc  ( rank `  g )
) h ) ) } ,  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { h } ) } )  i^i  (
( R1 `  dom  l )  X.  ( R1 `  dom  l ) ) )  =  ( if ( dom  e  =  U. dom  e ,  { <. g ,  h >.  |  ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( e `  suc  ( rank `  g )
) h ) ) } ,  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) } )  i^i  (
( R1 `  dom  e )  X.  ( R1 `  dom  e ) ) ) )
136135cbvmptv 4241 . . 3  |-  ( l  e.  _V  |->  ( if ( dom  l  = 
U. dom  l ,  { <. g ,  h >.  |  ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( l `  suc  ( rank `  g )
) h ) ) } ,  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { h } ) } )  i^i  (
( R1 `  dom  l )  X.  ( R1 `  dom  l ) ) ) )  =  ( e  e.  _V  |->  ( if ( dom  e  =  U. dom  e ,  { <. g ,  h >.  |  ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( e `  suc  ( rank `  g )
) h ) ) } ,  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  e ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  e ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  e ) ( j ( e `  U. dom  e ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  e
)  \  ran  g ) ) ) ) " { h } ) } )  i^i  (
( R1 `  dom  e )  X.  ( R1 `  dom  e ) ) ) )
137 recseq 6570 . . 3  |-  ( ( l  e.  _V  |->  ( if ( dom  l  =  U. dom  l ,  { <. g ,  h >.  |  ( ( rank `  g )  _E  ( rank `  h )  \/  ( ( rank `  g
)  =  ( rank `  h )  /\  g
( l `  suc  ( rank `  g )
) h ) ) } ,  { <. g ,  h >.  |  |^| ( `'recs ( ( g  e. 
_V  |->  ( ( g  e.  _V  |->  sup (
( y `  g
) ,  ( R1
`  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g ) ) ) ) " { g } )  e.  |^| ( `'recs (
( g  e.  _V  |->  ( ( g  e. 
_V  |->  sup ( ( y `
 g ) ,  ( R1 `  dom  l ) ,  { <. g ,  h >.  |  E. i  e.  ( R1 `  U. dom  l ) ( ( i  e.  h  /\  -.  i  e.  g
)  /\  A. j  e.  ( R1 `  U. dom  l ) ( j ( l `  U. dom  l ) i  -> 
( j  e.  g  <-> 
j  e.  h ) ) ) } ) ) `  ( ( R1 `  dom  l
)  \  ran  g