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

Theorem aomclem8 27262
Description: Lemma for dfac11 27263. 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 1701 . . . . . . 7  |-  ( h  =  b  ->  (
i  e.  h  <->  i  e.  b ) )
2 elequ2 1701 . . . . . . . 8  |-  ( g  =  c  ->  (
i  e.  g  <->  i  e.  c ) )
32notbid 285 . . . . . . 7  |-  ( g  =  c  ->  ( -.  i  e.  g  <->  -.  i  e.  c ) )
41, 3bi2anan9r 844 . . . . . 6  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( i  e.  h  /\  -.  i  e.  g )  <->  ( i  e.  b  /\  -.  i  e.  c ) ) )
5 elequ2 1701 . . . . . . . . 9  |-  ( g  =  c  ->  (
j  e.  g  <->  j  e.  c ) )
6 elequ2 1701 . . . . . . . . 9  |-  ( h  =  b  ->  (
j  e.  h  <->  j  e.  b ) )
75, 6bi2bian9 845 . . . . . . . 8  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( j  e.  g  <->  j  e.  h
)  <->  ( j  e.  c  <->  j  e.  b ) ) )
87imbi2d 307 . . . . . . 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 2576 . . . . . 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 691 . . . . 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 2577 . . . 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 1699 . . . . . . 7  |-  ( i  =  d  ->  (
i  e.  b  <->  d  e.  b ) )
13 elequ1 1699 . . . . . . . 8  |-  ( i  =  d  ->  (
i  e.  c  <->  d  e.  c ) )
1413notbid 285 . . . . . . 7  |-  ( i  =  d  ->  ( -.  i  e.  c  <->  -.  d  e.  c ) )
1512, 14anbi12d 691 . . . . . 6  |-  ( i  =  d  ->  (
( i  e.  b  /\  -.  i  e.  c )  <->  ( d  e.  b  /\  -.  d  e.  c ) ) )
16 breq2 4043 . . . . . . . . 9  |-  ( i  =  d  ->  (
j ( e `  U. dom  e ) i  <-> 
j ( e `  U. dom  e ) d ) )
1716imbi1d 308 . . . . . . . 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 2576 . . . . . . 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 4042 . . . . . . . . 9  |-  ( j  =  f  ->  (
j ( e `  U. dom  e ) d  <-> 
f ( e `  U. dom  e ) d ) )
20 elequ1 1699 . . . . . . . . . 10  |-  ( j  =  f  ->  (
j  e.  c  <->  f  e.  c ) )
21 elequ1 1699 . . . . . . . . . 10  |-  ( j  =  f  ->  (
j  e.  b  <->  f  e.  b ) )
2220, 21bibi12d 312 . . . . . . . . 9  |-  ( j  =  f  ->  (
( j  e.  c  <-> 
j  e.  b )  <-> 
( f  e.  c  <-> 
f  e.  b ) ) )
2319, 22imbi12d 311 . . . . . . . 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 2777 . . . . . . 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 252 . . . . . 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 691 . . . . 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 2778 . . . 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 252 . . 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 4104 . 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 2432 . . 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 2432 . . . 4  |-  F/_ g
( y `  c
)
32 nfcv 2432 . . . 4  |-  F/_ g
( R1 `  dom  e )
33 nfopab1 4101 . . . 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 7218 . . 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 5541 . . . 4  |-  ( g  =  c  ->  (
y `  g )  =  ( y `  c ) )
3635supeq1d 7215 . . 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 4126 . 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 2432 . . . 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 nfmpt1 4125 . . . . 5  |-  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 ) ) ) } ) )
40 nfcv 2432 . . . . 5  |-  F/_ g
( ( R1 `  dom  e )  \  ran  c )
4139, 40nffv 5548 . . . 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 ) )
42 rneq 4920 . . . . . 6  |-  ( g  =  c  ->  ran  g  =  ran  c )
4342difeq2d 3307 . . . . 5  |-  ( g  =  c  ->  (
( R1 `  dom  e )  \  ran  g )  =  ( ( R1 `  dom  e )  \  ran  c ) )
4443fveq2d 5545 . . . 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 ) ) )
4538, 41, 44cbvmpt 4126 . . 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 ) ) )
46 recseq 6405 . . 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 ) ) ) ) )
4745, 46ax-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 ) ) ) )
48 nfv 1609 . . 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 } )
49 nfv 1609 . . 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 } )
50 nfmpt1 4125 . . . . . . . 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 ) ) )
5150nfrecs 6406 . . . . . . 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 ) ) ) )
5251nfcnv 4876 . . . . . 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 ) ) ) )
53 nfcv 2432 . . . . . 6  |-  F/_ g { c }
5452, 53nfima 5036 . . . . 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 } )
5554nfint 3888 . . . 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 } )
56 nfcv 2432 . . . . . 6  |-  F/_ g { b }
5752, 56nfima 5036 . . . . 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 } )
5857nfint 3888 . . . 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 } )
5955, 58nfel 2440 . . 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 } )
60 nfcv 2432 . . . . . . . . 9  |-  F/_ h _V
61 nfcv 2432 . . . . . . . . . . . 12  |-  F/_ h
( y `  g
)
62 nfcv 2432 . . . . . . . . . . . 12  |-  F/_ h
( R1 `  dom  e )
63 nfopab2 4102 . . . . . . . . . . . 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 ) ) ) }
6461, 62, 63nfsup 7218 . . . . . . . . . . 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 ) ) ) } )
6560, 64nfmpt 4124 . . . . . . . . . 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 ) ) ) } ) )
66 nfcv 2432 . . . . . . . . . 10  |-  F/_ h
( ( R1 `  dom  e )  \  ran  g )
6765, 66nffv 5548 . . . . . . . . 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 ) )
6860, 67nfmpt 4124 . . . . . . . 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 ) ) )
6968nfrecs 6406 . . . . . . 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 ) ) ) )
7069nfcnv 4876 . . . . . 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 ) ) ) )
71 nfcv 2432 . . . . . 6  |-  F/_ h { c }
7270, 71nfima 5036 . . . . 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 } )
7372nfint 3888 . . . 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 } )
74 nfcv 2432 . . . . . 6  |-  F/_ h { b }
7570, 74nfima 5036 . . . . 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 } )
7675nfint 3888 . . . 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 } )
7773, 76nfel 2440 . . 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 } )
78 sneq 3664 . . . . . 6  |-  ( g  =  c  ->  { g }  =  { c } )
7978imaeq2d 5028 . . . . 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 } ) )
8079inteqd 3883 . . . 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 } ) )
81 sneq 3664 . . . . . 6  |-  ( h  =  b  ->  { h }  =  { b } )
8281imaeq2d 5028 . . . . 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 } ) )
8382inteqd 3883 . . . 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 } ) )
84 eleq12 2358 . . . 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 } ) ) )
8580, 83, 84syl2an 463 . . 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 } ) ) )
8648, 49, 59, 77, 85cbvopab 4103 . 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 } ) }
87 fveq2 5541 . . . . 5  |-  ( g  =  c  ->  ( rank `  g )  =  ( rank `  c
) )
88 fveq2 5541 . . . . 5  |-  ( h  =  b  ->  ( rank `  h )  =  ( rank `  b
) )
8987, 88breqan12d 4054 . . . 4  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( rank `  g
)  _E  ( rank `  h )  <->  ( rank `  c )  _E  ( rank `  b ) ) )
9087, 88eqeqan12d 2311 . . . . 5  |-  ( ( g  =  c  /\  h  =  b )  ->  ( ( rank `  g
)  =  ( rank `  h )  <->  ( rank `  c )  =  (
rank `  b )
) )
91 simpl 443 . . . . . 6  |-  ( ( g  =  c  /\  h  =  b )  ->  g  =  c )
92 suceq 4473 . . . . . . . . 9  |-  ( (
rank `  g )  =  ( rank `  c
)  ->  suc  ( rank `  g )  =  suc  ( rank `  c )
)
9387, 92syl 15 . . . . . . . 8  |-  ( g  =  c  ->  suc  ( rank `  g )  =  suc  ( rank `  c
) )
9493adantr 451 . . . . . . 7  |-  ( ( g  =  c  /\  h  =  b )  ->  suc  ( rank `  g
)  =  suc  ( rank `  c ) )
9594fveq2d 5545 . . . . . 6  |-  ( ( g  =  c  /\  h  =  b )  ->  ( e `  suc  ( rank `  g )
)  =  ( e `
 suc  ( rank `  c ) ) )
96 simpr 447 . . . . . 6  |-  ( ( g  =  c  /\  h  =  b )  ->  h  =  b )
9791, 95, 96breq123d 4053 . . . . 5  |-  ( ( g  =  c  /\  h  =  b )  ->  ( g ( e `
 suc  ( rank `  g ) ) h  <-> 
c ( e `  suc  ( rank `  c
) ) b ) )
9890, 97anbi12d 691 . . . 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 ) ) )
9989, 98orbi12d 690 . . 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 ) ) ) )
10099cbvopabv 4104 . 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 ) ) }
101 eqid 2296 . 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 ) ) )
102 dmeq 4895 . . . . . . 7  |-  ( l  =  e  ->  dom  l  =  dom  e )
103102unieqd 3854 . . . . . . 7  |-  ( l  =  e  ->  U. dom  l  =  U. dom  e
)
104102, 103eqeq12d 2310 . . . . . 6  |-  ( l  =  e  ->  ( dom  l  =  U. dom  l  <->  dom  e  =  U. dom  e ) )
105 fveq1 5540 . . . . . . . . . 10  |-  ( l  =  e  ->  (
l `  suc  ( rank `  g ) )  =  ( e `  suc  ( rank `  g )
) )
106105breqd 4050 . . . . . . . . 9  |-  ( l  =  e  ->  (
g ( l `  suc  ( rank `  g
) ) h  <->  g (
e `  suc  ( rank `  g ) ) h ) )
107106anbi2d 684 . . . . . . . 8  |-  ( l  =  e  ->  (
( ( rank `  g
)  =  ( rank `  h )  /\  g
( l `  suc  ( rank `  g )
) h )  <->  ( ( rank `  g )  =  ( rank `  h
)  /\  g (
e `  suc  ( rank `  g ) ) h ) ) )
108107orbi2d 682 . . . . . . 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 ) ) ) )
109108opabbidv 4098 . . . . . 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 ) ) } )
110 eqidd 2297 . . . . . . . . . . . . . . . 16  |-  ( l  =  e  ->  (
y `  g )  =  ( y `  g ) )
111102fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( l  =  e  ->  ( R1 `  dom  l )  =  ( R1 `  dom  e ) )
112103fveq2d 5545 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  e  ->  ( R1 `  U. dom  l
)  =  ( R1
`  U. dom  e ) )
113 id 19 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( l  =  e  ->  l  =  e )
114113, 103fveq12d 5547 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  e  ->  (
l `  U. dom  l
)  =  ( e `
 U. dom  e
) )
115114breqd 4050 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  e  ->  (
j ( l `  U. dom  l ) i  <-> 
j ( e `  U. dom  e ) i ) )
116115imbi1d 308 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
117112, 116raleqbidv 2761 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
118117anbi2d 684 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
119112, 118rexeqbidv 2762 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
120119opabbidv 4098 . . . . . . . . . . . . . . . 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 ) ) ) } )
121110, 111, 120supeq123d 27261 . . . . . . . . . . . . . . 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 ) ) ) } ) )
122121mpteq2dv 4123 . . . . . . . . . . . . . 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 ) ) ) } ) ) )
123111difeq1d 3306 . . . . . . . . . . . . . 14  |-  ( l  =  e  ->  (
( R1 `  dom  l )  \  ran  g )  =  ( ( R1 `  dom  e )  \  ran  g ) )
124122, 123fveq12d 5547 . . . . . . . . . . . . 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 ) ) )
125124mpteq2dv 4123 . . . . . . . . . . . 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 ) ) ) )
126 recseq 6405 . . . . . . . . . . . 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 ) ) ) ) )
127125, 126syl 15 . . . . . . . . . . 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 ) ) ) ) )
128127cnveqd 4873 . . . . . . . . . 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 ) ) ) ) )
129128imaeq1d 5027 . . . . . . . . 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 } ) )
130129inteqd 3883 . . . . . . . 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 } ) )
131128imaeq1d 5027 . . . . . . . . 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 } ) )
132131inteqd 3883 . . . . . . . 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 } ) )
133130, 132eleq12d 2364 . . . . . . 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 } ) ) )
134133opabbidv 4098 . . . . . 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 } ) } )
135104, 109, 134ifbieq12d 3600 . . . . 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 } ) } ) )
136111, 111xpeq12d 4730 . . . . 5  |-  ( l  =  e  ->  (
( R1 `  dom  l )  X.  ( R1 `  dom  l ) )  =  ( ( R1 `  dom  e
)  X.  ( R1
`  dom  e )
) )
137135, 136ineq12d 3384 . . . 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 ) ) ) )
138137cbvmptv 4127 . . 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 ) ) ) )
139 recseq 6405 . . 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 ,